English
In a group with continuous multiplication, any open subgroup is closed as a subset.
Русский
В группе с непрерывным умножением любая открытая подгруппа замкнута как множество.
LaTeX
$$$\forall G\, [\mathrm{ContinuousMul}(G)],\ \forall U \in \mathrm{OpenSubgroup}(G):\ \mathrm{IsClosed}(U)$$$
Lean4
@[to_additive]
theorem isClosed [ContinuousMul G] (U : OpenSubgroup G) : IsClosed (U : Set G) :=
by
apply isOpen_compl_iff.1
refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ⟨(fun y ↦ y * x⁻¹) ⁻¹' U, ?_, ?_, ?_⟩
· refine fun u hux hu ↦ hx ?_
simp only [Set.mem_preimage, SetLike.mem_coe] at hux hu ⊢
convert U.mul_mem (U.inv_mem hux) hu
simp
· exact U.isOpen.preimage (continuous_mul_right _)
· simp [one_mem]
