Theorems · Theorem · combinatorics

Finset.inj_on_of_surj_on_of_card_le

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

Given a surjective map f defined on a finite set s to another finite set t, if s is no larger than t, then f is injective when restricted to s. See Finset.injOn_of_surjOn_of_card_le for the version where f is a non-dependent function.

Defined in

Mathlib.Data.Finset.Card

Cited by

2 results in Mathlib

Foundations

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