le_def — Mathlib

English

Let p and q be NonarchAddGroupSeminorms on an additive group E. The order on seminorms is defined pointwise by evaluating at each element, so p ≤ q if and only if p(x) ≤ q(x) for every x ∈ E.

Русский

Пусть p и q — NonarchAddGroupSeminorm на аддитивной группе E. Порядок на семинормax задаётся по значениям на каждом элементе: p ≤ q тогда и только тогда, когда p(x) ≤ q(x) для каждого x ∈ E.

LaTeX

$$$ p \le q \iff \forall x : E,\; p(x) \le q(x) $$$

Lean4

theorem le_def : p ≤ q ↔ (p : E → ℝ) ≤ q :=
  Iff.rfl

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