fibration_iff_isLowerSet_image_Iic

English

A fibration is characterized by the property that for every x, the image under f of the interval Iic x is a lower set in the codomain, i.e., f''Iic x is a lower set for all x.

Русский

Фибрация характеризуется свойством: для каждого x образ под f множества Iic x образуется как нижнее множество в кодоменде.

LaTeX

$$$ \forall x, \ IsLowerSet( f'' Iic x ) $$$

Lean4

theorem fibration_iff_isLowerSet_image_Iic [Preorder α] [LE β] :
    Fibration (· ≤ ·) (· ≤ ·) 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⟩⟩

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