map_csInf — Mathlib

English

Let β be a ConditionallyCompleteLattice and s ⊆ α be nonempty. If f is monotone on s, then f(sInf s) = sInf (f'' s).

Русский

Пусть β — упорядоченная полная по условию решетка, s ⊆ α непусто. Если отображение f сохраняет порядок на s, то отображение инфимума сохраняется: f(sInf s) = sInf(f'' s).

LaTeX

$$$\text{Monotone on } s \Rightarrow f(sInf(s)) = sInf(f''s) \quad\text{(assuming } hs: s\neq \emptyset\text{)}$$$

Lean4

theorem map_csInf {β : Type*} [ConditionallyCompleteLattice β] {f : α → β} (hf : MonotoneOn f s) (hs : s.Nonempty) :
    f (sInf s) = sInf (f '' s) :=
  (hf.map_isLeast (isLeast_csInf hs)).csInf_eq.symm

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