English
If s is open, then s·t is open for any t; this is a direct corollary of IsOpenMap via image under scalar multiplication.
Русский
Если s открыто, то s·t открыто для любого t; следует из открытости отображения под действием смулю.
LaTeX
$$$\\text{IsOpen}(s) \\Rightarrow \\text{IsOpen}(s\\cdot t).$$$
Lean4
@[to_additive]
theorem mul_closure (hs : IsOpen s) (t : Set G) : s * closure t = s * t :=
by
refine (mul_subset_iff.2 fun a ha b hb => ?_).antisymm (mul_subset_mul_left subset_closure)
rw [mem_closure_iff] at hb
have hbU : b ∈ s⁻¹ * {a * b} := ⟨a⁻¹, Set.inv_mem_inv.2 ha, a * b, rfl, inv_mul_cancel_left _ _⟩
obtain ⟨_, ⟨c, hc, d, rfl : d = _, rfl⟩, hcs⟩ := hb _ hs.inv.mul_right hbU
exact ⟨c⁻¹, hc, _, hcs, inv_mul_cancel_left _ _⟩
