ofPreimageEquiv — Mathlib

English

A family of fiberwise equivalences e_c : f^{-1}({c}) ≃ g^{-1}({c}) for all c induces a global equivalence α ≃ β between the domains.

Русский

Функции-переключатели по каждому волокну порождают глобальную эквиваленцию между доменами.

LaTeX

$$(∀ c, f^{-1}({c}) ≃ g^{-1}({c})) ⇒ α ≃ β$$

Lean4

/-- A family of equivalences between preimages of points gives an equivalence between domains. -/
@[simps!]
def ofPreimageEquiv {α β γ} {f : α → γ} {g : β → γ} (e : ∀ c, f ⁻¹' { c } ≃ g ⁻¹' { c }) : α ≃ β :=
  Equiv.ofFiberEquiv e

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