ext

Mathlib.Analysis.Normed.Group.Seminorm

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

English

Extensionality for NonarchAddGroupNorm: two elements are equal if they agree on every x ∈ E.

Русский

Экстенсиональность NonarchAddGroupNorm: два элемента равны, если согласованы на каждом x ∈ E.

LaTeX

$$(∀ x:E, p x = q x) → p = q$$

Lean4

@[ext]
theorem ext : (∀ x, p x = q x) → p = q :=
  DFunLike.ext p q

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

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

Разделы

Аффилиация

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