eq — Mathlib · SciLib

English

For any types α and β, the cardinalities are equal if and only if the types α and β are in bijection (there exists an equivalence α ≃ β).

Русский

Для любых типов α и β кардинальности равны тогда и только тогда, когда между типами α и β существует биекция (существует эквивалентность α ≃ β).

LaTeX

$$$\\#\\alpha = \\#\\beta \\;\\iff\\; \\exists e:\\; \\alpha \\simeq \\beta$$$

Lean4

protected theorem eq : #α = #β ↔ Nonempty (α ≃ β) :=
  Quotient.eq'

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