Ioo_inter_Ioi — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem Ioo_inter_Ioi : Ioo a b ∩ Ioi c = Ioo (max a c) b :=
  by
  ext
  simp_rw [mem_inter_iff, mem_Ioo, mem_Ioi, max_lt_iff, and_assoc, and_comm]

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