map_isLeast — Mathlib

English

If f is RightOrdContinuous, then for any subset s ⊆ α and x ∈ α, if x is the least element of s, then f(x) is the least element of f''s.

Русский

Если f — правая непрерывность, то для любой подмножества s ⊆ α и x ∈ α, если x — наименьший элемент в s, то f(x) — наименьший элемент в множестве f''s.

LaTeX

$$$ \\text{RightOrdContinuous}(f) \\Rightarrow \\forall s \\subseteq \\alpha, \\forall x, \\mathrm{IsLeast}(s,x) \\Rightarrow \\mathrm{IsLeast}(f''s, f(x)). $$$

Lean4

theorem map_isLeast (hf : RightOrdContinuous f) {s : Set α} {x : α} (h : IsLeast s x) : IsLeast (f '' s) (f x) :=
  hf.orderDual.map_isGreatest h

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