Ioi_disjUnion_Iio — Mathlib

English

In a linearly ordered finite-type setting, the disjoint union of Ioi(a) and Iio(a) equals the complement of the singleton {a}.

Русский

Для линейно упорядоченного множества с конечным типом верно, что несовпадающее объединение Ioi(a) и Iio(a) равно дополнению к синглтону {a}.

LaTeX

$$(Ioi(a) ⊎ Iio(a)) = {a}^c$$

Lean4

theorem Ioi_disjUnion_Iio (a : α) : (Ioi a).disjUnion (Iio a) (disjoint_Ioi_Iio a) = ({ a } : Finset α)ᶜ :=
  by
  ext
  simp [eq_comm]

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