Iic_ssubset_Iic

Mathlib.Order.Interval.Set.Basic

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

English

Iic(a) is a proper subset of Iic(b) iff a < b.

Русский

Iic(a) является строгим подмножеством Iic(b) тогда и только тогда, когда a < b.

LaTeX

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

Lean4

@[simp]
theorem Iic_ssubset_Iic : Iic a ⊂ Iic b ↔ a < b :=
  @Ici_ssubset_Ici αᵒᵈ _ _ _

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

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

Разделы

Аффилиация

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