English
If μ is nonzero, the constant-ae representative equals the constant function everywhere, up to almost-everywhere equality; in particular, for nonzero μ, the cast equals the actual constant function at almost every point.
Русский
Если μ не равна нулю, то константный ae-представитель эквивалентен константной функции повсеместно, почти всюду совпадая.
LaTeX
$$$[\NeZero μ] \; (\operatorname{const}(b) : α \to_μ β) =^\mathrm{ae}_{μ} (\text{Function.const}(α, b))$$$
Lean4
/-- If the measure is nonzero, we can strengthen `coeFn_const` to get an equality. -/
@[simp]
theorem coeFn_const_eq [NeZero μ] (b : β) (x : α) : (const α b : α →ₘ[μ] β) x = b :=
by
simp only [cast]
split_ifs with h
case neg => exact h.elim ⟨b, rfl⟩
have := Classical.choose_spec h
set b' := Classical.choose h
simp_rw [const, mk_eq_mk, EventuallyEq, ← const_def, eventually_const] at this
rw [Function.const, this]
