coeFn_mk — Mathlib

English

Compatibility of SMul action with the FiniteMeasure structure: the scalar action is well-behaved with respect to the underlying measure.

Русский

Совместимость скалярного действия SMul с конструкцией FiniteMeasure: действие скаляра корректно по отношению к базовой мере.

LaTeX

$$instSMul congruence$$

Lean4

theorem coeFn_mk (μ : Measure Ω) (hμ) : DFunLike.coe (F := FiniteMeasure Ω) ⟨μ, hμ⟩ = fun s ↦ (μ s).toNNReal :=
  rfl

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