Mathlib.Order.UpperLower.Fibration

Relation.Fibration.isLowerSet_image theorem

[LE α] [LE β] (hf : Fibration (· ≤ ·) (· ≤ ·) f) {s : Set α} (hs : IsLowerSet s) : IsLowerSet (f '' s)

Full source

lemma Fibration.isLowerSet_image [LE α] [LE β] (hf : Fibration (· ≤ ·) (· ≤ ·) f)
    {s : Set α} (hs : IsLowerSet s) : IsLowerSet (f '' s) := by
  rintro _ y' e ⟨x, hx, rfl⟩; obtain ⟨y, e', rfl⟩ := hf e; exact ⟨_, hs e' hx, rfl⟩

Image of a Lower Set under a Fibration is a Lower Set

Informal description

Let $\alpha$ and $\beta$ be types equipped with a preorder relation $\leq$, and let $f : \alpha \to \beta$ be a fibration with respect to $\leq$ (i.e., $f$ preserves the order structure in a specific way). If $s \subseteq \alpha$ is a lower set (meaning for all $x \in s$ and $y \leq x$, $y \in s$), then the image $f(s)$ is also a lower set in $\beta$.

Relation.fibration_iff_isLowerSet_image_Iic theorem

[Preorder α] [LE β] : Fibration (· ≤ ·) (· ≤ ·) f ↔ ∀ x, IsLowerSet (f '' Iic x)

Full source

lemma fibration_iff_isLowerSet_image_Iic [Preorder α] [LE β] :
    FibrationFibration (· ≤ ·) (· ≤ ·) f ↔ ∀ x, IsLowerSet (f '' Iic x) :=
  ⟨fun h x ↦ (isLowerSet_Iic x).image_fibration h, fun H x _ e ↦ H x e ⟨x, le_rfl, rfl⟩⟩

Fibration Characterization via Lower Set Images of Intervals

Informal description

Let $\alpha$ be a preorder and $\beta$ be a type with a preorder relation $\leq$. A function $f : \alpha \to \beta$ is a fibration with respect to $\leq$ if and only if for every $x \in \alpha$, the image $f(\text{Iic } x)$ is a lower set in $\beta$, where $\text{Iic } x = (-\infty, x]$ denotes the left-infinite right-closed interval in $\alpha$.

Relation.fibration_iff_isLowerSet_image theorem

[Preorder α] [LE β] : Fibration (· ≤ ·) (· ≤ ·) f ↔ ∀ s, IsLowerSet s → IsLowerSet (f '' s)

Full source

lemma fibration_iff_isLowerSet_image [Preorder α] [LE β] :
    FibrationFibration (· ≤ ·) (· ≤ ·) f ↔ ∀ s, IsLowerSet s → IsLowerSet (f '' s) :=
  ⟨Fibration.isLowerSet_image,
    fun H ↦ fibration_iff_isLowerSet_image_Iic.mpr (H _ <| isLowerSet_Iic ·)⟩

Fibration Characterization via Preservation of Lower Sets

Informal description

Let $\alpha$ be a preorder and $\beta$ be a type with a preorder relation $\leq$. A function $f : \alpha \to \beta$ is a fibration with respect to $\leq$ if and only if for every lower set $s \subseteq \alpha$, the image $f(s)$ is a lower set in $\beta$.

Relation.fibration_iff_image_Iic theorem

[Preorder α] [Preorder β] (hf : Monotone f) : Fibration (· ≤ ·) (· ≤ ·) f ↔ ∀ x, f '' Iic x = Iic (f x)

Full source

lemma fibration_iff_image_Iic [Preorder α] [Preorder β] (hf : Monotone f) :
    FibrationFibration (· ≤ ·) (· ≤ ·) f ↔ ∀ x, f '' Iic x = Iic (f x) :=
  ⟨fun H x ↦ le_antisymm (fun _ ⟨_, hy, e⟩ ↦ e ▸ hf hy)
    ((H.isLowerSet_image (isLowerSet_Iic x)).Iic_subset ⟨x, le_rfl, rfl⟩),
    fun H ↦ fibration_iff_isLowerSet_image_Iic.mpr (fun x ↦ (H x).symm ▸ isLowerSet_Iic (f x))⟩

