subset_Icc_csInf_csSup — Mathlib

English

If s is bounded below and bounded above, then s ⊆ Icc(sInf s, sSup s).

Русский

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

LaTeX

$$$(BddBelow\, s) \land (BddAbove\, s) \rightarrow s \subseteq \mathrm{Icc}(\mathrm{sInf}(s), \mathrm{sSup}(s))$$$

Lean4

theorem subset_Icc_csInf_csSup (hb : BddBelow s) (ha : BddAbove s) : s ⊆ Icc (sInf s) (sSup s) := fun _ hx =>
  ⟨csInf_le hb hx, le_csSup ha hx⟩

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