symm — Mathlib

English

If f and g are identically distributed with respect to μ and ν, then the pair (g, f) is identically distributed with respect to ν and μ.

Русский

Если f и g идентично распределены относительно μ и ν, то пара (g, f) имеет идентично распределение относительно ν и μ.

LaTeX

$$$\text{IdentDistrib } f\ g\ μ\ ν \to\ \text{IdentDistrib } g\ f\ ν\ μ$$$

Lean4

protected theorem symm (h : IdentDistrib f g μ ν) : IdentDistrib g f ν μ :=
  { aemeasurable_fst := h.aemeasurable_snd
    aemeasurable_snd := h.aemeasurable_fst
    map_eq := h.map_eq.symm }

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