English
The value of a germ at a point is the common value shared by all representatives at that point.
Русский
Значение жерма в точке есть общее значение всех представителeй жерма в данной точке.
LaTeX
$$value {X α : Type*} [TopologicalSpace X] {x : X} (φ : Germ (\mathcal{N} x) α) : α$$
Lean4
/-- The value associated to a germ at a point. This is the common value
shared by all representatives at the given point. -/
def value {X α : Type*} [TopologicalSpace X] {x : X} (φ : Germ (𝓝 x) α) : α :=
Quotient.liftOn' φ (fun f ↦ f x) fun f g h ↦ by dsimp only; rw [Eventually.self_of_nhds h]