Icc_subset

Mathlib.Topology.Order.IntermediateValue

URI: https://scilib.ai/kg/mathlib#IsConnected.Icc_subset

← MathLib Explorer

English

If s is connected and a,b ∈ s, then Icc(a,b) ⊆ s.

Русский

Если s связано и a,b ∈ s, то Icc(a,b) ⊆ s.

LaTeX

$$$a\in s \land b\in s \Rightarrow Icc(a,b) \subseteq s$$$

Lean4

/-- If a preconnected set contains endpoints of an interval, then it includes the whole interval. -/
theorem Icc_subset {s : Set α} (hs : IsConnected s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : Icc a b ⊆ s :=
  hs.2.Icc_subset ha hb

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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