mk_proj_snd' — Mathlib

English

Equivalently, the evaluation of the constructed trivialization equals the evaluation of the original open partial homeomorphism.

Русский

Эквивалентно: значение сконструированной тривиализации равно значению исходного открытого частичного гомеоморфизма.

LaTeX

$$$\big(\mathrm{Trivialization.mk}\ e\ i\ j\ k\ l\ m\big)(x) = e(x)$$$

Lean4

theorem mk_proj_snd' (ex : proj x ∈ e.baseSet) : (proj x, (e x).2) = e x :=
  Prod.ext (e.coe_fst' ex).symm rfl

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