finite_of_compl — Mathlib

English

If S and its complement are finite, then the ambient type is finite.

Русский

Если множество и его дополнение конечны, то базовый тип конечен.

LaTeX

$$$\forall {\alpha : Type u} {s : Set\alpha}, Finite s → Finite (s^c) → Finite \alpha$$$

Lean4

theorem finite_of_compl {s : Set α} (hs : s.Finite) (hsc : sᶜ.Finite) : Finite α :=
  by
  rw [← finite_univ_iff, ← union_compl_self s]
  exact hs.union hsc

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