toTrivialization_apply — Mathlib

English

If h is evenly covered, then the associated trivialization identifies the fiber with its image via the base mapping.

Русский

Связанная тривиализация устанавливает идентификацию волокна с образом через базовую карту.

LaTeX

$$$(h.toTrivialization x).2 = \\langle x, rfl \\rangle$$$

Lean4

theorem toTrivialization_apply {x : E} [Nonempty I] (h : IsEvenlyCovered f (f x) I) :
    (h.toTrivialization x).2 = ⟨x, rfl⟩ :=
  h.fiberHomeomorph.symm.injective <| by
    simp [toTrivialization, toTrivialization', dif_pos h.2.choose_spec.1, fiberHomeomorph]

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