continuousInv_iInf — Mathlib

English

If ts' is a family of topological spaces indexed by i and each has continuous inversion, then the infimum topology ⨅ i, ts' i also has continuous inversion.

Русский

Пусть ts' — семейство топологий, индексируемых i; если каждая имеет непрерывную инверсию, то инфимума этих топологий также имеет непрерывность инверсии.

LaTeX

$$$(\forall i, \text{ContinuousInv } G\text{ under } ts'(i)) \Rightarrow \text{ContinuousInv } G\text{ under } \bigwedge_i ts'(i).$$$

Lean4

@[to_additive]
theorem continuousInv_iInf {ts' : ι' → TopologicalSpace G} (h' : ∀ i, @ContinuousInv G (ts' i) _) :
    @ContinuousInv G (⨅ i, ts' i) _ := by
  rw [← sInf_range]
  exact continuousInv_sInf (Set.forall_mem_range.mpr h')

Похожие утверждения