ofPreimageEquiv_map — Mathlib

English

Given a fiberwise equivalence e between f^{-1}({c}) and g^{-1}({c}), the global equivalence satisfies g(ofPreimageEquiv e (a)) = f(a) for all a.

Русский

Пусть для каждого c существует эквив between f^{-1}({c}) и g^{-1}({c}). Тогда глобальная эквив согласуется с отображениями: g(ofPreimageEquiv e (a)) = f(a).

LaTeX

$$$\\forall a,\\; g(\\text{ofPreimageEquiv}(e)(a)) = f(a)$$$

Lean4

theorem ofPreimageEquiv_map {α β γ} {f : α → γ} {g : β → γ} (e : ∀ c, f ⁻¹' { c } ≃ g ⁻¹' { c }) (a : α) :
    g (ofPreimageEquiv e a) = f a :=
  Equiv.ofFiberEquiv_map e a

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