mem_span_insert — Mathlib

English

Adding an element x to a set s increases the span to the sum of spans: span(insert x s) = span({x}) ⊔ span(s).

Русский

Добавление элемента x к множеству s приводит к сумме порождений: span(insert x s) = span({x}) ⊔ span(s).

LaTeX

$$$\\operatorname{span}(\\operatorname{insert}(x,s)) = \\operatorname{span}(\\{x\\}) \\;\\sqcup\\; \\operatorname{span}(s)$$$

Lean4

theorem mem_span_insert {s : Set α} {x y} : x ∈ span (insert y s) ↔ ∃ a, ∃ z ∈ span s, x = a * y + z :=
  Submodule.mem_span_insert

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