quot_mk_eq_mk — Mathlib

English

The quotient construction for AEStronglyMeasurable functions agrees with the canonical mk construction for AEEqFun.

Русский

Квотирование для AEStronglyMeasurable функций согласуется с каноническим mk-описанием AEEqFun.

LaTeX

$$theorem quot_mk_eq_mk (f : α → β) (hf) : (Quot.mk (@Setoid.r _ | μ.aeEqSetoid β) ⟨f, hf⟩ : α →ₘ[μ] β) = mk f hf$$

Lean4

@[simp]
theorem quot_mk_eq_mk (f : α → β) (hf) : (Quot.mk (@Setoid.r _ <| μ.aeEqSetoid β) ⟨f, hf⟩ : α →ₘ[μ] β) = mk f hf :=
  rfl

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