comp — Mathlib

English

If f and g are almost everywhere equal with respect to μ, then f and g are identically distributed with respect to μ and μ.

Русский

Если f и g равны почти всюду по отношению к μ, то они идентично распределены по μ.

LaTeX

$$$f =^{\text{a.e.}}_{\mu} g \implies \text{IdentDistrib } f\ g\ μ\ μ$$$

Lean4

protected theorem comp {u : γ → δ} (h : IdentDistrib f g μ ν) (hu : Measurable u) : IdentDistrib (u ∘ f) (u ∘ g) μ ν :=
  h.comp_of_aemeasurable hu.aemeasurable

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