continuous_apply_apply — Mathlib

English

For fixed j and i, the map p ↦ p(j,i) is continuous from the iterated product to the fiber ρ_j,i.

Русский

Для фиксированных j, i отображение p ↦ p(j,i) непрерывно.

LaTeX

$$$$ \operatorname{Continuous}(\lambda p. p(j,i)) $$$$

Lean4

@[continuity]
theorem continuous_apply_apply {ρ : κ → ι → Type*} [∀ j i, TopologicalSpace (ρ j i)] (j : κ) (i : ι) :
    Continuous fun p : ∀ j, ∀ i, ρ j i => p j i :=
  (continuous_apply i).comp (continuous_apply j)

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