English
The map from germs to E is a linear map: value_ℓ is a K-linear map with value_ℓ(φ) = value(φ).
Русский
Отображение жерма в E является линейным отображением: value_ℓ — это K-подобное линейное отображение с value_ℓ(φ) = value(φ).
LaTeX
$$def valueₗ {X 𝕜 E : Type*} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace X] {x : X} : Germ (𝓝 x) E →ₗ[𝕜] E$$
Lean4
/-- The map `Germ (𝓝 x) E → E` into a `𝕜`-module `E` as a `𝕜`-linear map -/
def valueₗ {X 𝕜 E : Type*} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace X] {x : X} :
Germ (𝓝 x) E →ₗ[𝕜] E where
__ := Filter.Germ.valueAddHom
map_smul' := fun _ φ ↦ Germ.inductionOn φ fun _ ↦ rfl
