Iic_diff_Ioc

Mathlib.Order.Interval.Set.LinearOrder

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

← MathLib Explorer

English

For a ≤ b, the difference Iic b \\ Ioc a b equals Iic (a ∧ b) (the infimum of a and b).

Русский

Для a ≤ b разность Iic(b) \\\\ Ioc(a,b) равна Iic(min(a,b)).

LaTeX

$$$Iic\\,b \\\\ Ioc a b = Iic(\\\\min a b)$$$

Lean4

theorem Iic_diff_Ioc : Iic b \ Ioc a b = Iic (a ⊓ b) := by
  rw [diff_eq, compl_Ioc, inter_union_distrib_left, Iic_inter_Iic, ← compl_Iic, inter_compl_self, union_empty, min_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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