coe_symm_of_notMem — Mathlib

English

The symmetric of a pretrivialization outside its base set is identically zero as a fiber map.

Русский

За пределами базового множества симметрический отображатель равен нулю на каждом волокне.

LaTeX

$$$e.symm\_b = 0\;\text{when } b\notin e.baseSet$$$

Lean4

theorem coe_symm_of_notMem (e : Pretrivialization F (π F E)) {b : B} (hb : b ∉ e.baseSet) : (e.symm b : F → E b) = 0 :=
  funext fun _ => dif_neg hb

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