coe_le_coe — Mathlib

English

The order on GroupNorm corresponds to the order on the underlying functions; i.e., (p ≤ q) iff ((p: E → ℝ) ≤ q).

Русский

Порядок над GroupNorm эквивалентен порядку на соответствующих функциях: p ≤ q эквивалентно (p: E → ℝ) ≤ q.

LaTeX

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

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_le_coe : (p : E → ℝ) ≤ q ↔ p ≤ q :=
  Iff.rfl

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