Theorems · Theorem · logic and foundations

Set.inj_on_of_surj_on_of_ncard_le

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (f : (a : α) → a ∈ s → β),
  (∀ (a : α) (ha : a ∈ s), f a ha ∈ t) →
    (∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b) →
      s.ncard ≤ t.ncard →
        ∀ ⦃a₁ : α⦄ (ha₁ : a₁ ∈ s) ⦃a₂ : α⦄ (ha₂ : a₂ ∈ s),
          f a₁ ha₁ = f a₂ ha₂ → autoParam s.Finite Set.inj_on_of_surj_on_of_ncard_le._auto_1 → a₁ = a₂

Defined in

Mathlib.Data.Set.Card

Cited by

0 results in Mathlib

Foundations

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