mk_equiv_comm — Mathlib

English

The cardinality of equivalences is invariant under swapping domain and codomain, i.e., #(α ≃ β) = #(β ≃ α).

Русский

Кардинал эквивалентностей не изменяется при смене места определения и кодирования: #(α ≃ β) = #(β ≃ α).

LaTeX

$$$ #(\\alpha \\simeq \\beta) = #(\\beta \\simeq \\alpha) $$$

Lean4

/-- This lemma makes lemmas assuming `Infinite α` applicable to the situation where we have
  `Infinite β` instead. -/
theorem mk_equiv_comm : #(α ≃ β') = #(β' ≃ α) :=
  (ofBijective _ symm_bijective).cardinal_eq

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