ae_mem_snd — Mathlib

English

If h is IdentDistrib f g μ ν, then for any measurable s, μ(f⁻¹(s)) = ν(g⁻¹(s)).

Русский

Если h — IdentDistrib f g μ ν, то для любого измеримого s верно μ(f⁻¹(s)) = ν(g⁻¹(s)).

LaTeX

$$$\forall s\ MeasurableSet s, μ(f^{-1}(s)) = ν(g^{-1}(s))$$$

Lean4

theorem ae_mem_snd (h : IdentDistrib f g μ ν) {t : Set γ} (tmeas : MeasurableSet t) (ht : ∀ᵐ x ∂μ, f x ∈ t) :
    ∀ᵐ x ∂ν, g x ∈ t :=
  h.ae_snd tmeas ht

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