English
Cardinality is preserved by a bijection (Equiv) between the ambient types, provided the membership correspondence holds on the relevant finite sets.
Русский
Кардинал сохраняется биекцией между типами, если соответствие принадлежности сохраняется на данных подмножеств.
LaTeX
$$card_equiv e hst$$
Lean4
/-- Specialization of `Finset.card_nbij'` that automatically fills in most arguments.
See `Fintype.card_equiv` for the version where `s` and `t` are `univ`. -/
theorem card_equiv (e : α ≃ β) (hst : ∀ i, i ∈ s ↔ e i ∈ t) : #s = #t := by
refine card_nbij' e e.symm ?_ ?_ ?_ ?_ <;> simp [hst, Set.MapsTo, Set.LeftInvOn, Set.RightInvOn]
