le_iff_le — Mathlib

English

Let x ∈ K and r ∈ ℝ. The statement (∀ w, w x ≤ r) is equivalent to (∀ φ, ‖φ x‖ ≤ r).

Русский

Пусть x ∈ K и r ∈ ℝ. Утверждение (для всех w, w x ≤ r) эквивалентно (для всех φ, ‖φ x‖ ≤ r).

LaTeX

$$$\\forall x \\\\in K, \\\\forall r \\\\in \\mathbb{R},\\\\ (\\\\forall w \\\\in \\\\mathrm{InfinitePlace}(K), w x \\\\le r) \\\\iff \\\\left(\\\\forall \\varphi \\\\colon K \\\\to+* \\\\mathbb{C}, \\\\|\\\\varphi x\\\\| \\\\le r\\\\).$$$

Lean4

theorem le_iff_le (x : K) (r : ℝ) : (∀ w : InfinitePlace K, w x ≤ r) ↔ ∀ φ : K →+* ℂ, ‖φ x‖ ≤ r :=
  ⟨fun hw φ => hw (mk φ), by rintro hφ ⟨w, ⟨φ, rfl⟩⟩; exact hφ φ⟩

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