ext — Mathlib

English

Two open maps are equal if they agree at every point; extensionality principle for ContinuousOpenMap.

Русский

Два открытых отображения равны, если их значения совпадают в каждой точке; принцип эквивалентности для ContinuousOpenMap.

LaTeX

$$$\forall f,g : α \toCO β,\ (\forall a, f\,a = g\,a) \Rightarrow f = g.$$$

Lean4

@[ext]
theorem ext {f g : α →CO β} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

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