ruzsaSzemerediNumberNat_card — Mathlib

English

Equality between nat-based RS-number and RS-number via equivalence FINITE_CARD.

Русский

Эквивалентность RS-чисел через эквивалентность между конечными типами и натуральной картой.

LaTeX

$$$$ \\ ruzsaSzemerediNumberNat_card : \\ ruzsaSzemerediNumberNat (card α) = \\ ruzsaSzemerediNumber α. $$$$

Lean4

@[simp]
theorem ruzsaSzemerediNumberNat_card : ruzsaSzemerediNumberNat (card α) = ruzsaSzemerediNumber α :=
  ruzsaSzemerediNumber_congr (Fintype.equivFin _).symm

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