span_relation_le_ker_π — Mathlib

English

The span of the relation images is contained in the kernel of π.

Русский

Оболочка изображений отношений содержится в ядре π.

LaTeX

$$\operatorname{span}_A(\mathrm{Set.range}(\text{relations.relation})) \le \ker(\text{solution.π})$$

Lean4

theorem span_relation_le_ker_π : Submodule.span A (Set.range relations.relation) ≤ LinearMap.ker solution.π :=
  by
  rw [Submodule.span_le]
  rintro _ ⟨r, rfl⟩
  simp only [SetLike.mem_coe, LinearMap.mem_ker, π_relation]

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