value — Mathlib

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]

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