symm_coe_proj — Mathlib

English

For a member b of the base set of e', the first component of e'.toFun' applied to (proj, y) equals b.

Русский

Для члена базового множества e' первая координата e'.toFun' (proj, y) равна b.

LaTeX

$$$\forall b\in e'.baseSet\,\forall y:\,E b,\ (e'.toFun' { proj := b, snd := y }).1 = b$$$

Lean4

theorem symm_coe_proj {x : B} {y : F} (e' : Pretrivialization F (π F E)) (h : x ∈ e'.baseSet) :
    (e'.toPartialEquiv.symm (x, y)).1 = x :=
  e'.proj_symm_apply' h

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