English
If c ∈ G₀ is nonzero, then closure(c · s) = c · closure(s) in appropriate spaces, with zero handled separately.
Русский
Если c ∈ G₀ не нулевое, то closure(c · s) = c · closure(s) в подходящих пространствах; ноль обрабатывается отдельно.
LaTeX
$$$\text{closure}(c \cdot s) = c \cdot \text{closure}(s)$$$
Lean4
theorem closure_smul₀ {E} [Zero E] [MulActionWithZero G₀ E] [TopologicalSpace E] [T1Space E] [ContinuousConstSMul G₀ E]
(c : G₀) (s : Set E) : closure (c • s) = c • closure s :=
by
rcases eq_or_ne c 0 with (rfl | hc)
· rcases eq_empty_or_nonempty s with (rfl | hs)
· simp
· rw [zero_smul_set hs, zero_smul_set hs.closure]
exact closure_singleton
· exact closure_smul₀' hc s
