Theorems · Definition

Equiv.ofFiberEquiv

{α : Type u_13} →
  {β : Type u_14} →
    {γ : Type u_15} → {f : α → γ} → {g : β → γ} → ((c : γ) → { a // f a = c } ≃ { b // g b = c }) → α ≃ β

A family of equivalences between fibers gives an equivalence between domains.

Defined in

Mathlib.Logic.Equiv.Basic

Cited by

4 results in Mathlib

Foundations

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