English
The previous statement (prodUnits) asserts a homeomorphism between units of a product and the product of units; its auxiliary lemmas establish continuity of the forward and inverse maps.
Русский
Предыдущее утверждение (prodUnits) утверждает гомеоморфизм между единицами произведения и произведением единиц; вспомогательные леммы устанавливают непрерывность прямого и обратного отображений.
LaTeX
$$$ \\text{Homeomorph } (\\alpha \\times \\beta)^{\\times} \\cong_{top} \\alpha^{\\times} \\times \\beta^{\\times} $$$
Lean4
/-- The topological group isomorphism between the units of a product of two monoids, and the product
of the units of each monoid. -/
@[to_additive prodAddUnits /-- The topological group isomorphism between the additive units of a product of two
additive monoids, and the product of the additive units of each additive monoid. -/
]
def _root_.Homeomorph.prodUnits : (α × β)ˣ ≃ₜ αˣ × βˣ
where
continuous_toFun :=
(continuous_fst.units_map (MonoidHom.fst α β)).prodMk (continuous_snd.units_map (MonoidHom.snd α β))
continuous_invFun :=
Units.continuous_iff.2
⟨continuous_val.fst'.prodMk continuous_val.snd', continuous_coe_inv.fst'.prodMk continuous_coe_inv.snd'⟩
toEquiv := MulEquiv.prodUnits.toEquiv
