le_def

Mathlib.Analysis.Seminorm

URI: https://scilib.ai/kg/mathlib#Seminorm.le_def

English

The relation p ≤ q between seminorms is equivalent to the pointwise inequality p(x) ≤ q(x) for all x.

Русский

Отношение p ≤ q между полунормами эквивалентно неравенству p(x) ≤ q(x) для всех x.

LaTeX

$$$ p \le q \iff \forall x, p(x) \le q(x) $$$

Lean4

theorem le_def {p q : Seminorm 𝕜 E} : p ≤ q ↔ ∀ x, p x ≤ q x :=
  Iff.rfl

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

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

Разделы

Аффилиация

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