Ici_subset_Ici

Mathlib.Order.Interval.Set.Basic

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

English

The interval Ici(a) is contained in Ici(b) iff b ≤ a.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ici_subset_Ici : Ici a ⊆ Ici b ↔ b ≤ a :=
  ⟨fun h => h <| left_mem_Ici, fun h _ hx => h.trans hx⟩

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

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

Разделы

Аффилиация

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