Theorems · Theorem · logic and foundations

Set.surj_on_of_inj_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) →
    (∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂) →
      t.ncard ≤ s.ncard →
        autoParam t.Finite Set.surj_on_of_inj_on_of_ncard_le._auto_1 → ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha

Defined in

Mathlib.Data.Set.Card

Cited by

1 results in Mathlib

Foundations

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