sectionOfRetractionKerToTensor_algebraMap

English

The composition of sectionOfRetractionKerToTensorAux with kerToTensor yields the desired Section to P.

Русский

Композиция sectionOfRetractionKerToTensorAux с kerToTensor даёт требуемую секцию к P.

LaTeX

$$sectionOfRetractionKerToTensor (l) hl (σ) hσ hf' hf$$

Lean4

@[simp]
theorem sectionOfRetractionKerToTensor_algebraMap (x : P) :
    sectionOfRetractionKerToTensor l hl hf' hf (algebraMap P S x) = x - l (1 ⊗ₜ .D _ _ x) :=
  sectionOfRetractionKerToTensorAux_algebraMap l hl _ _ hf' x

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