Ioi_inter_Ioo — Mathlib

English

Let α be a linearly ordered set and a, b, c ∈ α. Then the intersection (a, ∞) ∩ (b, c) equals (max(a, b), c).

Русский

Пусть α — линейно упорядоченное множество и a, b, c ∈ α. Тогда пересечение (a, ∞) и (b, c) равняется (max(a, b), c).

LaTeX

$$$Ioi a \\\\cap Ioo b c = Ioo (\\\\max a b) c$$$

Lean4

theorem Ioi_inter_Ioo : Set.Ioi a ∩ Set.Ioo b c = Set.Ioo (max a b) c := by rw [inter_comm, Ioo_inter_Ioi, max_comm]

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