fibration_iff_image_Ici — Mathlib

English

Let hf be a monotone map. Then the fibration property is equivalent to f''Iic x = Iic(f x) for all x.

Русский

Пусть hf — монотонное отображение. Тогда свойство фибрации эквивалентно f''Iic x = Iic(f x) для всех x.

LaTeX

$$$ Fibration(\le, \le, f) \iff \forall x, f'' Iic x = Iic (f x) $$$

Lean4

theorem fibration_iff_image_Ici [Preorder α] [Preorder β] (hf : Monotone f) :
    Fibration (· ≥ ·) (· ≥ ·) f ↔ ∀ x, f '' Ici x = Ici (f x) :=
  fibration_iff_image_Iic hf.dual

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