toProd — Mathlib

English

A trivial bundle is naturally equivalent to the product B × F; explicitly, TotalSpace F (const B → F) is isomorphic to B × F.

Русский

Тривиальный биндинг естественным образом эквивалентен произведению B × F; точно, общие пространства тривиального биндинга из F по B изоморфны B × F.

LaTeX

$$$$(TotalSpace F (\text{const } B \\to F)) \cong B \times F.$$$$

Lean4

/-- A trivial bundle is equivalent to the product `B × F`. -/
@[simps (attr := mfld_simps)]
def toProd (B F : Type*) : (TotalSpace F fun _ : B => F) ≃ B × F
    where
  toFun x := (x.1, x.2)
  invFun x := ⟨x.1, x.2⟩

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