subset_Icc_sInf_sSup

Mathlib.Topology.Order.Bornology

URI: https://scilib.ai/kg/mathlib#Bornology.IsBounded.subset_Icc_sInf_sSup

English

If s is bounded, then every element of s lies between its infimum and supremum.

Русский

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

LaTeX

$$$\operatorname{IsBounded}(s) \rightarrow s \subseteq Icc(\operatorname{sInf}(s), \operatorname{sSup}(s))$$$

Lean4

protected theorem subset_Icc_sInf_sSup (hs : IsBounded s) : s ⊆ Icc (sInf s) (sSup s) :=
  subset_Icc_csInf_csSup hs.bddBelow hs.bddAbove

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru