English
Let ts be a set of topologies on G; the infimum inherits a topological group structure if each ts(t) makes G a topological group.
Русский
Пусть ts множество топологий на G; инфимума наследует топологическую группу, если каждая ts(t) делает G топологической группой.
LaTeX
$$$ IsTopologicalGroup(G, sInf ts) $$$
Lean4
@[to_additive]
theorem topologicalGroup_sInf {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, @IsTopologicalGroup G t _) :
@IsTopologicalGroup G (sInf ts) _ :=
letI := sInf ts
{ toContinuousInv := @continuousInv_sInf _ _ _ fun t ht => @IsTopologicalGroup.toContinuousInv G t _ <| h t ht
toContinuousMul := @continuousMul_sInf _ _ _ fun t ht => @IsTopologicalGroup.toContinuousMul G t _ <| h t ht }
