map_surjective_iff — Mathlib

English

Map f is surjective if and only if f is surjective.

Русский

Map f сюръективно тогда и только тогда, когда f сюръективен.

LaTeX

$$$$\operatorname{map} f \text{ is surjective} \iff f \text{ is surjective}.$$$$

Lean4

theorem map_surjective_iff : Function.Surjective (map (σ := σ) f) ↔ Function.Surjective f :=
  ⟨fun h s ↦
    let ⟨p, h⟩ := h (C s);
    ⟨p.coeff 0, by simpa [coeff_map] using congr(coeff 0 $h)⟩,
    map_surjective f⟩

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