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
{α : 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.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
{α : 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)