Theorems · Definition

Equiv.piCongrRight

{α : Sort u_1} →
  {β₁ : α → Sort u_9} → {β₂ : α → Sort u_10} → ((a : α) → β₁ a ≃ β₂ a) → ((a : α) → β₁ a) ≃ ((a : α) → β₂ a)

A family of equivalences ∀ a, β₁ a ≃ β₂ a generates an equivalence between ∀ a, β₁ a and ∀ a, β₂ a.

Defined in

Mathlib.Logic.Equiv.Basic

Cited by

15 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound