Ico_subset_Icc_self

Mathlib.Order.Interval.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.Ico_subset_Icc_self

English

For any a and b, the half-open interval Ico(a, b) is contained in the closed interval Icc(a, b).

Русский

Ico(a,b) ⊆ Icc(a,b) для любых a,b.

LaTeX

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

Lean4

theorem Ico_subset_Icc_self : Ico a b ⊆ Icc a b :=
  by
  rw [← coe_subset, coe_Ico, coe_Icc]
  exact Set.Ico_subset_Icc_self

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

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

Разделы

Аффилиация

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