sigmaCongr — Mathlib

English

An equivalence e: α1 ≃ α2 yields an equivalence between Σ a1, β (e a) and Σ a2, β a.

Русский

Эквивалентность e: α1 ≃ α2 порождает эквивалентность между Σ a1, β (e a) и Σ a2, β a.

LaTeX

$$$${\text{sigmaCongrLeft }(e): (\Sigma a_1, \beta (e a)) \cong \Sigma a_2, \beta a.}$$$$

Lean4

/-- Transporting a sigma type through an equivalence of the base and a family of equivalences
of matching fibers -/
def sigmaCongr {α₁ α₂} {β₁ : α₁ → Sort _} {β₂ : α₂ → Sort _} (f : α₁ ≃ α₂) (F : ∀ a, β₁ a ≃ β₂ (f a)) :
    Sigma β₁ ≃ Sigma β₂ :=
  (sigmaCongrRight F).trans (sigmaCongrLeft f)

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