span_nat_eq_addSubmonoidClosure — Mathlib

English

For an additive commutative monoid M, the span over natural numbers of s, viewed as a set, equals the AddSubmonoid-closure of s.

Русский

Для аддитивной абелевой моноиды M порождение по натуральным числам от множества s равно замыканию AddSubmonoid от s.

LaTeX

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

Lean4

theorem span_nat_eq_addSubmonoidClosure (s : Set M) : (span ℕ s).toAddSubmonoid = AddSubmonoid.closure s :=
  by
  refine Eq.symm (AddSubmonoid.closure_eq_of_le subset_span ?_)
  apply
    (OrderIso.to_galoisConnection (AddSubmonoid.toNatSubmodule (M := M)).symm).l_le (a := span ℕ s) (b :=
      AddSubmonoid.closure s)
  rw [span_le]
  exact AddSubmonoid.subset_closure

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