card_bijective — Mathlib

English

Specialization: if e is a bijection between α and β and membership correspondence holds, then |s| = |t|.

Русский

Специализация: если e — биекция между α и β и выполняется соответствие принадлежностей, то |s| = |t|.

LaTeX

$$card_bijective e hst$$

Lean4

/-- Specialization of `Finset.card_nbij` that automatically fills in most arguments.

See `Fintype.card_bijective` for the version where `s` and `t` are `univ`. -/
theorem card_bijective (e : α → β) (he : e.Bijective) (hst : ∀ i, i ∈ s ↔ e i ∈ t) : #s = #t :=
  card_equiv (.ofBijective e he) hst

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