map_surjective_of_surjective — Mathlib

English

If f is surjective, map f is surjective on multisets: for every multiset s there exists t with map f t = s.

Русский

Если f сюръективна, отображение map f сюръективно на мультимножества: для каждого мультимножества s существует t, такое что map f t = s.

LaTeX

$$$$ \\text{If } hf : \\operatorname{Surjective}(f), \\ \\forall s, \\exists t, \\operatorname{map} f t = s $$$$

Lean4

theorem map_surjective_of_surjective {f : α → β} (hf : Function.Surjective f) : Function.Surjective (map f) :=
  by
  intro s
  induction s using Multiset.induction_on with
  | empty => exact ⟨0, map_zero _⟩
  | cons x s ih =>
    obtain ⟨y, rfl⟩ := hf x
    obtain ⟨t, rfl⟩ := ih
    exact ⟨y ::ₘ t, map_cons _ _ _⟩

Похожие утверждения