Theorems · Theorem · order theory

Set.card_image_of_inj_on

∀ {α : Type u} {β : Type v} {s : Set α} [inst : Fintype ↑s] {f : α → β} [inst_1 : Fintype ↑(f '' s)],
  (∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y) → Fintype.card ↑(f '' s) = Fintype.card ↑s

Defined in

Mathlib.Data.Set.Finite.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeFintype