iInf_ker_proj — Mathlib

English

For the product space ∏_{i∈I} φ_i and the coordinate projections proj_i, the greatest lower bound (infimum) of all kernels ker(proj_i) is the zero subspace: ⨅_{i} ker(proj_i) = ⊥.

Русский

Для пространства произведения и проекций на координаты ker(proj_i) имеют общую младшую границу равную нулевому подпространству: ⨅_{i} ker(proj_i) = ⊥.

LaTeX

$$$ \\bigwedge_{i} \\ker(\\mathrm{proj}_i) = \\bot$$$

Lean4

theorem iInf_ker_proj : (⨅ i, ker (proj i : (∀ i, φ i) →L[R] φ i) : Submodule R (∀ i, φ i)) = ⊥ :=
  LinearMap.iInf_ker_proj

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