set_smul_closure_subset — Mathlib

English

For a set s ⊆ M and t ⊆ α, the smul-closure satisfies s • closure t ⊆ closure (s • t).

Русский

Для множества s ⊆ M и t ⊆ α выполняется s • closure t ⊆ closure (s • t).

LaTeX

$$$ s \\;\\mathrm{•} \\; \\overline{t} \\subseteq \\overline{ s \\;\\mathrm{•} \\; t } $$$

Lean4

@[to_additive]
theorem set_smul_closure_subset (s : Set M) (t : Set α) : s • closure t ⊆ closure (s • t) :=
  by
  simp only [← iUnion_smul_set]
  exact
    iUnion₂_subset fun c hc ↦ (smul_closure_subset c t).trans <| closure_mono <| subset_biUnion_of_mem (u := (· • t)) hc

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