Ioi_inter_Ioi

Mathlib.Order.Interval.Set.LinearOrder

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

English

If a < b and b ≤ c, then Ioc a b ∪ Icc b c = Ioc a c.

Русский

Если a < b и b ≤ c, то Ioc(a,b) ∪ Icc(b,c) = Ioc(a,c).

LaTeX

$$$(a < b) \land (b \le c) \implies \mathrm{Ioc}(a,b) \cup \mathrm{Icc}(b,c) = \mathrm{Ioc}(a,c)$$$

Lean4

@[simp]
theorem Ioi_inter_Ioi : Ioi a ∩ Ioi b = Ioi (a ⊔ b) :=
  ext fun _ => sup_lt_iff.symm

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

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

Разделы

Аффилиация

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