trans — Mathlib

English

If f and g are identically distributed with μ, ν and u is a measurable map from γ to δ, then u ∘ f and u ∘ g are identically distributed with μ, ν.

Русский

Если f и g имеют одинаковое распределение с μ, ν и u — измеримое отображение из γ в δ, то u ∘ f и u ∘ g имеют одинаковое распределение с μ, ν.

LaTeX

$$$\text{IdentDistrib } f\ g\ μ\ ν \to\ \text{Measurable } u \to \text{IdentDistrib } (u \circ f)\ (u \circ g)\ μ\ ν$$$

Lean4

protected theorem trans {ρ : Measure δ} {h : δ → γ} (h₁ : IdentDistrib f g μ ν) (h₂ : IdentDistrib g h ν ρ) :
    IdentDistrib f h μ ρ :=
  { aemeasurable_fst := h₁.aemeasurable_fst
    aemeasurable_snd := h₂.aemeasurable_snd
    map_eq := h₁.map_eq.trans h₂.map_eq }

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