closure_eq_mrange — Mathlib

English

For a set s in a monoid M, the submonoid closure of s equals the image of FreeMonoid.lift from s into M.

Русский

Для множества s в моноиде M замыкание под_monomoid s равно образу функтора FreeMonoid.lift от s в M.

LaTeX

$$$ \\operatorname{closure}(s) = \\operatorname{mrange}(\\mathrm{FreeMonoid.lift}(\\iota : s \\to M)) $$$

Lean4

@[to_additive]
theorem closure_eq_mrange (s : Set M) : closure s = mrange (FreeMonoid.lift ((↑) : s → M)) := by
  rw [FreeMonoid.mrange_lift, Subtype.range_coe]

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