map'_surjective_iff — Mathlib

English

Surjectivity of map' f is equivalent to surjectivity of f.

Русский

Сюръективность map' f эквивалентна сюръективности f.

LaTeX

$$$ \\operatorname{Surjective}(\\mathrm{map}' f) \\iff \\operatorname{Surjective}(f) $$$

Lean4

theorem map'_surjective_iff {f : α →* β} : Surjective (map' f) ↔ Surjective f :=
  by
  simp only [Surjective, «forall»]
  refine ⟨fun h b ↦ ?_, fun h ↦ ⟨⟨0, by simp⟩, fun b ↦ ?_⟩⟩
  · obtain ⟨a, hab⟩ := h.2 b
    induction a using WithZero.recZeroCoe <;> simp at hab
    grind
  · obtain ⟨a, ha⟩ := h b
    use a
    simp [ha]

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