smul_closure_orbit_subset — Mathlib

English

For any c ∈ M and x ∈ α, the smul of the closure of the orbit of x is contained in the closure of the orbit: c • closure (orbit M x) ⊆ closure (orbit M x).

Русский

Для любого c ∈ M и x ∈ α выполняется c • closure (orbit M x) ⊆ closure (orbit M x).

LaTeX

$$$ c \\cdot \\overline{\\mathrm{orbit}(M, x)} \\subseteq \\overline{\\mathrm{orbit}(M, x)} $$$

Lean4

@[to_additive]
theorem smul_closure_orbit_subset (c : M) (x : α) : c • closure (MulAction.orbit M x) ⊆ closure (MulAction.orbit M x) :=
  (smul_closure_subset c _).trans <| closure_mono <| MulAction.smul_orbit_subset _ _

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