Iic_subset_Iio

Mathlib.Order.Interval.Set.Basic

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

English

Iic(a) is contained in Iio(b) iff a < b.

Русский

Iic(a) вложено в Iio(b) тогда и только тогда, когда a < b.

LaTeX

$$$ \mathrm{Iic}(a) \subseteq \mathrm{Iio}(b) \iff a < b $$$

Lean4

@[simp]
theorem Iic_subset_Iio : Iic a ⊆ Iio b ↔ a < b :=
  ⟨fun h => h right_mem_Iic, fun h _ hx => lt_of_le_of_lt hx h⟩

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

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

Разделы

Аффилиация

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