encard_ne_add_one — Mathlib

English

For any a, the ENat-card of {x | x ≠ a} plus 1 equals ENat.card α.

Русский

Для любого a кардинал ENat множества {x | x ≠ a} плюс 1 равен ENat.card α.

LaTeX

$$$ (\{x \mid x \ne a\}).encard + 1 = \operatorname{ENat.card} \alpha $$$

Lean4

theorem encard_ne_add_one (a : α) : ({x | x ≠ a}).encard + 1 = ENat.card α :=
  by
  have : Disjoint {x | x ≠ a} { a } := disjoint_singleton_right.mpr <| by simp
  replace this := (Set.encard_union_eq this).symm
  have aux : {x | x ≠ a} ∪ { a } = univ := by ext x; simp [eq_or_ne x a]
  rwa [encard_singleton, aux, encard_univ] at this

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