English
If a dependent function f on s maps into t, is surjective from s onto t, and |s| ≤ |t|, then f is injective on s.
Русский
Если зависимая функция на s отображает в t, сюръективна на s в t и |s| ≤ |t|, то она инъективна на s.
LaTeX
$$MapsTo f s t ∧ SurjOn f s t ∧ |s| ≤ |t| → InjOn f s$$
Lean4
/-- 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.
-/
theorem inj_on_of_surj_on_of_card_le (f : ∀ a ∈ s, β) (hf : ∀ a ha, f a ha ∈ t) (hsurj : ∀ b ∈ t, ∃ a ha, f a ha = b)
(hst : #s ≤ #t) ⦃a₁⦄ (ha₁ : a₁ ∈ s) ⦃a₂⦄ (ha₂ : a₂ ∈ s) (ha₁a₂ : f a₁ ha₁ = f a₂ ha₂) : a₁ = a₂ :=
by
let f' : s → β := fun a ↦ f a a.2
have hsurj' : Set.SurjOn f' s.attach t := fun x hx ↦ by simpa [f'] using hsurj x hx
have hinj' := injOn_of_surjOn_of_card_le f' (fun x hx ↦ hf _ _) hsurj' (by simpa)
exact congrArg Subtype.val (@hinj' ⟨a₁, ha₁⟩ (by simp) ⟨a₂, ha₂⟩ (by simp) ha₁a₂)
