English
If a dependent function f on s maps into t and t is covered by the range of f, then surjectivity on s onto t holds.
Русский
Если зависимая функция на s имеет образ, равный t, то сюръекция на s на t выполняется.
LaTeX
$$∀ b ∈ t, ∃ a ∈ s, b = f(a, ha)$$
Lean4
/-- Given an injective map `f` defined on a finite set `s` to another finite set `t`, if `t` is no
larger than `s`, then `f` is surjective to `t` when restricted to `s`.
See `Finset.surjOn_of_injOn_of_card_le` for the version where `f` is a non-dependent function.
-/
theorem surj_on_of_inj_on_of_card_le (f : ∀ a ∈ s, β) (hf : ∀ a ha, f a ha ∈ t)
(hinj : ∀ a₁ a₂ ha₁ ha₂, f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂) (hst : #t ≤ #s) : ∀ b ∈ t, ∃ a ha, b = f a ha :=
by
let f' : s → β := fun a ↦ f a a.2
have hinj' : Set.InjOn f' s.attach := fun x hx y hy hxy ↦ Subtype.ext (hinj _ _ x.2 y.2 hxy)
have hmapsto' : Set.MapsTo f' s.attach t := fun x hx ↦ hf _ _
intro b hb
obtain ⟨a, ha, rfl⟩ := surjOn_of_injOn_of_card_le _ hmapsto' hinj' (by rwa [card_attach]) hb
exact ⟨a, a.2, rfl⟩
