zero_of_map_zero — Mathlib

English

Two equivalent formulations of zero on pseudoelements are equivalent modulo isomorphism in Over P.

Русский

Две эквивалентные формулировки нуля на псевдоэлементах эквивалентны по отношению к изоморфизму в Over P.

LaTeX

$$$Eq\\;f\\;0\\;\\Leftrightarrow\\; \\forall a, pseudoApply f a =0$$$

Lean4

/-- A morphism that is injective on pseudoelements only maps the zero element to zero. -/
theorem zero_of_map_zero {P Q : C} (f : P ⟶ Q) : Function.Injective f → ∀ a, f a = 0 → a = 0 := fun h a ha =>
  by
  rw [← apply_zero f] at ha
  exact h ha

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