sectionCotangent_zero_of_notMem_range

English

If i is not in the range of P.map, then the corresponding basis element maps to zero under the section.

Русский

Если i не принадлежит диапазону отображения P.map, то соответствующий элемент базы отображается в ноль через секцию.

LaTeX

$$sectionCotangent P (P.cotangentSpaceBasis i) = 0 whenever i ∉ Set.range P.map$$

Lean4

theorem sectionCotangent_zero_of_notMem_range (i : ι) (hi : i ∉ Set.range P.map) :
    (sectionCotangent P) (P.cotangentSpaceBasis i) = 0 := by
  classical
  contrapose hi
  rw [sectionCotangent_eq_iff] at hi
  simp only [Basis.repr_self, map_zero, Pi.zero_apply, Finsupp.single_apply] at hi
  grind

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