le_ker_coord_of_notMem_range — Mathlib

English

If i is not in the range of snf.f, then N is contained in the kernel of snf.bM.coord i.

Русский

Если i не принадлежит диапазону snf.f, то N ⊆ ker (snf.bM.coord i).

LaTeX

$$$\\forall i, i \\notin \\operatorname{range}(snf.f) \\Rightarrow N \\le \\ker (snf.bM.coord i)$$$

Lean4

theorem le_ker_coord_of_notMem_range {i : ι} (hi : i ∉ Set.range snf.f) : N ≤ LinearMap.ker (snf.bM.coord i) :=
  fun m hm ↦ snf.repr_eq_zero_of_notMem_range ⟨m, hm⟩ hi

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