Ioo_union_Ioi — Mathlib

English

Ioo a b ∪ Ioi c equals Ioi(min a c) under a certain order-theoretic condition.

Русский

Союз интервалов Ioo(a,b) и Ioi(c) равен интервалу Ioi(min(a,c)) при условии порядка.

LaTeX

$$$ Ioo(a,b) \cup Ioi(c) = Ioi(\min(a,c)) \quad\text{under suitable order conditions}$$$

Lean4

theorem Ioo_union_Ioi (h : c < max a b) : Ioo a b ∪ Ioi c = Ioi (min a c) :=
  by
  rcases le_total a b with hab | hab
  · simp only [hab, sup_of_le_right] at h; exact Ioo_union_Ioi' h
  · rw [min_comm]
    simp_all [min_eq_left_of_lt]

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