Ico_subset_Ici_self

Mathlib.Order.Interval.Set.Basic

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

English

If a ≤ x < b, then x ≥ a. In symbols: Ico(a, b) ⊆ Ici(a).

Русский

Если a ≤ x < b, то x ≥ a. То есть Ico(a, b) ⊆ Ici(a).

LaTeX

$$$$Ico(a,b) \subseteq Ici(a)$$$$

Lean4

theorem Ico_subset_Ici_self : Ico a b ⊆ Ici a := fun _ => And.left

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

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

Разделы

Аффилиация

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