Open
Description
#+name: mfderivWithin_congr_of_eq_on_open
#+begin_src lean4
import Mathlib.Geometry.Manifold.MFDeriv.Defs
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Geometry.Manifold.AnalyticManifold
import Mathlib.Geometry.Manifold.ContMDiff.Atlas
import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
open Manifold
open SmoothManifoldWithCorners
theorem mfderivWithin_congr_of_eq_on_open
{m n : ℕ} {M N : Type*}
[TopologicalSpace M]
[ChartedSpace (EuclideanSpace ℝ (Fin m)) M]
[SmoothManifoldWithCorners (𝓡 m) M]
[TopologicalSpace N]
[ChartedSpace (EuclideanSpace ℝ (Fin n)) N]
[SmoothManifoldWithCorners (𝓡 n) N]
(f g : M → N) (s : Set M)
(ho : IsOpen s)
(he : ∀ x ∈ s, f x = g x) :
∀ x ∈ s, mfderivWithin (𝓡 m) (𝓡 n) f s x = mfderivWithin (𝓡 m) (𝓡 n) g s x := by
intros x hy
exact mfderivWithin_congr (IsOpen.uniqueMDiffWithinAt ho hy) he (he x hy)
#+end_src
#+RESULTS: mfderivWithin_congr_of_eq_on_open
: /tmp/babel-gASSFJ/lydaB7J.lean:1:0: error: unknown module prefix 'Mathlib'
:
: No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:
: /Users/dom/.elan/toolchains/leanprover--lean4---v4.14.0-rc2/lib/lean
Metadata
Metadata
Assignees
Labels
No labels