prodMap — Mathlib

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

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