fibration_iff_image_Iic — Mathlib

English

Let f be a monotone map between preorders. Then f is a fibration iff for all x, f''Iic x = Iic(f x).

Русский

Пусть f — монотонное отображение между порядками. Тогда f является фибрацией тогда и только тогда, когда для всех x выполняется равенство f''Iic x = Iic(f x).

LaTeX

$$$ Fibration(\le, \le, f) \iff \forall x, f''Iic x = Iic(f x) $$$

Lean4

theorem fibration_iff_image_Iic [Preorder α] [Preorder β] (hf : Monotone f) :
    Fibration (· ≤ ·) (· ≤ ·) 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))⟩

Похожие утверждения