lt_def

Mathlib.Analysis.Normed.Group.Seminorm

URI: https://scilib.ai/kg/mathlib#GroupNorm.lt_def

English

For p,q in GroupNorm E, p < q if and only if (as functions) p < q pointwise.

Русский

Для p,q ∈ GroupNorm E выполняется: p < q эквивалентно тому, что p(x) < q(x) для всех x ∈ E.

LaTeX

$$$p < q \iff (p: E \to \mathbb{R}) < q$$$

Lean4

@[to_additive]
theorem lt_def : p < q ↔ (p : E → ℝ) < q :=
  Iff.rfl

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

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

Разделы

Аффилиация

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