uIoc_eq_union — Mathlib

English

The unordered open-closed interval equals the union of the two ordinary open-closed intervals with reversed endpoints: Ι(a,b) = Ioc(a,b) ∪ Ioc(b,a).

Русский

Неупорядоченный открыто-закрытый интервал равен объединению двух обычных открыто-закрытых интервалов с обращением концов: Ι(a,b) = Ioc(a,b) ∪ Ioc(b,a).

LaTeX

$$$ Ι(a,b) = Ioc(a,b) \\cup Ioc(b,a) $$$

Lean4

theorem uIoc_eq_union : Ι a b = Ioc a b ∪ Ioc b a := by cases le_total a b <;> simp [uIoc, *]

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