lmap_surjective — Mathlib

English

The map lmap f is surjective if and only if each f_i is surjective.

Русский

Отображение lmap f сюръективно тогда и только тогда, когда каждое f_i сюръективно.

LaTeX

$$$\\mathrm{Surjective}(\\mathrm{lmap}\\ f) \\iff \\forall i, \\ \\mathrm{Surjective}(f_i).$$$

Lean4

theorem lmap_surjective : Function.Surjective (lmap f) ↔ (∀ i, Function.Surjective (f i)) := by
  classical exact DFinsupp.mapRange_surjective (hf := fun _ ↦ map_zero _)

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