closure_range_of — Mathlib

English

In the FreeMonoid on α, the closure of the range of the embedding is the whole monoid.

Русский

В свободном моноиде на алфавите α замыкание образа вставки равно всему моноиду.

LaTeX

$$$closure(\mathrm{range} \; {\mathrm{of}}) = \top$$$

Lean4

@[to_additive]
theorem closure_range_of : closure (Set.range <| @of α) = ⊤ :=
  eq_top_iff.2 fun x _ =>
    FreeMonoid.recOn x (one_mem _) fun _x _xs hxs => mul_mem (subset_closure <| Set.mem_range_self _) hxs

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