mk_coeFn — Mathlib

English

The equivalence-class constructor applied to a function gives back the original AEEqFun element.

Русский

Операция вложения функции в класс эквивалентности возвращает исходный элемент AEEqFun.

LaTeX

$$$\\operatorname{mk}(f,f\\!:\\!aestronglyMeasurable) = f$$$

Lean4

@[simp]
theorem mk_coeFn (f : α →ₘ[μ] β) : mk f f.aestronglyMeasurable = f :=
  by
  conv_lhs => simp only [cast]
  split_ifs with h
  · exact Classical.choose_spec h |>.symm
  conv_rhs => rw [← Quotient.out_eq' f]
  rw [← mk, mk_eq_mk]
  exact (AEStronglyMeasurable.ae_eq_mk _).symm

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