English
If ts is a set of topologies on G and each topology t ∈ ts has continuous inversion, then the infimum topology sInf ts also has continuous inversion.
Русский
Пусть ts — множество топологий на G; если для каждой топологии t ∈ ts операция обращения непрерывна, то и инфимума этих топологий имеет непрерывность обратной операции.
LaTeX
$$$(\forall t \in ts, \text{ContinuousInv}(G)\text{ under } t) \Rightarrow \text{ContinuousInv}(G)\text{ under } sInf(ts).$$$
Lean4
@[to_additive]
theorem continuousInv_sInf {ts : Set (TopologicalSpace G)} (h : ∀ t ∈ ts, @ContinuousInv G t _) :
@ContinuousInv G (sInf ts) _ :=
letI := sInf ts
{
continuous_inv :=
continuous_sInf_rng.2 fun t ht => continuous_sInf_dom ht (@ContinuousInv.continuous_inv G t _ (h t ht)) }
