Theorems · Theorem · combinatorics

Finset.card_bij

∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : (a : α) → a ∈ s → β),
  (∀ (a : α) (ha : a ∈ s), i a ha ∈ t) →
    (∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) →
      (∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b) → s.card = t.card

Given a bijection from a finite set s to a finite set t, the cardinalities of s and t are equal. The difference with Finset.card_bij' is that the bijection is specified as a surjective injection, rather than by an inverse function. The difference with Finset.card_nbij is that the bijection is allowed to use membership of the domain, rather than being a non-dependent function.

Defined in

Mathlib.Data.Finset.Card

Cited by

10 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound