Upper/lower sets and fibrations

theorem Relation.Fibration.isLowerSet_image {α : Type u_1} {β : Type u_2} {f : α → β} [LE α] [LE β] (hf : Fibration (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) f) {s : Set α} (hs : IsLowerSet s) : IsLowerSet (f '' s)

theorem IsLowerSet.image_fibration {α : Type u_1} {β : Type u_2} {f : α → β} [LE α] [LE β] (hf : Relation.Fibration (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) f) {s : Set α} (hs : IsLowerSet s) : IsLowerSet (f '' s)

Alias of Relation.Fibration.isLowerSet_image.

theorem Relation.fibration_iff_isLowerSet_image_Iic {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [LE β] : Fibration (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) f ↔ ∀ (x : α), IsLowerSet (f '' Set.Iic x)

theorem Relation.fibration_iff_isLowerSet_image {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [LE β] : Fibration (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) f ↔ ∀ (s : Set α), IsLowerSet s → IsLowerSet (f '' s)

theorem Relation.fibration_iff_image_Iic {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] (hf : Monotone f) : Fibration (fun (x1 x2 : α) => x1 ≤ x2) (fun (x1 x2 : β) => x1 ≤ x2) f ↔ ∀ (x : α), f '' Set.Iic x = Set.Iic (f x)

theorem Relation.Fibration.isUpperSet_image {α : Type u_1} {β : Type u_2} {f : α → β} [LE α] [LE β] (hf : Fibration (fun (x1 x2 : α) => x1 ≥ x2) (fun (x1 x2 : β) => x1 ≥ x2) f) {s : Set α} (hs : IsUpperSet s) : IsUpperSet (f '' s)

theorem IsUpperSet.image_fibration {α : Type u_1} {β : Type u_2} {f : α → β} [LE α] [LE β] (hf : Relation.Fibration (fun (x1 x2 : α) => x1 ≥ x2) (fun (x1 x2 : β) => x1 ≥ x2) f) {s : Set α} (hs : IsUpperSet s) : IsUpperSet (f '' s)

Alias of Relation.Fibration.isUpperSet_image.

theorem Relation.fibration_iff_isUpperSet_image_Ici {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [LE β] : Fibration (fun (x1 x2 : α) => x1 ≥ x2) (fun (x1 x2 : β) => x1 ≥ x2) f ↔ ∀ (x : α), IsUpperSet (f '' Set.Ici x)

theorem Relation.fibration_iff_isUpperSet_image {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [LE β] : Fibration (fun (x1 x2 : α) => x1 ≥ x2) (fun (x1 x2 : β) => x1 ≥ x2) f ↔ ∀ (s : Set α), IsUpperSet s → IsUpperSet (f '' s)

theorem Relation.fibration_iff_image_Ici {α : Type u_1} {β : Type u_2} {f : α → β} [Preorder α] [Preorder β] (hf : Monotone f) : Fibration (fun (x1 x2 : α) => x1 ≥ x2) (fun (x1 x2 : β) => x1 ≥ x2) f ↔ ∀ (x : α), f '' Set.Ici x = Set.Ici (f x)