card_ne_eq — Mathlib

English

For a finite type α and a ∈ α, the cardinality of {x ≠ a} equals |α| − 1.

Русский

Для конечного типа α и элемента a мощность множества {x ≠ a} равна |α| − 1.

LaTeX

$$$ [Fintype α] (a) [Fintype {x : α | x \\neq a}] : Fintype.card {x : α | x \\neq a} = Fintype.card α - 1 $$$

Lean4

theorem card_ne_eq [Fintype α] (a : α) [Fintype {x : α | x ≠ a}] : Fintype.card {x : α | x ≠ a} = Fintype.card α - 1 :=
  by
  haveI := Classical.decEq α
  rw [← toFinset_card, toFinset_setOf, Finset.filter_ne', Finset.card_erase_of_mem (Finset.mem_univ _),
    Finset.card_univ]

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