Theorems · Theorem · logic and foundations

Set.ncard_eq_of_bijective

∀ {α : Type u_1} {s : Set α} {n : ℕ} (f : (i : ℕ) → i < n → α),
  (∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a) →
    (∀ (i : ℕ) (h : i < n), f i h ∈ s) → (∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j) → s.ncard = n

Defined in

Mathlib.Data.Set.Card

Cited by

2 results in Mathlib

Foundations

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