English
A family of fiberwise equivalences between the fibers of two maps yields a global equivalence between the domain types.
Русский
Единая эквивалентность между фибрами двух отображений порождает глобальную эквивалентность между их областями определения.
LaTeX
$$$$ \\text{ofFiberEquiv}(e) : \\alpha \\simeq \\beta \\quad\\text{with } e: \\forall c, { a : \\alpha \\\\ f a = c } \\simeq { b : \\beta \\\\ g b = c }. $$$$
Lean4
/-- A family of equivalences between fibers gives an equivalence between domains. -/
@[simps!]
def ofFiberEquiv {α β γ} {f : α → γ} {g : β → γ} (e : ∀ c, { a // f a = c } ≃ { b // g b = c }) : α ≃ β :=
(sigmaFiberEquiv f).symm.trans <| (Equiv.sigmaCongrRight e).trans (sigmaFiberEquiv g)
