tprod_inv — Mathlib

English

In a complete topological group, the infinite product of inverses equals the inverse of the infinite product: ∏' f(b)^{-1} = (∏' f(b))^{-1}.

Русский

В полной топологической группе бесконечное произведение обратных элементов равно обратному произведению: ∏ f(b)^{-1} = (∏ f(b))^{-1}.

LaTeX

$$$\prod'_{L} b, f(b)^{-1} = (\prod'_{L} b, f(b))^{-1}.$$$

Lean4

@[to_additive]
theorem tprod_inv : ∏'[L] b, (f b)⁻¹ = (∏'[L] b, f b)⁻¹ :=
  ((Homeomorph.inv α).isClosedEmbedding.map_tprod f (g := MulEquiv.inv α)).symm

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