Ici_subset_Ico_union_Ici — Mathlib

English

For any a, b in a linear order and any x with x ≥ a, we have x ∈ [a,b) or x ∈ [b, ∞).

Русский

Для любых a, b в линейном порядке и любого x, такого что x ≥ a, верно: x лежит либо в [a, b), либо в [b, ∞).

LaTeX

$$$[a,\infty) \subseteq [a,b) \cup [b,\infty) $$$

Lean4

theorem Ici_subset_Ico_union_Ici : Ici a ⊆ Ico a b ∪ Ici b := fun x hx =>
  (lt_or_ge x b).elim (fun hxb => Or.inl ⟨hx, hxb⟩) fun hxb => Or.inr hxb

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