ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>↑(fs.toFun (fs.ind x hx)) x = 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>x ∈ Function.support ↑(fs.toFun (fs.ind x hx))
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>x ∈ (chartAt H (fs.c (fs.ind x hx))).source
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>x : M<VAR>hx : x ∈ s<GOAL>x ∈ (extChartAt I (fs.c (fs.ind x hx))).source
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>T2Space M<VAR>f : SmoothBumpCovering ι I M s<VAR>U : M → Set M<GOAL>(f.toBumpCovering.IsSubordinate fun i => U (f.c i)) ↔ f.IsSubordinate U
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>T2Space M<VAR>i : ι<VAR>x : M<GOAL>(fs.toSmoothPartitionOfUnity i) x = ↑(fs.toFun i) x * ∏ᶠ (j : ι) (_ : WellOrderingRel j i), (1 - ↑(fs.toFun j) x)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>T2Space M<VAR>i : ι<VAR>x : M<VAR>t : Finset ι<VAR>ht : ∀ (j : ι), WellOrderingRel j i → ↑(fs.toFun j) x ≠ 0 → j ∈ t<GOAL>(fs.toSmoothPartitionOfUnity i) x = ↑(fs.toFun i) x * ∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) t, (1 - ↑(fs.toFun j) x)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>T2Space M<VAR>i : ι<VAR>x : M<GOAL>∃ t, ⇑(fs.toSmoothPartitionOfUnity i) =ᶠ[𝓝 x] ↑(fs.toFun i) * ∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) t, (1 - ↑(fs.toFun j))
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>T2Space M<VAR>i : ι<VAR>x : M<VAR>h : ↑(fs.toFun i) x = 0<GOAL>(fs.toSmoothPartitionOfUnity i) x = 0
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>T2Space M<VAR>i : ι<GOAL>Function.support ⇑(fs.toSmoothPartitionOfUnity i) ⊆ Function.support ↑(fs.toFun i)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>T2Space M<VAR>f : SmoothBumpCovering ι I M s<VAR>U : M → Set M<VAR>h : f.IsSubordinate U<GOAL>f.toSmoothPartitionOfUnity.IsSubordinate fun i => U (f.c i)
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>s : Set M<VAR>fs : SmoothBumpCovering ι I M s<VAR>T2Space M<VAR>x : M<GOAL>∑ᶠ (i : ι), (fs.toSmoothPartitionOfUnity i) x = 1 - ∏ᶠ (i : ι), (1 - ↑(fs.toFun i) x)
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<GOAL>∃ f, Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : M), f x ∈ Set.Icc 0 1
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>NormalSpace M<VAR>SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<GOAL>∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 0) ∧ (∀ᶠ (x : M) in 𝓝ˢ t, f x = 1) ∧ ∀ (x : M), f x ∈ Set.Icc 0 1
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>NormalSpace M<VAR>SigmaCompactSpace M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>hd : s ⊆ interior t<GOAL>∃ f, (∀ᶠ (x : M) in 𝓝ˢ s, f x = 1) ∧ (∀ x ∉ t, f x = 0) ∧ ∀ (x : M), f x ∈ Set.Icc 0 1
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>SigmaCompactSpace M<VAR>s : Set M<VAR>hs : IsClosed s<VAR>U : ι → Set M<VAR>ho : ∀ (i : ι), IsOpen (U i)<VAR>hU : s ⊆ ⋃ i, U i<GOAL>∃ f, f.IsSubordinate U
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>SigmaCompactSpace M<VAR>s : Set M<VAR>hs : IsClosed s<GOAL>∃ f, f.IsSubordinate fun x => (chartAt H ↑x).source
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>T2Space M<VAR>SigmaCompactSpace M<GOAL>∃ f, f.IsSubordinate fun x => (chartAt H x).source
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>SigmaCompactSpace M<VAR>T2Space M<VAR>t : M → Set F<VAR>n : ℕ∞<VAR>ht : ∀ (x : M), Convex ℝ (t x)<VAR>Hloc : ∀ (x : M), ∃ U ∈ 𝓝 x, ∃ g, ContMDiffOn I 𝓘(ℝ, F) n g U ∧ ∀ y ∈ U, g y ∈ t y<GOAL>∃ g, ∀ (x : M), g x ∈ t x
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>SigmaCompactSpace M<VAR>T2Space M<VAR>t : M → Set F<VAR>ht : ∀ (x : M), Convex ℝ (t x)<VAR>Hloc : ∀ (x : M), ∃ U ∈ 𝓝 x, ∃ g, SmoothOn I 𝓘(ℝ, F) g U ∧ ∀ y ∈ U, g y ∈ t y<GOAL>∃ g, ∀ (x : M), g x ∈ t x
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>SigmaCompactSpace M<VAR>T2Space M<VAR>t : M → Set F<VAR>ht : ∀ (x : M), Convex ℝ (t x)<VAR>Hloc : ∀ (x : M), ∃ c, ∀ᶠ (y : M) in 𝓝 x, c ∈ t y<GOAL>∃ g, ∀ (x : M), g x ∈ t x
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_1<VAR>EMetricSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>SigmaCompactSpace M<VAR>K U : ι → Set M<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<GOAL>∃ δ, (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, EMetric.closedBall x (ENNReal.ofReal (δ x)) ⊆ U i
<VAR>ι : Type uι<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_1<VAR>MetricSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>SigmaCompactSpace M<VAR>K U : ι → Set M<VAR>hK : ∀ (i : ι), IsClosed (K i)<VAR>hU : ∀ (i : ι), IsOpen (U i)<VAR>hKU : ∀ (i : ι), K i ⊆ U i<VAR>hfin : LocallyFinite K<GOAL>∃ δ, (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedBall x (δ x) ⊆ U i
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>s : Set H<VAR>hs : IsOpen s<GOAL>∃ f, Function.support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ Set.range f ⊆ Set.Icc 0 1
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>SigmaCompactSpace M<VAR>T2Space M<VAR>s : Set M<VAR>hs : IsOpen s<GOAL>∃ f, Function.support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ ∀ (x : M), 0 ≤ f x
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>SigmaCompactSpace M<VAR>T2Space M<VAR>s t : Set M<VAR>hs : IsOpen s<VAR>ht : IsClosed t<VAR>h : t ⊆ s<GOAL>∃ f, Smooth I 𝓘(ℝ, ℝ) f ∧ Set.range f ⊆ Set.Icc 0 1 ∧ Function.support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>FiniteDimensional ℝ E<VAR>H : Type uH<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>SigmaCompactSpace M<VAR>T2Space M<VAR>s t : Set M<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<GOAL>∃ f, Smooth I 𝓘(ℝ, ℝ) f ∧ Set.range f ⊆ Set.Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>x : ↥U<VAR>h : IsUnit ((X.presheaf.germ x) f)<GOAL>∃ V i, ∃ (_ : ↑x ∈ V), IsUnit ((X.presheaf.map i.op) f)
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>h : ∀ (x : ↥U), IsUnit ((X.presheaf.germ x) f)<GOAL>IsUnit f
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>x : ↥U<GOAL>↑x ∈ X.basicOpen f ↔ IsUnit ((X.presheaf.germ x) f)
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>f : ↑(X.presheaf.obj (Opposite.op ⊤))<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ X.basicOpen f ↔ IsUnit ((X.presheaf.germ ⟨x, ⋯⟩) f)
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>X.basicOpen f ≤ U
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>IsUnit ((X.presheaf.map (CategoryTheory.homOfLE ⋯).op) f)
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ<VAR>i : U ⟶ V<VAR>f : ↑(X.presheaf.obj U)<GOAL>X.basicOpen ((X.presheaf.map i) f) = Opposite.unop V ⊓ X.basicOpen f
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ<VAR>i : U ⟶ V<VAR>CategoryTheory.IsIso i<VAR>f : ↑(X.presheaf.obj U)<GOAL>X.basicOpen ((X.presheaf.map i) f) = X.basicOpen f
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<VAR>f g : ↑(X.presheaf.obj (Opposite.op U))<GOAL>X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>n : ℕ<VAR>h : 0 < n<GOAL>X.basicOpen (f ^ n) = X.basicOpen f
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>hf : IsUnit f<GOAL>X.basicOpen f = U
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<VAR>s : Set ↑(X.presheaf.obj (Opposite.op U))<GOAL>IsClosed (X.zeroLocus s)
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>X.zeroLocus {f} = (X.basicOpen f).carrierᶜ
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<GOAL>X.zeroLocus ∅ = Set.univ
<VAR>X : AlgebraicGeometry.RingedSpace<VAR>U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace<VAR>s : Set ↑(X.presheaf.obj (Opposite.op U))<VAR>x : ↑↑X.toPresheafedSpace<GOAL>x ∈ X.zeroLocus s ↔ ∀ f ∈ s, x ∉ X.basicOpen 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' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>f : M → M'<VAR>g : M → N'<VAR>hf : ContMDiffWithinAt I I' n f s x<VAR>hg : ContMDiffWithinAt I J' n g s x<GOAL>ContMDiffWithinAt I (I'.prod J') n (fun x => (f x, g 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>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>s : Set M<VAR>x : M<VAR>n : ℕ∞<VAR>f : M → E'<VAR>g : M → F'<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, E') n f s x<VAR>hg : ContMDiffWithinAt I 𝓘(𝕜, F') n g s x<GOAL>ContMDiffWithinAt I 𝓘(𝕜, E' × F') n (fun x => (f x, g 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' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>x : M<VAR>n : ℕ∞<VAR>f : M → M'<VAR>g : M → N'<VAR>hf : ContMDiffAt I I' n f x<VAR>hg : ContMDiffAt I J' n g x<GOAL>ContMDiffAt I (I'.prod J') n (fun x => (f x, g x)) 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>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>x : M<VAR>n : ℕ∞<VAR>f : M → E'<VAR>g : M → F'<VAR>hf : ContMDiffAt I 𝓘(𝕜, E') n f x<VAR>hg : ContMDiffAt I 𝓘(𝕜, F') n g x<GOAL>ContMDiffAt I 𝓘(𝕜, E' × F') n (fun x => (f x, g x)) 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' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>s : Set M<VAR>n : ℕ∞<VAR>f : M → M'<VAR>g : M → N'<VAR>hf : ContMDiffOn I I' n f s<VAR>hg : ContMDiffOn I J' n g s<GOAL>ContMDiffOn I (I'.prod J') n (fun x => (f x, g x)) 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>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>s : Set M<VAR>n : ℕ∞<VAR>f : M → E'<VAR>g : M → F'<VAR>hf : ContMDiffOn I 𝓘(𝕜, E') n f s<VAR>hg : ContMDiffOn I 𝓘(𝕜, F') n g s<GOAL>ContMDiffOn I 𝓘(𝕜, E' × F') n (fun x => (f x, g x)) 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' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>n : ℕ∞<VAR>f : M → M'<VAR>g : M → N'<VAR>hf : ContMDiff I I' n f<VAR>hg : ContMDiff I J' n g<GOAL>ContMDiff I (I'.prod J') n fun x => (f x, g 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>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>n : ℕ∞<VAR>f : M → E'<VAR>g : M → F'<VAR>hf : ContMDiff I 𝓘(𝕜, E') n f<VAR>hg : ContMDiff I 𝓘(𝕜, F') n g<GOAL>ContMDiff I 𝓘(𝕜, E' × F') n fun x => (f x, g 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' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>s : Set M<VAR>x : M<VAR>f : M → M'<VAR>g : M → N'<VAR>hf : SmoothWithinAt I I' f s x<VAR>hg : SmoothWithinAt I J' g s x<GOAL>SmoothWithinAt I (I'.prod J') (fun x => (f x, g 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>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>s : Set M<VAR>x : M<VAR>f : M → E'<VAR>g : M → F'<VAR>hf : SmoothWithinAt I 𝓘(𝕜, E') f s x<VAR>hg : SmoothWithinAt I 𝓘(𝕜, F') g s x<GOAL>SmoothWithinAt I 𝓘(𝕜, E' × F') (fun x => (f x, g 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' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>x : M<VAR>f : M → M'<VAR>g : M → N'<VAR>hf : SmoothAt I I' f x<VAR>hg : SmoothAt I J' g x<GOAL>SmoothAt I (I'.prod J') (fun x => (f x, g x)) 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>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>x : M<VAR>f : M → E'<VAR>g : M → F'<VAR>hf : SmoothAt I 𝓘(𝕜, E') f x<VAR>hg : SmoothAt I 𝓘(𝕜, F') g x<GOAL>SmoothAt I 𝓘(𝕜, E' × F') (fun x => (f x, g x)) 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' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>TopologicalSpace N'<VAR>ChartedSpace G' N'<VAR>s : Set M<VAR>f : M → M'<VAR>g : M → N'<VAR>hf : SmoothOn I I' f s<VAR>hg : SmoothOn I J' g s<GOAL>SmoothOn I (I'.prod J') (fun x => (f x, g x)) 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>F' : Type u_14<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜 F'<VAR>s : Set M<VAR>f : M → E'<VAR>g : M → F'<VAR>hf : SmoothOn I 𝓘(𝕜, E') f s<VAR>hg : SmoothOn I 𝓘(𝕜, F') g s<GOAL>SmoothOn I 𝓘(𝕜, E' × F') (fun x => (f x, g x)) s