isUpperSet_image — Mathlib

English

Under a fibration, the image of an upper set is again an upper set (dually via order reversal).

Русский

При фибрации образ верхнего множества снова является верхним множеством (взаимно через обращение порядка).

LaTeX

$$$ \forall s, \text{IsUpperSet}(s) \Rightarrow \text{IsUpperSet}(f''s) $$$

Lean4

theorem isUpperSet_image [LE α] [LE β] (hf : Fibration (· ≥ ·) (· ≥ ·) f) {s : Set α} (hs : IsUpperSet s) :
    IsUpperSet (f '' s) :=
  @Fibration.isLowerSet_image αᵒᵈ βᵒᵈ _ _ _ hf s hs

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