map_le_map_iff' — Mathlib

English

If the kernel of a semilinear map f is trivial, then the map p ↦ map f p on submodules is injective; that is, map f p = map f p' implies p = p'.

Русский

Если ядро отображения f равно нулю, то отображение подмодулов p ↦ map f p инъективно, то есть map f p = map f p' тогда и только тогда p = p'.

LaTeX

$$$\ker f = \{0\} \Rightarrow (p \mapsto \operatorname{map} f\,p)\ ext{инъективно}$$$

Lean4

theorem map_le_map_iff' {f : F} (hf : ker f = ⊥) {p p'} : map f p ≤ map f p' ↔ p ≤ p' := by
  rw [LinearMap.map_le_map_iff, hf, sup_bot_eq]

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