sInf_eq — Mathlib

English

Analogous to WithTop, the Infimum on WithBot α equals the embedding of the Infimum of the preimage when the set is not containing ⊥ and is bounded below.

Русский

Аналогично WithTop, инфимума на WithBot α равна вложению инфимума предобраза, если множество не содержит ⊥ и ограничено снизу.

LaTeX

$$$$ \operatorname{sInf} S = \uparrow\bigl( \operatorname{sInf}((\uparrow)^{-1} S) : \alpha \bigr). $$$$

Lean4

theorem sInf_eq [InfSet α] {s : Set (WithBot α)} (hs : ⊥ ∉ s) (hs' : BddBelow ((↑) ⁻¹' s : Set α)) :
    sInf s = ↑(sInf ((↑) ⁻¹' s) : α) :=
  (if_neg hs).trans <| if_pos hs'

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