Ioc_subset_uIoc

Mathlib.Order.Interval.Set.UnorderedInterval

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

English

If a ≤ b then Ι(a,b) = Ioc(a,b).

Русский

Если a ≤ b, то Ι(a,b) = Ioc(a,b).

LaTeX

$$$ a \\le b \\implies Ι(a,b) = Ioc(a,b) $$$

Lean4

theorem Ioc_subset_uIoc : Ioc a b ⊆ Ι a b :=
  Ioc_subset_Ioc (min_le_left _ _) (le_max_right _ _)

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

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

Разделы

Аффилиация

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