eq_Icc_of_connected_compact — Mathlib

English

If s is connected and compact, then s equals the closed interval from sInf s to sSup s.

Русский

Если s несамопересекается и компактно, то s совпадает с замкнутым интервалом между sInf s и sSup s.

LaTeX

$$$s = Icc( sInf\,s, sSup\,s )$$$

Lean4

theorem eq_Icc_of_connected_compact {s : Set α} (h₁ : IsConnected s) (h₂ : IsCompact s) : s = Icc (sInf s) (sSup s) :=
  eq_Icc_csInf_csSup_of_connected_bdd_closed h₁ h₂.bddBelow h₂.bddAbove h₂.isClosed

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