smul_set_closure_subset — Mathlib

English

The product of closures is contained in the closure of the product: closure K • closure L ⊆ closure(K • L).

Русский

Произведение замыканий вложено в замыкание произведения: closure K • closure L ⊆ closure(K • L).

LaTeX

$$$closure(K) \cdot closure(L) \subseteq closure(K \cdot L)$$$

Lean4

@[to_additive]
theorem smul_set_closure_subset (K : Set M) (L : Set X) : closure K • closure L ⊆ closure (K • L) :=
  Set.smul_subset_iff.2 fun _x hx _y hy ↦
    map_mem_closure₂ continuous_smul hx hy fun _a ha _b hb ↦ Set.smul_mem_smul ha hb

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