coe_injective — Mathlib

English

The natural inclusion m ↦ (m in DivisibleHull M) is injective, i.e., if m and m' have the same image, then m = m'.

Русский

Естественное включение $m \\mapsto (m\\in DivisibleHull M)$ инъективно: если образы совпадают, то исходные элементы равны.

LaTeX

$$$\\forall m,m'\\in M,\\; (m):(DivisibleHull M) = (m'):(DivisibleHull M) \\iff m=m'.$$$

Lean4

theorem coe_injective : Function.Injective ((↑) : M → DivisibleHull M) :=
  mk_left_injective 1

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