mk_proj_snd — Mathlib

English

The second variant of the projection equality for the constructed trivialization holds: (proj x, (e x).2) = e x whenever proj x ∈ baseSet.

Русский

Вторая версия равенства проекции для сконструированной тривиализации: (proj x, (e x).2) = e x при proj x ∈ baseSet.

LaTeX

$$$\forall x \in e.source,\ (proj x, (e(x)).2) = e(x)$$$

Lean4

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

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