norm_prod_le_iff — Mathlib

English

For a pair x = (x1, x2) in E × F and real r, we have ‖x‖ ≤ r if and only if both ‖x1‖ ≤ r and ‖x2‖ ≤ r. Equivalently, ‖x‖ ≤ r ⇔ ‖x1‖ ≤ r ∧ ‖x2‖ ≤ r.

Русский

Для пары x = (x1, x2) в E × F и вещественного r выполняется: ‖x‖ ≤ r тогда и только тогда, когда оба ‖x1‖ ≤ r и ‖x2‖ ≤ r. Эквивалентно: ‖x‖ ≤ r ⇔ ‖x1‖ ≤ r ∧ ‖x2‖ ≤ r.

LaTeX

$$$‖x‖ ≤ r \iff ‖x_{1}‖ ≤ r ∧ ‖x_{2}‖ ≤ r$$$

Lean4

theorem norm_prod_le_iff : ‖x‖ ≤ r ↔ ‖x.1‖ ≤ r ∧ ‖x.2‖ ≤ r :=
  max_le_iff

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