Theorems · Definition

Equiv.sigmaCongr

{α₁ : Type u_1} →
  {α₂ : Type u_2} →
    {β₁ : α₁ → Type u_3} → {β₂ : α₂ → Type u_4} → (f : α₁ ≃ α₂) → ((a : α₁) → β₁ a ≃ β₂ (f a)) → Sigma β₁ ≃ Sigma β₂

Transporting a sigma type through an equivalence of the base and a family of equivalences of matching fibers

Defined in

Mathlib.Logic.Equiv.Defs

Cited by

4 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound