Ioc_inter_Iic

Mathlib.Order.Interval.Set.Basic

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

English

For a semilattice_inf α and elements a ≤ b, c, the intersection Ioc a b ∩ Iic c equals Ioc a (b ⊓ c).

Русский

В полупорядке с inf: пересечение интервалов (a, b] ∩ (−∞, c] равно (a, min(b,c)].

LaTeX

$$Ioc a b \cap Iic c = Ioc a (b ⊓ c)$$

Lean4

@[simp]
theorem Ioc_inter_Iic (a b c : α) : Ioc a b ∩ Iic c = Ioc a (b ⊓ c) := by
  rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_assoc, Iic_inter_Iic]

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

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

Разделы

Аффилиация

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