English
The product of two dense inducings is a dense inducing map.
Русский
Произведение двух плотных индуциирующих отображений является плотным индуциирующим отображением.
LaTeX
$$$ \\text{IsDenseInducing} (\\text{Prod.map } e_1 e_2) $$$
Lean4
/-- The product of two dense inducings is a dense inducing -/
protected theorem prodMap [TopologicalSpace γ] [TopologicalSpace δ] {e₁ : α → β} {e₂ : γ → δ} (de₁ : IsDenseInducing e₁)
(de₂ : IsDenseInducing e₂) : IsDenseInducing (Prod.map e₁ e₂)
where
toIsInducing := de₁.isInducing.prodMap de₂.isInducing
dense := de₁.dense.prodMap de₂.dense