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 }