injOn_of_disjoint_ker — Mathlib

English

Let p ⊆ M be a submodule and s ⊆ M with s ⊆ p. If p has trivial intersection with ker f, then f is injective on s.

Русский

Пусть p ⊆ M — подмодуль и пусть s ⊆ p. Если p пересечение с ker f тривиально, то f инъективно на s.

LaTeX

$$({s} ⊆ {p}) ∧ Disjoint(p, ker f) ⇒ Set.InjOn f s$$

Lean4

theorem injOn_of_disjoint_ker {p : Submodule R M} {s : Set M} (h : s ⊆ p) (hd : Disjoint p (ker f)) : Set.InjOn f s :=
  fun _ hx _ hy => disjoint_ker'.1 hd _ (h hx) _ (h hy)

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