English
The symmetric coordinate change map between trivializations is ContMDiffOn on its target.
Русский
Переход симметричен по гладкости.
LaTeX
$$$$\\text{ContMDiffOn }(\\text{e}.toOpenPartialHomeomorph.symm) \\; \\text{ на } \\text{e.target}. $$$$
Lean4
/-- Smoothness of a `C^n` section at `x₀` within a set `a` can be determined
using any trivialisation whose `baseSet` contains `x₀`. -/
theorem contMDiffWithinAt_section {s : ∀ x, E x} (a : Set B) {x₀ : B}
{e : Trivialization F (Bundle.TotalSpace.proj : Bundle.TotalSpace F E → B)} [MemTrivializationAtlas e]
(hx₀ : x₀ ∈ e.baseSet) :
ContMDiffWithinAt IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) a x₀ ↔
ContMDiffWithinAt IB 𝓘(𝕜, F) n (fun x ↦ (e ⟨x, s x⟩).2) a x₀ :=
by
rw [e.contMDiffWithinAt_iff]
· change ContMDiffWithinAt IB IB n id a x₀ ∧ _ ↔ _
simp [contMDiffWithinAt_id]
· rwa [mem_source]
