sInf_eq — Mathlib

English

If S is not contained entirely in the top and S is bounded below, then theInfimum of S in WithTop α equals the embedding of the Infimum of the preimage in α.

Русский

Если S не полностью состоит из верхнего элемента и S ограничено снизу, то инфимума S в WithTop α равна вложению инфимума предобраза S в α.

LaTeX

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

Lean4

theorem sInf_eq [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) (h's : BddBelow s) :
    sInf s = ↑(sInf ((↑) ⁻¹' s) : α) :=
  if_neg <| by simp [hs, h's]

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