closure_mul_le — Mathlib

English

For any S, the closure of S raised to a positive NPow is below the closure of S; in particular, closure(S^n) ≤ closure S for n ≠ 0.

Русский

Замыкание S в степени n с n ≠ 0 ⊆ замыкание S.

LaTeX

$$$ closure (S ^ n) \leq closure S \; (n \neq 0) $$$

Lean4

@[to_additive]
theorem closure_mul_le (S T : Set M) : closure (S * T) ≤ closure S ⊔ closure T :=
  sInf_le fun _x ⟨_s, hs, _t, ht, hx⟩ =>
    hx ▸
      (closure S ⊔ closure T).mul_mem (SetLike.le_def.mp le_sup_left <| subset_closure hs)
        (SetLike.le_def.mp le_sup_right <| subset_closure ht)

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