mdifferentiable_zeroSection — Mathlib

English

The zero section is differentiable as a bundle morphism in the MDifferentiable sense.

Русский

Нулевая секция является дифференцируемым морфизмом расслоения в смысле MDifferentiable.

LaTeX

$$$$MDifferentiable IB (IB.prod 𝓘(\mathbb{k}, F)) (zeroSection F E).$$$$

Lean4

theorem mdifferentiable_zeroSection : MDifferentiable IB (IB.prod 𝓘(𝕜, F)) (zeroSection F E) :=
  by
  intro x
  unfold zeroSection
  rw [mdifferentiableAt_section]
  apply (mdifferentiableAt_const (c := 0)).congr_of_eventuallyEq
  filter_upwards [(trivializationAt F E x).open_baseSet.mem_nhds (mem_baseSet_trivializationAt F E x)] with y hy using
    congr_arg Prod.snd <| (trivializationAt F E x).zeroSection 𝕜 hy

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