ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<GOAL>SmoothWithinAt I I' f s x ↔ ∀ (n : ℕ), ContMDiffWithinAt I I' (↑n) f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<GOAL>SmoothAt I I' f x ↔ ∀ (n : ℕ), ContMDiffAt I I' (↑n) f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<GOAL>SmoothOn I I' f s ↔ ∀ (n : ℕ), ContMDiffOn I I' (↑n) f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<GOAL>Smooth I I' f ↔ ∀ (n : ℕ), ContMDiff I I' (↑n) f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<GOAL>ContMDiffWithinAt I I' n f s x ↔ ∀ (m : ℕ), ↑m ≤ n → ContMDiffWithinAt I I' (↑m) f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s t : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>hf : ContMDiffWithinAt I I' n f s x<VAR>hts : s ∈ 𝓝[t] x<GOAL>ContMDiffWithinAt I I' n f t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s t : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>hf : ContMDiffWithinAt I I' n f s x<VAR>hts : t ⊆ s<GOAL>ContMDiffWithinAt I I' n f t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s t : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>hst : 𝓝[s] x = 𝓝[t] x<GOAL>ContMDiffWithinAt I I' n f s x ↔ ContMDiffWithinAt I I' n f t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<GOAL>ContMDiffWithinAt I I' n f (insert x s) x ↔ ContMDiffWithinAt I I' n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>h : ContMDiffWithinAt I I' n f s x<GOAL>ContMDiffWithinAt I I' n f (insert x s) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>hf : ContMDiffAt I I' n f x<GOAL>ContMDiffWithinAt I I' n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>hf : SmoothAt I I' f x<GOAL>SmoothWithinAt I I' f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s t : Set M<VAR>n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>hts : t ⊆ s<GOAL>ContMDiffOn I I' n f t
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>n : ℕ∞<VAR>hf : ContMDiff I I' n f<GOAL>ContMDiffOn I I' n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>hf : Smooth I I' f<GOAL>SmoothOn I I' f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s t : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>ht : t ∈ 𝓝[s] x<GOAL>ContMDiffWithinAt I I' n f (s ∩ t) x ↔ ContMDiffWithinAt I I' n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s t : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>ht : t ∈ 𝓝 x<GOAL>ContMDiffWithinAt I I' n f (s ∩ t) x ↔ ContMDiffWithinAt I I' n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>h : ContMDiffWithinAt I I' n f s x<VAR>ht : s ∈ 𝓝 x<GOAL>ContMDiffAt I I' n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>h : SmoothWithinAt I I' f s x<VAR>ht : s ∈ 𝓝 x<GOAL>SmoothAt I I' f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>h : ContMDiffOn I I' n f s<VAR>hx : s ∈ 𝓝 x<GOAL>ContMDiffAt I I' n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>h : SmoothOn I I' f s<VAR>hx : s ∈ 𝓝 x<GOAL>SmoothAt I I' f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>e : PartialHomeomorph M H<VAR>f : M → M'<VAR>s : Set M<VAR>n : ℕ∞<VAR>he : e ∈ SmoothManifoldWithCorners.maximalAtlas I M<VAR>hs : s ⊆ e.source<GOAL>ContMDiffOn I I' n f s ↔ ContMDiffOn 𝓘(𝕜, E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>SmoothManifoldWithCorners I' M'<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ<GOAL>ContMDiffWithinAt I I' (↑n) f s x ↔ ∃ u ∈ 𝓝[insert x s] x, ContMDiffOn I I' (↑n) f u
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>SmoothManifoldWithCorners I' M'<VAR>f : M → M'<VAR>x : M<VAR>n : ℕ<GOAL>ContMDiffAt I I' (↑n) f x ↔ ∃ u ∈ 𝓝 x, ContMDiffOn I I' (↑n) f u
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>SmoothManifoldWithCorners I' M'<VAR>f : M → M'<VAR>x : M<VAR>n : ℕ<GOAL>ContMDiffAt I I' (↑n) f x ↔ ∀ᶠ (x' : M) in 𝓝 x, ContMDiffAt I I' (↑n) f x'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f f₁ : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>h : ContMDiffWithinAt I I' n f s x<VAR>h₁ : ∀ y ∈ s, f₁ y = f y<VAR>hx : f₁ x = f x<GOAL>ContMDiffWithinAt I I' n f₁ s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f f₁ : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>h₁ : ∀ y ∈ s, f₁ y = f y<VAR>hx : f₁ x = f x<GOAL>ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f f₁ : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>h : ContMDiffWithinAt I I' n f s x<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>ContMDiffWithinAt I I' n f₁ s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f f₁ : M → M'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>ContMDiffWithinAt I I' n f₁ s x ↔ ContMDiffWithinAt I I' n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f f₁ : M → M'<VAR>x : M<VAR>n : ℕ∞<VAR>h : ContMDiffAt I I' n f x<VAR>h₁ : f₁ =ᶠ[𝓝 x] f<GOAL>ContMDiffAt I I' n f₁ x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f f₁ : M → M'<VAR>x : M<VAR>n : ℕ∞<VAR>h₁ : f₁ =ᶠ[𝓝 x] f<GOAL>ContMDiffAt I I' n f₁ x ↔ ContMDiffAt I I' n f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f f₁ : M → M'<VAR>s : Set M<VAR>n : ℕ∞<VAR>h : ContMDiffOn I I' n f s<VAR>h₁ : ∀ y ∈ s, f₁ y = f y<GOAL>ContMDiffOn I I' n f₁ s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f f₁ : M → M'<VAR>s : Set M<VAR>n : ℕ∞<VAR>h₁ : ∀ y ∈ s, f₁ y = f y<GOAL>ContMDiffOn I I' n f₁ s ↔ ContMDiffOn I I' n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f f₁ : M → M'<VAR>s s₁ : Set M<VAR>n : ℕ∞<VAR>hf : ContMDiffOn I I' n f s<VAR>h₁ : ∀ y ∈ s₁, f₁ y = f y<VAR>hs : s₁ ⊆ s<GOAL>ContMDiffOn I I' n f₁ s₁
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>s : Set M<VAR>n : ℕ∞<VAR>h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' n f (s ∩ u)<GOAL>ContMDiffOn I I' n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>E' : Type u_5<VAR>NormedAddCommGroup E'<VAR>NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>f : M → M'<VAR>n : ℕ∞<VAR>h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' n f u<GOAL>ContMDiff I I' n f
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<VAR>S : Set σ<GOAL>S ⊆ M.εClosure S
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<GOAL>M.εClosure ∅ = ∅
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<GOAL>M.εClosure Set.univ = Set.univ
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<VAR>S : Set σ<VAR>s : σ<VAR>a : α<GOAL>s ∈ M.stepSet S a ↔ ∃ t ∈ S, s ∈ M.εClosure (M.step t (some a))
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<VAR>a : α<GOAL>M.stepSet ∅ a = ∅
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<VAR>S : Set σ<GOAL>M.evalFrom S [] = M.εClosure S
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<VAR>S : Set σ<VAR>a : α<GOAL>M.evalFrom S [a] = M.stepSet (M.εClosure S) a
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<VAR>S : Set σ<VAR>x : List α<VAR>a : α<GOAL>M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<VAR>x : List α<GOAL>M.evalFrom ∅ x = ∅
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<GOAL>M.eval [] = M.εClosure M.start
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<VAR>a : α<GOAL>M.eval [a] = M.stepSet (M.εClosure M.start) a
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<VAR>x : List α<VAR>a : α<GOAL>M.eval (x ++ [a]) = M.stepSet (M.eval x) a
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<VAR>start : Set σ<GOAL>M.toNFA.evalFrom (M.εClosure start) = M.evalFrom start
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<GOAL>M.toNFA.accepts = M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : εNFA α σ<VAR>Fintype σ<VAR>x : List α<VAR>hx : x ∈ M.accepts<VAR>hlen : Fintype.card (Set σ) ≤ x.length<GOAL>∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card (Set σ) ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<VAR>S : Set σ<GOAL>M.toεNFA.εClosure S = S
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<VAR>start : Set σ<GOAL>M.toεNFA.evalFrom start = M.evalFrom start
<VAR>α : Type u<VAR>σ : Type v<VAR>M : NFA α σ<GOAL>M.toεNFA.accepts = M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>s : σ<VAR>a : Option α<GOAL>εNFA.step 0 s a = ∅
<VAR>α : Type u<VAR>σ : Type v<VAR>s : σ<VAR>a : Option α<GOAL>εNFA.step 1 s a = ∅
<VAR>α : Type u<VAR>σ : Type v<GOAL>εNFA.start 0 = ∅
<VAR>α : Type u<VAR>σ : Type v<GOAL>εNFA.start 1 = Set.univ
<VAR>α : Type u<VAR>σ : Type v<GOAL>εNFA.accept 0 = ∅
<VAR>α : Type u<VAR>σ : Type v<GOAL>εNFA.accept 1 = Set.univ
<VAR>α : Type u_1<VAR>l m : Language α<GOAL>l + m = l ∪ m
<VAR>α : Type u_1<VAR>l m : Language α<GOAL>l * m = Set.image2 (fun x x_1 => x ++ x_1) l m
<VAR>α : Type u_1<VAR>l : Language α<GOAL>l∗ = {x | ∃ L, x = L.join ∧ ∀ y ∈ L, y ∈ l}
<VAR>α : Type u_1<VAR>l m : Language α<VAR>h : ∀ (x : List α), x ∈ l ↔ x ∈ m<GOAL>l = m
<VAR>α : Type u_1<VAR>x : List α<GOAL>x ∉ 0
<VAR>α : Type u_1<VAR>x : List α<GOAL>x ∈ 1 ↔ x = []
<VAR>α : Type u_1<GOAL>[] ∈ 1
<VAR>α : Type u_1<VAR>l m : Language α<VAR>x : List α<GOAL>x ∈ l + m ↔ x ∈ l ∨ x ∈ m
<VAR>α : Type u_1<VAR>l m : Language α<VAR>x : List α<GOAL>x ∈ l * m ↔ ∃ a ∈ l, ∃ b ∈ m, a ++ b = x
<VAR>α : Type u_1<VAR>l m : Language α<VAR>a b : List α<GOAL>a ∈ l → b ∈ m → a ++ b ∈ l * m
<VAR>α : Type u_1<VAR>l : Language α<VAR>x : List α<GOAL>x ∈ l∗ ↔ ∃ L, x = L.join ∧ ∀ y ∈ L, y ∈ l
<VAR>α : Type u_1<VAR>l : Language α<VAR>L : List (List α)<VAR>h : ∀ y ∈ L, y ∈ l<GOAL>L.join ∈ l∗
<VAR>α : Type u_1<VAR>l : Language α<GOAL>[] ∈ l∗