Ioi_subset_Ioo_union_Ici

Mathlib.Order.Interval.Set.LinearOrder

URI: https://scilib.ai/kg/mathlib#Set.Ioi_subset_Ioo_union_Ici

English

Ioi a is contained in Ioo a b ∪ Ici b for any b > a.

Русский

Ioi a содержится в Ioo a b ∪ Ici b при любом b > a.

LaTeX

$$$ \text{Ioi}(a) \subseteq \text{Ioo}(a,b) \cup \text{Ici}(b) $ for any b > a$$

Lean4

theorem Ioi_subset_Ioo_union_Ici : Ioi a ⊆ Ioo a b ∪ Ici b := fun x hx =>
  (lt_or_ge x b).elim (fun hxb => Or.inl ⟨hx, hxb⟩) fun hxb => Or.inr hxb

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

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

Разделы

Аффилиация

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