prodMap — Mathlib

English

If f: X → Y and g: Z → W are embeddings, then the product map Prod.map f g is an embedding.

Русский

Если f: X → Y и g: Z → W — вложения, то Prod.map f g — вложение.

LaTeX

$$$\IsEmbedding f \land \IsEmbedding g \Rightarrow \IsEmbedding(\mathrm{Prod.map} f g)$$$

Lean4

theorem prodMap {f : X → Y} {g : Z → W} (hf : IsEmbedding f) (hg : IsEmbedding g) : IsEmbedding (Prod.map f g)
    where
  toIsInducing := hf.isInducing.prodMap hg.isInducing
  injective := hf.injective.prodMap hg.injective

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