English
There exists a canonical order-preserving ring homomorphism from Germ(𝓝 x) E to E, i.e. an evaluation map that sends a germ to its value at x; this map is monotone with respect to the germ order.
Русский
Существует каноническое монотонное отображение колец из Germ(𝓝 x) E в E, задаваемое взятием значения гёрма в точке x; это отображение сохраняет порядок.
LaTeX
$$$\exists\phi\;\big(\phi : \operatorname{Germ}(\mathcal{N}_x) E \to E\big) \quad \text{and} \quad \phi \text{ is a monotone ring homomorphism}.$$
Lean4
/-- The map `Germ (𝓝 x) E → E` as a monotone ring homomorphism -/
def valueOrderRingHom {X E : Type*} [Semiring E] [PartialOrder E] [TopologicalSpace X] {x : X} : Germ (𝓝 x) E →+*o E
where
__ := Filter.Germ.valueRingHom
monotone' := fun φ ψ ↦ Germ.inductionOn φ fun _ ↦ Germ.inductionOn ψ fun _ h ↦ h.self_of_nhds
