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>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>One M'<GOAL>ContMDiffWithinAt I I' n 1 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>s : Set M<VAR>x : M<VAR>c : M'<GOAL>SmoothWithinAt I I' (fun x => c) 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>s : Set M<VAR>x : M<VAR>One M'<GOAL>SmoothWithinAt I I' 1 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>s : Set M<VAR>x : M<VAR>Zero M'<GOAL>SmoothWithinAt I I' 0 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>n : ℕ∞<VAR>Zero M'<VAR>f : M → M'<VAR>hf : ∀ x ∈ tsupport f, ContMDiffAt I I' n f x<GOAL>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>n : ℕ∞<VAR>One M'<VAR>f : M → M'<VAR>hf : ∀ x ∈ mulTSupport f, ContMDiffAt I I' n f x<GOAL>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>One M'<VAR>x : M<VAR>hx : x ∉ mulTSupport f<VAR>n : ℕ∞<VAR>s : Set M<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>Zero M'<VAR>x : M<VAR>hx : x ∉ tsupport f<VAR>n : ℕ∞<VAR>s : Set M<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>One M'<VAR>x : M<VAR>hx : x ∉ mulTSupport f<VAR>n : ℕ∞<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>Zero M'<VAR>x : M<VAR>hx : x ∉ tsupport f<VAR>n : ℕ∞<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>n : ℕ∞<VAR>U : TopologicalSpace.Opens M<VAR>f : M → M'<VAR>x : ↥U<GOAL>ContMDiffAt I I' n (fun x => f ↑x) 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>n : ℕ∞<VAR>U : TopologicalSpace.Opens M<GOAL>ContMDiff I I n Subtype.val
<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>T2Space M<VAR>One M'<VAR>n : ℕ∞<VAR>U : TopologicalSpace.Opens M<VAR>f : ↥U → M'<VAR>supp : HasCompactMulSupport f<VAR>diff : ContMDiff I I' n f<GOAL>ContMDiff I I' n (Function.extend Subtype.val f 1)
<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>T2Space M<VAR>Zero M'<VAR>n : ℕ∞<VAR>U : TopologicalSpace.Opens M<VAR>f : ↥U → M'<VAR>supp : HasCompactSupport f<VAR>diff : ContMDiff I I' n f<GOAL>ContMDiff I I' n (Function.extend Subtype.val f 0)
<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>n : ℕ∞<VAR>U V : TopologicalSpace.Opens M<VAR>h : U ≤ V<GOAL>ContMDiff I I n (Set.inclusion h)
<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>U : TopologicalSpace.Opens M<VAR>f : M → M'<VAR>x : ↥U<GOAL>SmoothAt I I' (fun x => f ↑x) x ↔ 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>U : TopologicalSpace.Opens M<GOAL>Smooth I I Subtype.val
<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>T2Space M<VAR>Zero M'<VAR>U : TopologicalSpace.Opens M<VAR>f : ↥U → M'<VAR>supp : HasCompactSupport f<VAR>diff : Smooth I I' f<GOAL>Smooth I I' (Function.extend Subtype.val f 0)
<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>T2Space M<VAR>One M'<VAR>U : TopologicalSpace.Opens M<VAR>f : ↥U → M'<VAR>supp : HasCompactMulSupport f<VAR>diff : Smooth I I' f<GOAL>Smooth I I' (Function.extend Subtype.val f 1)
<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>U V : TopologicalSpace.Opens M<VAR>h : U ≤ V<GOAL>Smooth I I (Set.inclusion h)
<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>Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>n : WithTop ℕ<GOAL>ContMDiff I I n e
<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>Nonempty M<VAR>e : M → H<VAR>h : OpenEmbedding e<VAR>n : WithTop ℕ<GOAL>ContMDiffOn I I n (↑(OpenEmbedding.toPartialHomeomorph e h).symm) (Set.range e)
<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>Nonempty M'<VAR>e' : M' → H'<VAR>h' : OpenEmbedding e'<VAR>n : WithTop ℕ<VAR>f : M → M'<VAR>hf : ContMDiff I I' n (e' ∘ f)<GOAL>ContMDiff I I' n f
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>U : TopologicalSpace.Opens ↑X.toTopCat<VAR>x : ↥U<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>(X.evaluation x) f = 0 ↔ ↑x ∉ X.toRingedSpace.basicOpen f
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>U : TopologicalSpace.Opens ↑X.toTopCat<VAR>x : ↥U<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>(X.evaluation x) f ≠ 0 ↔ ↑x ∈ X.toRingedSpace.basicOpen f
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>x : ↑X.toTopCat<VAR>f : ↑(X.presheaf.obj (Opposite.op ⊤))<GOAL>(X.Γevaluation x) f = 0 ↔ x ∉ X.toRingedSpace.basicOpen f
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>x : ↑X.toTopCat<VAR>f : ↑(X.presheaf.obj (Opposite.op ⊤))<GOAL>(X.Γevaluation x) f ≠ 0 ↔ x ∈ X.toRingedSpace.basicOpen f
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>x : ↑X.toTopCat<GOAL>LocalRing.residue ↑(Y.presheaf.stalk (f.val.base x)) ≫ AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x = AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x ≫ LocalRing.residue ↑(X.presheaf.stalk x)
<VAR>X : AlgebraicGeometry.LocallyRingedSpace<VAR>x : ↑X.toTopCat<GOAL>AlgebraicGeometry.LocallyRingedSpace.residueFieldMap (𝟙 X) x = 𝟙 (X.residueField x)
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>Z : AlgebraicGeometry.LocallyRingedSpace<VAR>g : Y ⟶ Z<VAR>x : ↑X.toTopCat<GOAL>AlgebraicGeometry.LocallyRingedSpace.residueFieldMap (f ≫ g) x = AlgebraicGeometry.LocallyRingedSpace.residueFieldMap g (f.val.base x) ≫ AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>V : TopologicalSpace.Opens ↑Y.toTopCat<VAR>x : ↥((TopologicalSpace.Opens.map f.val.base).obj V)<GOAL>Y.evaluation ⟨f.val.base ↑x, ⋯⟩ ≫ AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f ↑x = f.val.c.app (Opposite.op V) ≫ X.evaluation x
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>V : TopologicalSpace.Opens ↑Y.toTopCat<VAR>x : ↥((TopologicalSpace.Opens.map f.val.base).obj V)<VAR>a : ↑(Y.presheaf.obj (Opposite.op V))<GOAL>(AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f ↑x) ((Y.evaluation ⟨f.val.base ↑x, ⋯⟩) a) = (X.evaluation x) ((f.val.c.app (Opposite.op V)) a)
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>x : ↑X.toTopCat<GOAL>Y.Γevaluation (f.val.base x) ≫ AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x = f.val.c.app (Opposite.op ⊤) ≫ X.Γevaluation x
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>x : ↑X.toTopCat<VAR>a : ↑(Y.presheaf.obj (Opposite.op ⊤))<GOAL>(AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x) ((Y.Γevaluation (f.val.base x)) a) = (X.Γevaluation x) ((f.val.c.app (Opposite.op ⊤)) a)
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>self : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f g : H → H'<GOAL>(∀ y ∈ s, f y = g y) → f x = g x → P f s x → P g s x
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>self : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<GOAL>e ∈ G → x ∈ e.source → P f s x → P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>self : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e' : PartialHomeomorph H' H'<GOAL>e' ∈ G' → s ⊆ f ⁻¹' e'.source → f x ∈ e'.source → P f s x → P (↑e' ∘ f) s x
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>self : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>u : Set H<VAR>f : H → H'<GOAL>IsOpen u → x ∈ u → (P f s x ↔ P f (s ∩ u) x)
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>s t : Set H<VAR>x : H<VAR>f : H → H'<VAR>hu : s =ᶠ[𝓝 x] t<GOAL>P f s x ↔ P f t x
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>s u : Set H<VAR>x : H<VAR>f : H → H'<VAR>hu : u ∈ 𝓝[s] x<GOAL>P f s x ↔ P f (s ∩ u) x
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f g : H → H'<VAR>h1 : f =ᶠ[𝓝[s] x] g<VAR>h2 : f x = g x<GOAL>P f s x ↔ P g s x
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f g : H → H'<VAR>h1 : f =ᶠ[𝓝[s] x] g<VAR>h2 : f x = g x<VAR>hP : P f s x<GOAL>P g s x
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f g : H → H'<VAR>h1 : f =ᶠ[𝓝[s] x] g<VAR>h2 : f x = g x<VAR>hP : P g s x<GOAL>P f s x
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f g : H → H'<VAR>h : f =ᶠ[𝓝 x] g<GOAL>P f s x ↔ P g s x
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f g : H → H'<VAR>h : f =ᶠ[𝓝 x] g<VAR>hP : P f s x<GOAL>P g s x
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f g : H → H'<VAR>h : f =ᶠ[𝓝 x] g<VAR>hP : P g s x<GOAL>P f s x
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e' : PartialHomeomorph H' H'<VAR>he' : e' ∈ G'<VAR>hfs : ContinuousWithinAt f s x<VAR>hxe' : f x ∈ e'.source<GOAL>P (↑e' ∘ f) s x ↔ P f s x
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ G<VAR>hxe : x ∈ e.source<GOAL>P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P f s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>P : (H → H') → Set H → H → Prop<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>self : ChartedSpace.LiftPropWithinAt P f s x<GOAL>ContinuousWithinAt f s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>P : (H → H') → Set H → H → Prop<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<GOAL>ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>P : (H → H') → Set H → H → Prop<VAR>f : M → M'<VAR>s : Set M<VAR>x : M<VAR>self : ChartedSpace.LiftPropWithinAt P f s x<GOAL>P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>P : (H → H') → Set H → H → Prop<VAR>f : M → M'<VAR>x : M<GOAL>ChartedSpace.LiftPropAt P f x ↔ ContinuousAt f x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) Set.univ (↑(chartAt H x) x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>P : (H → H') → Set H → H → Prop<VAR>f : M → M'<GOAL>ChartedSpace.LiftProp P f ↔ Continuous f ∧ ∀ (x : M), P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) Set.univ (↑(chartAt H x) x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<VAR>x : M<GOAL>ChartedSpace.LiftPropWithinAt P g Set.univ x ↔ ChartedSpace.LiftPropAt P g x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>P : (H → H') → Set H → H → Prop<VAR>g : M → M'<GOAL>ChartedSpace.LiftPropOn P g Set.univ ↔ ChartedSpace.LiftProp P g
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>P : (H → H') → Set H → H → Prop<VAR>f : H → H'<VAR>s : Set H<VAR>x : H<GOAL>ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P f s x
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>P : (H → H') → Set H → H → Prop<VAR>f : H → M'<VAR>s : Set H<VAR>x : H<GOAL>ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (↑(chartAt H' (f x)) ∘ f) s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s : Set M<VAR>x : M<VAR>f : M → H'<GOAL>ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>f : M → M'<GOAL>ChartedSpace.LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ((chartAt H x).target ∩ ↑(chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source)) (↑(chartAt H x) x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>TopologicalSpace H<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>TopologicalSpace H'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>P : (H → H') → Set H → H → Prop<VAR>s : Set M<VAR>x : M<VAR>hG : G.LocalInvariantProp G' P<VAR>g : M → H'<VAR>he : e ∈ StructureGroupoid.maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>he' : e' ∈ StructureGroupoid.maximalAtlas M G<VAR>xe' : x ∈ e'.source<GOAL>P (g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P (g ∘ ↑e'.symm) (↑e'.symm ⁻¹' s) (↑e' x)
<VAR>H : Type u_1<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>TopologicalSpace H<VAR>TopologicalSpace H'<VAR>TopologicalSpace M'<VAR>ChartedSpace H' M'<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>g : H → M'<VAR>x : H<VAR>s : Set H<VAR>hf : f ∈ StructureGroupoid.maximalAtlas M' G'<VAR>xf : g x ∈ f.source<VAR>hf' : f' ∈ StructureGroupoid.maximalAtlas M' G'<VAR>xf' : g x ∈ f'.source<VAR>hgs : ContinuousWithinAt g s x<GOAL>P (↑f ∘ g) s x ↔ P (↑f' ∘ g) s x