isInducing_diag — Mathlib

English

The diagonal map from the total space of the fiberwise product into the product of the two total spaces is inducing.

Русский

Диагональное отображение из общего пространства произведения волокон в произведение двух общих пространств индукционно.

LaTeX

$$$\mathrm{IsInducing}\left(\lambda p, (\langle p.1, p.2.1\rangle, \langle p.1, p.2.2\rangle)\right)$$$

Lean4

/-- The diagonal map from the total space of the fiberwise product of two fiber bundles
`E₁`, `E₂` into `TotalSpace F₁ E₁ × TotalSpace F₂ E₂` is an inducing map. -/
theorem isInducing_diag :
    IsInducing
      (fun p ↦ (⟨p.1, p.2.1⟩, ⟨p.1, p.2.2⟩) : TotalSpace (F₁ × F₂) (E₁ ×ᵇ E₂) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂) :=
  ⟨rfl⟩

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