mrange_lift — Mathlib

English

Every element n of M lies in the submonoid generated by itself, i.e., n ∈ powers(n).

Русский

Каждый элемент n моноида M принадлежит подмоноиду, порождаемому самим n, то есть n ∈ powers(n).

LaTeX

$$$n \\in \\mathrm{powers}(n)$$$

Lean4

@[to_additive]
theorem _root_.FreeMonoid.mrange_lift {α} (f : α → M) : mrange (FreeMonoid.lift f) = closure (Set.range f) := by
  rw [mrange_eq_map, ← FreeMonoid.closure_range_of, map_mclosure, ← Set.range_comp, FreeMonoid.lift_comp_of]

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