fibration_iff_isLowerSet_image — Mathlib

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

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