mk_le_mk — Mathlib

English

For measurable representatives f and g with witnesses hf and hg, the induced order between the represented classes agrees with the almost everywhere order: mk f hf ≤ mk g hg iff f ≤ᵐ[μ] g.

Русский

Для представлений f и g с доказательствами измеримости hf, hg, неравенство между соответствующими классами совпадает с почти всюду существующим неравенством: mk f hf ≤ mk g hg тогда и только тогда, когда f ≤ᵐ[μ] g.

LaTeX

$$$\forall {f,g} \; (hf hg),\; (mk f hf : α \to_μ β) \le mk g hg \;\Longleftrightarrow\; f \le^\mathrm{μ}_{ae} g.$$$

Lean4

@[simp]
theorem mk_le_mk [Preorder β] {f g : α → β} (hf hg) : (mk f hf : α →ₘ[μ] β) ≤ mk g hg ↔ f ≤ᵐ[μ] g :=
  Iff.rfl

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