continuousInv — Mathlib

English

For the function space ∀ i, C(i), the inverse is continuous pointwise, i.e., (i ↦ f(i))^{-1} is continuous in i given each C(i) has continuous inverse.

Русский

Для пространства функций ∀ i, C(i) инверсия выполняется по каждой координате. Если каждый C(i) имеет непрерывную инверссию, то пространство функций ∀ i, C(i) имеет непрерывную обратную карту по координатам.

LaTeX

$$$\\\\operatorname{ContinuousInv} (\\\\forall i, C(i)).$$$

Lean4

@[to_additive]
instance continuousInv {C : ι → Type*} [∀ i, TopologicalSpace (C i)] [∀ i, Inv (C i)] [∀ i, ContinuousInv (C i)] :
    ContinuousInv (∀ i, C i) where continuous_inv := continuous_pi fun i => (continuous_apply i).inv

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