Ici_subset_Ioi

Mathlib.Order.Interval.Set.Basic

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

English

Ici(a) is contained in Ioi(b) iff b < a.

Русский

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

LaTeX

$$$ \mathrm{Ici}(a) \subseteq \mathrm{Ioi}(b) \iff b < a $$$

Lean4

@[simp]
theorem Ici_subset_Ioi : Ici a ⊆ Ioi b ↔ b < a :=
  ⟨fun h => h left_mem_Ici, fun h _ hx => h.trans_le hx⟩

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

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

Разделы

Аффилиация

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