ofFiberEquiv_map — Mathlib

English

In the fiber-equivalence construction, the image of a given a under the global equivalence corresponds to the original f(a).

Русский

При построении глобальной эквивалентности по фибрами образ элемента a совпадает с исходной f(a).

LaTeX

$$$$ g(\\mathrm{ofFiberEquiv}(e)\\; a) = f(a). $$$$

Lean4

theorem ofFiberEquiv_map {α β γ} {f : α → γ} {g : β → γ} (e : ∀ c, { a // f a = c } ≃ { b // g b = c }) (a : α) :
    g (ofFiberEquiv e a) = f a :=
  (_ : { b // g b = _ }).property

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