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))⟩