sigmaEquivProdOfEquiv — Mathlib

English

If each fiber β1(a) is equivalent to a fixed β, then Σ a, β1(a) ≃ α × β.

Русский

Если для каждого a имеется эквивалентность β1(a) ≃ β к фиксированному β, то Σ a, β1(a) ≃ α × β.

LaTeX

$$$$ \Sigma a, \beta_1(a) \cong \alpha \times \beta. $$$$

Lean4

/-- If each fiber of a `Sigma` type is equivalent to a fixed type, then the sigma type
is equivalent to the product. -/
def sigmaEquivProdOfEquiv {α β} {β₁ : α → Sort _} (F : ∀ a, β₁ a ≃ β) : Sigma β₁ ≃ α × β :=
  (sigmaCongrRight F).trans (sigmaEquivProd α β)

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