map_csInf — Mathlib

English

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

Русский

Пусть β — условно полноупорядоченная решетка, f: α → β монотонно. Если s непусто, то f(Inf s) = Inf( f'' s ).

LaTeX

$$$f(sInf(s)) = sInf(f''s) \quad\text{if } s \neq \varnothing$$$

Lean4

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

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