eq_Icc_csInf_csSup_of_connected_bdd_closed

English

If s is connected, bounded below and above, and closed, then s equals the closed interval between its infimum and supremum.

Русский

Если s связно, ограничено снизу и сверху и замкнуто, то s = [sInf(s), sSup(s)].

LaTeX

$$$\text{IsConnected}(s) \land BddBelow(s) \land BddAbove(s) \land \text{IsClosed}(s) \Rightarrow s = Icc(sInf(s), sSup(s))$$$

Lean4

theorem eq_Icc_csInf_csSup_of_connected_bdd_closed {s : Set α} (hc : IsConnected s) (hb : BddBelow s) (ha : BddAbove s)
    (hcl : IsClosed s) : s = Icc (sInf s) (sSup s) :=
  (subset_Icc_csInf_csSup hb ha).antisymm <| hc.Icc_subset (hcl.csInf_mem hc.nonempty hb) (hcl.csSup_mem hc.nonempty ha)

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