Iic_union_Ioc — Mathlib

English

Let α be a linearly ordered set and b,c,d ∈ α with min{c,d} < b. Then [−∞, b] ∪ (c, d] = [−∞, max{b,d}].

Русский

Пусть α — линейно упорядоченное множество, и b, c, d ∈ α удовлетворяют min{c,d} < b. Тогда {x : x ≤ b} ∪ {x : c < x ≤ d} = {x : x ≤ max(b,d)}.

LaTeX

$$$ \min(c,d) < b \implies Iic(b) \cup Ioc(c,d) = Iic(\max(b,d)). $$$

Lean4

theorem Iic_union_Ioc (h : min c d < b) : Iic b ∪ Ioc c d = Iic (max b d) :=
  by
  rcases le_total c d with hcd | hcd
  · simp only [hcd, inf_of_le_left] at h; exact Iic_union_Ioc' h
  · rw [max_comm]
    simp_all [max_eq_right_of_lt]

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