continuousMapClass — Mathlib

English

The family of continuous alternating maps forms a continuous-map class with the same input structure; i.e., ContinuousAlternatingMap R M N ι is equipped with the ContinuousMapClass structure relative to (ι → M) → N.

Русский

Множество непрерывных чередующихся отображений образует структуру класса непрерывных отображений совместную с тем же входным пространством; то есть ContinuousAlternatingMap R M N ι имеет структуру ContinuousMapClass относительно (ι → M) → N.

LaTeX

$$$\\text{ContinuousMapClass}\\big(\\mathrm{ContinuousAlternatingMap}(R,M,N,\\iota)\\big)\\big(\\iota \\to M\\big)\\, N$$$

Lean4

instance continuousMapClass : ContinuousMapClass (M [⋀^ι]→L[R] N) (ι → M) N where map_continuous f := f.cont

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