Iic_ssubset_Iic

Mathlib.Order.Interval.Finset.Basic

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

English

For a ≤ b, the strict subset relation between Iic(a) and Iic(b) holds iff a < b.

Русский

Если a < b, то Iic(a) ⊊ Iic(b).

LaTeX

$$Iic(a) ⊂ Iic(b) \iff a < b$$

Lean4

@[simp]
theorem Iic_ssubset_Iic : Iic a ⊂ Iic b ↔ a < b := by simp [← coe_ssubset]

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

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

Разделы

Аффилиация

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