coeFn_le — Mathlib

English

The coeFn_le lemma states that the pointwise order between the coerced functions equals the almost everywhere order of the original representatives: (f: α → β) ≤ᵐ g iff f ≤ g in the ae-representation.

Русский

Лемма coeFn_le утверждает, что понижение функций до обычной функции сохраняет отношение ≤ почти всюду: (f: α → β) ≤ᵐ g эквивалентно f ≤ g в ae-представлении.

LaTeX

$$$\bigl(f : α \to β\bigr) \le^{}_{\mathrm{μ}} g \;\Longleftrightarrow\; f \le g,$$$

Lean4

@[simp, norm_cast]
theorem coeFn_le [Preorder β] {f g : α →ₘ[μ] β} : (f : α → β) ≤ᵐ[μ] g ↔ f ≤ g :=
  liftRel_iff_coeFn.symm

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