subset_sInf_of_within — Mathlib

English

If t is a nonempty subset of s with t Nonempty and BddBelow, and the infimum of the image lies in s, then the infimum equals the infimum inside s.

Русский

Если t ⊆ s непусто и ограничено снизу, и инфиминум образа лежит в s, то инфиминум совпадает с инфиминумом внутри s.

LaTeX

$$$$ \operatorname{sInf}_{s}((\uparrow)''t) = \operatorname{sInf}_{s}(t) $$$$

Lean4

theorem subset_sInf_of_within [Inhabited s] {t : Set s} (h' : t.Nonempty) (h'' : BddBelow t)
    (h : sInf ((↑) '' t : Set α) ∈ s) : sInf ((↑) '' t : Set α) = (@sInf s _ t : α) := by simp [h, h', h'']

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