instOne — Mathlib

English

There is a canonical constant map 1 in ContMDiffMap giving the constant function 1.

Русский

Существуют константные отображения 1 в ContMDiffMap, задающие константную функцию 1.

LaTeX

$$$\text{One } G \Rightarrow \text{One } C^n⟮I,N;I',G⟯$$$

Lean4

@[to_additive]
protected instance instOne {G : Type*} [One G] [TopologicalSpace G] [ChartedSpace H' G] : One C^n⟮I, N; I', G⟯ :=
  ⟨ContMDiffMap.const (1 : G)⟩

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