English
A map f is a fibration iff the image of every lower set under f is again a lower set.
Русский
Отображение f является фибрацией тогда и только тогда, когда образ каждого нижнего множества под f снова является нижним множеством.
LaTeX
$$$ \text{Fibration}(\le, \le, f) \iff \forall s, \text{IsLowerSet}(s) \rightarrow \text{IsLowerSet}(f''s) $$$
Lean4
theorem fibration_iff_isLowerSet_image [Preorder α] [LE β] :
Fibration (· ≤ ·) (· ≤ ·) f ↔ ∀ s, IsLowerSet s → IsLowerSet (f '' s) :=
⟨Fibration.isLowerSet_image, fun H ↦ fibration_iff_isLowerSet_image_Iic.mpr (H _ <| isLowerSet_Iic ·)⟩