iInf_ker_lapply_le_bot — Mathlib

English

The infimum of the kernels of all lapply maps is contained in the bottom submodule (i.e., consists only of 0).

Русский

Пересечение ядер всех отображений lapply лежит в нулевом подпространстве.

LaTeX

$$$\bigwedge_{a} \ker (\mathrm{lapply} a) \le \bot$$$

Lean4

theorem iInf_ker_lapply_le_bot : ⨅ a, ker (lapply a : (α →₀ M) →ₗ[R] M) ≤ ⊥ :=
  by
  simp only [SetLike.le_def, mem_iInf, mem_ker, mem_bot, lapply_apply]
  exact fun a h => Finsupp.ext h

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