prod — Mathlib

English

Under completeness and separation hypotheses, the two-step extension after map equals the direct extension of the composed map.

Русский

При полноте и разделимости два шага продолжения после отображения эквивалентен прямому продолжению композиции отображения.

LaTeX

$$$ \text{(hf hg)} \to pkg'.extend f \circ map g = pkg.extend (f \circ g) $$$

Lean4

/-- Products of completions -/
protected def prod : AbstractCompletion (α × β)
    where
  space := hatα × hatβ
  coe p := ⟨ι p.1, ι' p.2⟩
  uniformStruct := inferInstance
  complete := inferInstance
  separation := inferInstance
  isUniformInducing := IsUniformInducing.prod pkg.isUniformInducing pkg'.isUniformInducing
  dense := pkg.dense.prodMap pkg'.dense

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