iInf_ker_weight_eq_bot — Mathlib

English

The intersection of all weight kernels is the zero subspace.

Русский

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

LaTeX

$$$\bigwedge_{\alpha \in \mathrm{Weight}(K,H,L)} \ker(\alpha) = \bot$$$

Lean4

@[simp]
theorem iInf_ker_weight_eq_bot : ⨅ α : Weight K H L, α.ker = ⊥ :=
  by
  rw [← Subspace.dualAnnihilator_inj, Subspace.dualAnnihilator_iInf_eq, Submodule.dualAnnihilator_bot]
  simp [← LinearMap.range_dualMap_eq_dualAnnihilator_ker, ← Submodule.span_range_eq_iSup]

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