coeFn_le — Mathlib

English

For simple functions f,g with values in an ordered normed group G, the ae-order comparison coincides with pointwise order.

Русский

Для простых функций f,g с значениями в упорядоченной нормированной группе G, отношение почти везде совпадает с точечным неравенством.

LaTeX

$$$(f : \alpha \to G) \le\!_{\mathrm{ae}} g \iff f \le g$$$

Lean4

theorem coeFn_le [PartialOrder G] (f g : Lp.simpleFunc G p μ) : (f : α → G) ≤ᵐ[μ] g ↔ f ≤ g := by
  rw [← Subtype.coe_le_coe, ← Lp.coeFn_le]

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