prodMap — Mathlib

English

Embedding of a subtype inside a dense embedding is itself dense.

Русский

Вложение подмножества внутрь плотного вложения образует плотное вложение.

LaTeX

$$$IsDenseEmbedding.subtypeEmb p e \\text{ is dense embedding for any } p, e$$$

Lean4

/-- The product of two dense embeddings is a dense embedding. -/
protected theorem prodMap {e₁ : α → β} {e₂ : γ → δ} (de₁ : IsDenseEmbedding e₁) (de₂ : IsDenseEmbedding e₂) :
    IsDenseEmbedding fun p : α × γ => (e₁ p.1, e₂ p.2)
    where
  toIsDenseInducing := de₁.isDenseInducing.prodMap de₂.isDenseInducing
  injective := de₁.injective.prodMap de₂.injective

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