coe_lt_coe — Mathlib

English

The strict order between GroupNorm structures matches the strict order of their function realizations: (p: E → ℝ) < q iff p < q.

Русский

Строгий порядок между GroupNorm соответствует строгому порядку их отображений: (p: E → ℝ) < q ⇔ p < q.

LaTeX

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

Lean4

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

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