instContinuousInvCoe — Mathlib

English

An instance ensuring continuity of inverse/map under principal inclusions and open restrictions; the result is the continuous inverse map for the restricted product.

Русский

Существование непрерывности обратной карты при принципиальном включении и открытых ограничениях; непрерывность обратной карты ограниченного произведения.

LaTeX

$$$\\text{ContinuousInv} (\\Piʳ i, [R i, B i]_[𝓕])$ via principal inclusions$$

Lean4

@[to_additive]
instance [Π i, Inv (R i)] [∀ i, InvMemClass (S i) (R i)] [∀ i, ContinuousInv (R i)] :
    ContinuousInv (Πʳ i, [R i, B i]_[𝓕]) where
  continuous_inv := by
    rw [continuous_dom]
    intro T hT
    haveI : ContinuousInv (Πʳ i, [R i, B i]_[𝓟 T]) := isEmbedding_coe_of_principal.continuousInv fun _ ↦ rfl
    exact (continuous_inclusion hT).comp continuous_inv

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