English
A group equipped with a topology coming from a group filter basis is a topological group; i.e., the group operations are continuous with respect to that topology.
Русский
Группа, оснащённая топологией, полученной из базиса фильтра группы, является топологической группой; операции группы непрерывны в этой топологии.
LaTeX
$$$(G, B.topology)$ является топологической группой.$$
Lean4
/-- If a group is endowed with a topological structure coming from a group filter basis then, it's a
topological group. -/
@[to_additive /-- If an additive group is endowed with a topological structure coming from an
additive group filter basis, then it's an additive topological group. -/
]
instance (priority := 100) isTopologicalGroup (B : GroupFilterBasis G) : @IsTopologicalGroup G B.topology _ :=
by
letI := B.topology
have basis := B.nhds_one_hasBasis
have basis' := basis.prod basis
refine IsTopologicalGroup.of_nhds_one ?_ ?_ ?_ ?_
· rw [basis'.tendsto_iff basis]
suffices ∀ U ∈ B, ∃ V W, (V ∈ B ∧ W ∈ B) ∧ ∀ a b, a ∈ V → b ∈ W → a * b ∈ U by simpa
intro U U_in
rcases mul U_in with ⟨V, V_in, hV⟩
refine ⟨V, V, ⟨V_in, V_in⟩, ?_⟩
intro a b a_in b_in
exact hV <| mul_mem_mul a_in b_in
· rw [basis.tendsto_iff basis]
intro U U_in
simpa using inv U_in
· intro x₀
rw [nhds_eq, nhds_one_eq]
rfl
· intro x₀
rw [basis.tendsto_iff basis]
intro U U_in
exact conj x₀ U_in
