span_eq_bot — Mathlib

English

For any subset S of M, span_R(S) equals the bottom submodule (⊥) if and only if every element of S is zero in M.

Русский

Для любой подмножества S множества M линейная оболочка span_R(S) равна нижнему подмодулю (⊥) тогда и только тогда, когда каждый элемент S равен нулю в M.

LaTeX

$$$\operatorname{span}_R(S) = \bot \;\Longleftrightarrow\; \forall x\in S, x=0$$$

Lean4

@[simp]
theorem span_eq_bot : span R (s : Set M) = ⊥ ↔ ∀ x ∈ s, (x : M) = 0 :=
  eq_bot_iff.trans
    ⟨fun H _ h => (mem_bot R).1 <| H <| subset_span h, fun H => span_le.2 fun x h => (mem_bot R).2 <| H x h⟩

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