ext

Mathlib.Topology.UniformSpace.Equiv

URI: https://scilib.ai/kg/mathlib#UniformEquiv.ext

English

Two uniform equivalences are equal if they agree pointwise on all arguments.

Русский

Два UniformEquiv равны, если их значения совпадают на всех точках.

LaTeX

$$extensionality: ∀ x, h x = h' x → h = h'$$

Lean4

@[ext]
theorem ext {h h' : α ≃ᵤ β} (H : ∀ x, h x = h' x) : h = h' :=
  toEquiv_injective <| Equiv.ext H

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru