continuous

Mathlib.Topology.Algebra.ContinuousAffineMap

URI: https://scilib.ai/kg/mathlib#ContinuousAffineMap.continuous

English

The constant map q ∈ Q is the affine map from P to Q sending every point to q.

Русский

Константная карта q ∈ Q является аффинной картой, отправляющей каждую точку p ∈ P в q.

LaTeX

$$$\forall p \in P:\, \text{const}(q)(p) = q$$$

Lean4

@[continuity]
protected theorem continuous (f : P →ᴬ[R] Q) : Continuous f :=
  f.2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru