liftRel_mk_mk — Mathlib

English

If f and g are represented by measurable functions f and g with witnesses hf and hg respectively, then LiftRel(r, mk f hf, mk g hg) is equivalent to ∀ᵐ a ∂μ, r(f(a), g(a)).

Русский

Если f и g заданы через представления mk f hf и mk g hg, то LiftRel(r, mk f hf, mk g hg) эквивалентно ∀ᵐ a ∂μ, r(f(a), g(a)).

LaTeX

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

Lean4

theorem liftRel_mk_mk {r : β → γ → Prop} {f : α → β} {g : α → γ} {hf hg} :
    LiftRel r (mk f hf : α →ₘ[μ] β) (mk g hg) ↔ ∀ᵐ a ∂μ, r (f a) (g a) :=
  Iff.rfl

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