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 }