sigmaEquivProd — Mathlib

English

A Sigma type with a constant fiber is equivalent to the product α × β.

Русский

Тип сигма с константным волокном эквивалентен произведению α × β.

LaTeX

$$$$(\Sigma _: \alpha, \beta) \cong \alpha \times \beta.$$$$

Lean4

/-- `Sigma` type with a constant fiber is equivalent to the product. -/
@[simps (attr := mfld_simps, grind =) apply symm_apply]
def sigmaEquivProd (α β : Type*) : (Σ _ : α, β) ≃ α × β
    where
  toFun a := ⟨a.1, a.2⟩
  invFun a := ⟨a.1, a.2⟩

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