csInf_eq_least_of_bdd — Mathlib

English

If s is nonempty and bounded below by b, then the infimum of s equals the leastOfBdd b Hb Hinh: sInf s = leastOfBdd b Hb Hinh.

Русский

Если множество s непусто и ограничено снизу головой b, то инфиминум множества равен leastOfBdd b Hb Hinh.

LaTeX

$$$\operatorname{sInf}(s) = \mathrm{leastOfBdd}(b,\ Hb,\ Hinh)$$$

Lean4

theorem csInf_eq_least_of_bdd {s : Set ℤ} [DecidablePred (· ∈ s)] (b : ℤ) (Hb : ∀ z ∈ s, b ≤ z)
    (Hinh : ∃ z : ℤ, z ∈ s) : sInf s = leastOfBdd b Hb Hinh :=
  by
  have : s.Nonempty ∧ BddBelow s := ⟨Hinh, b, Hb⟩
  simp only [sInf, dif_pos this]
  convert (coe_leastOfBdd_eq Hb (Classical.choose_spec (⟨b, Hb⟩ : BddBelow s)) Hinh).symm

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