closure_eq_image_prod — Mathlib

English

The closure of s equals the image of lists of elements from s under the product map; equivalently, elements of closure(s) are exactly finite products of elements of s.

Русский

Замыкание s равно образу списков элементов из s под отображением произведения; то есть элементы closure(s) есть ровно конечные произведения элементов из s.

LaTeX

$$$ \\operatorname{closure}(s) = \\mathrm{List.prod} '' \\{ l : \\mathrm{List} M \\mid \\forall x \\in l, x \\in s \\} $$$

Lean4

@[to_additive]
theorem closure_eq_image_prod (s : Set M) : (closure s : Set M) = List.prod '' {l : List M | ∀ x ∈ l, x ∈ s} :=
  by
  rw [closure_eq_mrange, coe_mrange, ← Set.range_list_map_coe, ← Set.range_comp]
  exact congrArg _ (funext <| FreeMonoid.lift_apply _)

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