smul_closure_subset — Mathlib

English

The image of a closed set under the action by an element c ∈ M contains the closure of the image of the set: c • closure s ⊆ closure (c • s).

Русский

Образ замкнутого множества под действием элемента c ⊂ M содержит замыкание образа множества: c • closure s ⊆ closure(c • s).

LaTeX

$$$ c \\cdot \\overline{s} \\subseteq \\overline{c \\cdot s} $$$

Lean4

@[to_additive]
theorem smul_closure_subset (c : M) (s : Set α) : c • closure s ⊆ closure (c • s) :=
  ((Set.mapsTo_image _ _).closure <| continuous_const_smul c).image_subset

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