closure_mul — Mathlib

English

In a topological group, if t is an open subset, then for every subset s of G we have closure(s) · t = s · t.

Русский

В топологической группе, если t — открытое подмножество, то для любого множества s ⊆ G выполняется \u0304s \u22C5 t = s \u22C5 t.

LaTeX

$$$\\forall S \\subseteq G,\\ \\forall T \\subseteq G,\\ (\\text{open}(T)) \\Rightarrow \\overline{S} \\cdot T = S \\cdot T$$$

Lean4

@[to_additive]
theorem closure_mul (ht : IsOpen t) (s : Set G) : closure s * t = s * t := by
  rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv, inv_inv]

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