span_nat_eq — Mathlib

English

In general, for a AddSubmonoid s of M, span Nat of its underlying set equals the AddSubmonoid closure of s.

Русский

Для произвольного AddSubmonoid s в M Span Nat от множества s равно замыканию AddSubmonoid от s.

LaTeX

$$$$ (\operatorname{span} \mathbb{N} (s : Set M)).\text{toAddSubmonoid} = \operatorname{AddSubmonoid}.closure s $$$$

Lean4

@[simp]
theorem span_nat_eq (s : AddSubmonoid M) : (span ℕ (s : Set M)).toAddSubmonoid = s := by
  rw [span_nat_eq_addSubmonoidClosure, s.closure_eq]

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