Ioo_subset_openSegment

Mathlib.Analysis.Convex.Segment

URI: https://scilib.ai/kg/mathlib#Ioo_subset_openSegment

← MathLib Explorer

English

For any x,y, Ioo x y is contained in openSegment 𝕜 x y.

Русский

Для любых x,y множество Ioo x y содержится в openSegment 𝕜 x y.

LaTeX

$$$ Ioo(x,y) \subseteq openSegment_{\mathbb{k}}(x,y) $$$

Lean4

theorem Ioo_subset_openSegment : Ioo x y ⊆ openSegment 𝕜 x y := fun _ hz =>
  mem_openSegment_of_ne_left_right hz.1.ne hz.2.ne' <| Icc_subset_segment <| Ioo_subset_Icc_self hz

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

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

Разделы

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

Аффилиация

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