instOneTangentSpaceRealModelWithCornersSelf

English

There is a canonical element named 1 in the tangent space of Real with corners at each point.

Русский

Для каждой точки множества Real с углами существует канонический элемент 1 в касательном пространстве.

LaTeX

$$$\text{One in } \mathrm{TangentSpace}(\mathcal{I}(\mathbb{R}, \mathbb{R}), x)$ for each x$$

Lean4

instance (x : ℝ) : One (TangentSpace 𝓘(ℝ) x) where one := (1 : ℝ)

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