inv — Mathlib

English

If f and g are identically distributed, then their pointwise inverses are identically distributed, given the inverse operation is defined.

Русский

Если f и g распределены одинаково, то их обратные значения по точкам тоже распределены одинаково.

LaTeX

$$$\forall f,g,\ \text{IdentDistrib } f g\ \mu\ nu \Rightarrow \text{IdentDistrib}(f^{-1}) (g^{-1})\ mu \nu$$$

Lean4

@[to_additive]
theorem inv [Inv γ] [MeasurableInv γ] (h : IdentDistrib f g μ ν) : IdentDistrib f⁻¹ g⁻¹ μ ν :=
  h.comp measurable_inv

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