Icc_subset_Icc_union_Ioc — Mathlib

English

Let α be a linear order. For all a,b,c ∈ α and all x, if a ≤ x ≤ c then either a ≤ x ≤ b or b < x ≤ c.

Русский

Пусть α — линейно упорядоченное множество. Для любых a, b, c ∈ α и любого x, принадлежащего [a, c], верно: либо a ≤ x ≤ b, либо b < x ≤ c.

LaTeX

$$$\mathrm{Icc}(a,c) \subseteq \mathrm{Icc}(a,b) \cup \mathrm{Ioc}(b,c)$$$

Lean4

theorem Icc_subset_Icc_union_Ioc : Icc a c ⊆ Icc a b ∪ Ioc b c := fun x hx =>
  (le_or_gt x b).elim (fun hxb => Or.inl ⟨hx.1, hxb⟩) fun hxb => Or.inr ⟨hxb, hx.2⟩

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