Fibration Characterization via Interval Image Equality for Monotone Functions

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $f : \alpha \to \beta$ be a monotone function. Then $f$ is a fibration with respect to the $\leq$ relations if and only if for every $x \in \alpha$, the image of the left-infinite right-closed interval $(-\infty, x]$ under $f$ is equal to the left-infinite right-closed interval $(-\infty, f(x)]$ in $\beta$.

Relation.Fibration.isUpperSet_image theorem

[LE α] [LE β] (hf : Fibration (· ≥ ·) (· ≥ ·) f) {s : Set α} (hs : IsUpperSet s) : IsUpperSet (f '' s)

Full source

lemma Fibration.isUpperSet_image [LE α] [LE β] (hf : Fibration (· ≥ ·) (· ≥ ·) f)
    {s : Set α} (hs : IsUpperSet s) : IsUpperSet (f '' s) :=
  @Fibration.isLowerSet_image αᵒᵈ βᵒᵈ _ _ _ hf s hs

Image of an Upper Set under a Fibration is an Upper Set

Informal description

Let $\alpha$ and $\beta$ be types equipped with a preorder relation $\geq$, and let $f : \alpha \to \beta$ be a fibration with respect to $\geq$ (i.e., $f$ preserves the order structure in a specific way). If $s \subseteq \alpha$ is an upper set (meaning for all $x \in s$ and $x \leq y$, $y \in s$), then the image $f(s)$ is also an upper set in $\beta$.

Relation.fibration_iff_isUpperSet_image_Ici theorem

[Preorder α] [LE β] : Fibration (· ≥ ·) (· ≥ ·) f ↔ ∀ x, IsUpperSet (f '' Ici x)

Full source

lemma fibration_iff_isUpperSet_image_Ici [Preorder α] [LE β] :
    FibrationFibration (· ≥ ·) (· ≥ ·) f ↔ ∀ x, IsUpperSet (f '' Ici x) :=
  @fibration_iff_isLowerSet_image_Iic αᵒᵈ βᵒᵈ _ _ _

Fibration Characterization via Upper Set Images of Right-Infinite Intervals

Informal description

Let $\alpha$ be a preorder and $\beta$ be a type with a preorder relation $\geq$. A function $f : \alpha \to \beta$ is a fibration with respect to $\geq$ if and only if for every $x \in \alpha$, the image $f([x, \infty))$ is an upper set in $\beta$, where $[x, \infty) = \{ y \in \alpha \mid x \leq y \}$ denotes the left-closed right-infinite interval in $\alpha$.

Relation.fibration_iff_isUpperSet_image theorem

[Preorder α] [LE β] : Fibration (· ≥ ·) (· ≥ ·) f ↔ ∀ s, IsUpperSet s → IsUpperSet (f '' s)

Full source

lemma fibration_iff_isUpperSet_image [Preorder α] [LE β] :
    FibrationFibration (· ≥ ·) (· ≥ ·) f ↔ ∀ s, IsUpperSet s → IsUpperSet (f '' s) :=
  @fibration_iff_isLowerSet_image αᵒᵈ βᵒᵈ _ _ _

Fibration Characterization via Preservation of Upper Sets

Informal description

Let $\alpha$ be a preorder and $\beta$ be a type with a preorder relation $\geq$. A function $f : \alpha \to \beta$ is a fibration with respect to $\geq$ if and only if for every upper set $s \subseteq \alpha$, the image $f(s)$ is an upper set in $\beta$.

Relation.fibration_iff_image_Ici theorem

[Preorder α] [Preorder β] (hf : Monotone f) : Fibration (· ≥ ·) (· ≥ ·) f ↔ ∀ x, f '' Ici x = Ici (f x)

Full source

lemma fibration_iff_image_Ici [Preorder α] [Preorder β] (hf : Monotone f) :
    FibrationFibration (· ≥ ·) (· ≥ ·) f ↔ ∀ x, f '' Ici x = Ici (f x) :=
  fibration_iff_image_Iic hf.dual

Fibration Characterization via Interval Image Equality for Monotone Functions with $\geq$ Relations

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $f : \alpha \to \beta$ be a monotone function. Then $f$ is a fibration with respect to the $\geq$ relations if and only if for every $x \in \alpha$, the image of the right-infinite left-closed interval $[x, \infty)$ under $f$ is equal to the right-infinite left-closed interval $[f(x), \infty)$ in $\beta$.