liftRel_iff_coeFn — Mathlib

English

If f and g are μ-equivalence representatives, then LiftRel(r, f, g) is equivalent to r applied pointwise to f(a) and g(a) for almost every a.

Русский

Если f и g являются представителями эквивалентности по μ, то LiftRel(r, f, g) эквивалентно тому, что для почти всех a выполняется r(f(a), g(a)).

LaTeX

$$$\operatorname{LiftRel}(r, f, g) \;\Longleftrightarrow\; \forall^{\mathrm{ae}} a \;\partial\mu,\; r\bigl(f(a), g(a)\bigr).$$$

Lean4

theorem liftRel_iff_coeFn {r : β → γ → Prop} {f : α →ₘ[μ] β} {g : α →ₘ[μ] γ} : LiftRel r f g ↔ ∀ᵐ a ∂μ, r (f a) (g a) :=
  by rw [← liftRel_mk_mk (hf := f.aestronglyMeasurable) (hg := g.aestronglyMeasurable), mk_coeFn, mk_coeFn]

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