lt_def

Mathlib.Analysis.Seminorm

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

English

The relation p < q between seminorms is equivalent to p ≤ q and there exists x with p(x) < q(x).

Русский

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

LaTeX

$$$ p < q \iff p \le q \ \\land \ \exists x, p(x) < q(x) $$$

Lean4

theorem lt_def {p q : Seminorm 𝕜 E} : p < q ↔ p ≤ q ∧ ∃ x, p x < q x :=
  @Pi.lt_def _ _ _ p q

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

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

Разделы

Аффилиация

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