coe_le_coe — Mathlib

English

The pointwise comparison between seminorms coincides with the order in Seminorm: (p : E → ℝ) ≤ q if and only if p ≤ q.

Русский

Пусть сравнение по точечной оценке совпадает с порядком полунорм: (p : E → ℝ) ≤ q тогда и только тогда, когда p ≤ q.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_le_coe {p q : Seminorm 𝕜 E} : (p : E → ℝ) ≤ q ↔ p ≤ q :=
  Iff.rfl

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