isLowerSet_image — Mathlib

English

If f is a fibration between preorders, then the image of a lower set under f is again a lower set.

Русский

Если f — фибрация между предобразами, то образ нижнего множества под f снова является нижним множеством.

LaTeX

$$$ \text{IsLowerSet}(f''s) $$$

Lean4

theorem isLowerSet_image [LE α] [LE β] (hf : Fibration (· ≤ ·) (· ≤ ·) f) {s : Set α} (hs : IsLowerSet s) :
    IsLowerSet (f '' s) := by rintro _ y' e ⟨x, hx, rfl⟩; obtain ⟨y, e', rfl⟩ := hf e; exact ⟨_, hs e' hx, rfl⟩

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