cCompInsert — Mathlib

English

Composition with Cube.insertAt acts as a continuous map between function spaces.

Русский

Сложение с Cube.insertAt образует непрерывное отображение между пространствами функций.

LaTeX

$$cCompInsert(i) : C(C(I^N, X), C(I × I^{ j // j ≠ i }, X))$$

Lean4

/-- Composition with `Cube.insertAt` as a continuous map. -/
abbrev cCompInsert (i : N) : C(C(I^N, X), C(I × I^{ j // j ≠ i }, X)) :=
  ⟨fun f => f.comp (Cube.insertAt i), (toContinuousMap <| Cube.insertAt i).continuous_precomp⟩

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