ker — Mathlib

English

If l has basis p s, then the kernel of l is the intersection of all s i with p i: l.ker = ⋂ i (p i), s i.

Русский

Если у l есть базис p s, то ядро l равно пересечению всех s i для которых p i верно: l.ker = ⋂ i, p i, s i.

LaTeX

$$$ l.ker = \bigcap_{i} (p(i) \to s(i)) $$$

Lean4

protected theorem ker (h : HasBasis l p s) : l.ker = ⋂ (i) (_ : p i), s i :=
  sInter_eq_biInter.trans <| h.biInter_mem monotone_id

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