fibration_iff_isUpperSet_image — Mathlib

English

An equivalent formulation: the fibration property is equivalent to the statement that for all s, IsUpperSet s implies IsUpperSet (f '' s).

Русский

Эквивалентная формулировка: свойство фибрации эквивалентно утверждению, что для всех s, если s — верхнее множество, то f''s — верхнее множество.

LaTeX

$$$ \forall s, \ IsUpperSet(s) \rightarrow \ IsUpperSet(f''s) $$$

Lean4

theorem fibration_iff_isUpperSet_image [Preorder α] [LE β] :
    Fibration (· ≥ ·) (· ≥ ·) f ↔ ∀ s, IsUpperSet s → IsUpperSet (f '' s) :=
  @fibration_iff_isLowerSet_image αᵒᵈ βᵒᵈ _ _ _

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