symm_apply — Mathlib

English

For any base set membership hb, the symm b y equals the cast-adjusted inverse image of (b,y) under the partial equivalence.

Русский

Для любого члена базы hb симм b y равен приведённой к нужному базовому основанию величине обратного отображения.

LaTeX

$$$e.symm b y = CAST (congr_arg E (e.symm_coe_proj hb)) (e.toPartialEquiv.symm (b,y)).2$$$

Lean4

theorem symm_apply (e : Pretrivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : F) :
    e.symm b y = cast (congr_arg E (e.symm_coe_proj hb)) (e.toPartialEquiv.symm (b, y)).2 :=
  dif_pos hb

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