iInf_ker_proj — Mathlib

English

Let (φ_i) be a family of R-modules. The intersection of all kernels of the coordinate projections ker(proj_i) is the zero submodule.

Русский

Пусть есть семейство модулей (φ_i). Пересечение ядер координатных проекций ker(proj_i) по всем i равно нулевому подпростольству.

LaTeX

$$$\\bigcap_{i} \\ker(\\mathrm{proj}_i) = \\{0\\}.$$$

Lean4

theorem iInf_ker_proj : (⨅ i, ker (proj i : ((i : ι) → φ i) →ₗ[R] φ i) : Submodule R ((i : ι) → φ i)) = ⊥ :=
  bot_unique <|
    SetLike.le_def.2 fun a h => by
      simp only [mem_iInf, mem_ker, proj_apply] at h
      exact (mem_bot _).2 (funext fun i => h i)

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