equivOfCardEq — Mathlib

English

If #s = #t, then there is an equivalence s ≃ t.

Русский

Если #s = #t, то существует эквив s ≃ t.

LaTeX

$${s : Finset α}{t : Finset β}(h : #s = #t) → s ≃ t$$

Lean4

/-- Noncomputable equivalence between two finsets `s` and `t` as fintypes when there is a proof
that `#s = #t`. -/
noncomputable def equivOfCardEq {s : Finset α} {t : Finset β} (h : #s = #t) : s ≃ t :=
  Fintype.equivOfCardEq ((Fintype.card_coe _).trans (h.trans (Fintype.card_coe _).symm))

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