ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<GOAL>ContinuousAt γ t₀
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>hγ : IsIntegralCurve γ v<GOAL>Continuous γ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>t : ℝ<VAR>ht : t ∈ s<VAR>hsrc : γ t ∈ (extChartAt I (γ t₀)).source<GOAL>HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<GOAL>∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt (↑(extChartAt I (γ t₀)) ∘ γ) ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t))) t
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s : Set ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>dt : ℝ<GOAL>IsIntegralCurveOn (γ ∘ fun x => x + dt) v {t | t + dt ∈ s}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s : Set ℝ<VAR>dt : ℝ<GOAL>IsIntegralCurveOn γ v s ↔ IsIntegralCurveOn (γ ∘ fun x => x + dt) v {t | t + dt ∈ s}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>dt : ℝ<GOAL>IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ dt : ℝ<GOAL>IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>hγ : IsIntegralCurve γ v<VAR>dt : ℝ<GOAL>IsIntegralCurve (γ ∘ fun x => x + dt) v
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>dt : ℝ<GOAL>IsIntegralCurve γ v ↔ IsIntegralCurve (γ ∘ fun x => x + dt) v
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s : Set ℝ<VAR>hγ : IsIntegralCurveOn γ v s<VAR>a : ℝ<GOAL>IsIntegralCurveOn (γ ∘ fun x => x * a) (a • v) {t | t * a ∈ s}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s : Set ℝ<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>IsIntegralCurveOn γ v s ↔ IsIntegralCurveOn (γ ∘ fun x => x * a) (a • v) {t | t * a ∈ s}
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ a : ℝ<VAR>ha : a ≠ 0<GOAL>IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ fun x => x * a) (a • v) (t₀ / a)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>hγ : IsIntegralCurve γ v<VAR>a : ℝ<GOAL>IsIntegralCurve (γ ∘ fun x => x * a) (a • v)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>a : ℝ<VAR>ha : a ≠ 0<GOAL>IsIntegralCurve γ v ↔ IsIntegralCurve (γ ∘ fun x => x * a) (a • v)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>v : (x : M) → TangentSpace I x<VAR>x : M<VAR>h : v x = 0<GOAL>IsIntegralCurve (fun x_1 => x) v
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>hv : ContMDiffAt I I.tangent 1 (fun x => { proj := x, snd := v x }) x₀<VAR>hx : I.IsInteriorPoint x₀<GOAL>∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v t₀
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<VAR>x₀ : M<VAR>BoundarylessManifold I M<VAR>hv : ContMDiffAt I I.tangent 1 (fun x => { proj := x, snd := v x }) x₀<GOAL>∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v t₀
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<VAR>hγt₀ : I.IsInteriorPoint (γ t₀)<VAR>hv : ContMDiffAt I I.tangent 1 (fun x => { proj := x, snd := v x }) (γ t₀)<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>hγ' : IsIntegralCurveAt γ' v t₀<VAR>h : γ t₀ = γ' t₀<GOAL>γ =ᶠ[𝓝 t₀] γ'
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<VAR>BoundarylessManifold I M<VAR>hv : ContMDiffAt I I.tangent 1 (fun x => { proj := x, snd := v x }) (γ t₀)<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>hγ' : IsIntegralCurveAt γ' v t₀<VAR>h : γ t₀ = γ' t₀<GOAL>γ =ᶠ[𝓝 t₀] γ'
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<VAR>T2Space M<VAR>a b : ℝ<VAR>ht₀ : t₀ ∈ Set.Ioo a b<VAR>hγt : ∀ t ∈ Set.Ioo a b, I.IsInteriorPoint (γ t)<VAR>hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }<VAR>hγ : IsIntegralCurveOn γ v (Set.Ioo a b)<VAR>hγ' : IsIntegralCurveOn γ' v (Set.Ioo a b)<VAR>h : γ t₀ = γ' t₀<GOAL>Set.EqOn γ γ' (Set.Ioo a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<VAR>T2Space M<VAR>a b : ℝ<VAR>BoundarylessManifold I M<VAR>ht₀ : t₀ ∈ Set.Ioo a b<VAR>hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }<VAR>hγ : IsIntegralCurveOn γ v (Set.Ioo a b)<VAR>hγ' : IsIntegralCurveOn γ' v (Set.Ioo a b)<VAR>h : γ t₀ = γ' t₀<GOAL>Set.EqOn γ γ' (Set.Ioo a b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<VAR>T2Space M<VAR>hγt : ∀ (t : ℝ), I.IsInteriorPoint (γ t)<VAR>hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }<VAR>hγ : IsIntegralCurve γ v<VAR>hγ' : IsIntegralCurve γ' v<VAR>h : γ t₀ = γ' t₀<GOAL>γ = γ'
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>t₀ : ℝ<VAR>T2Space M<VAR>BoundarylessManifold I M<VAR>hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }<VAR>hγ : IsIntegralCurve γ v<VAR>hγ' : IsIntegralCurve γ' v<VAR>h : γ t₀ = γ' t₀<GOAL>γ = γ'
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>T2Space M<VAR>a b : ℝ<VAR>BoundarylessManifold I M<VAR>hγ : IsIntegralCurve γ v<VAR>hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }<VAR>heq : γ a = γ b<GOAL>Function.Periodic γ (a - b)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>H : Type u_2<VAR>TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>TopologicalSpace M<VAR>ChartedSpace H M<VAR>SmoothManifoldWithCorners I M<VAR>γ : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>T2Space M<VAR>BoundarylessManifold I M<VAR>hγ : IsIntegralCurve γ v<VAR>hv : ContMDiff I I.tangent 1 fun x => { proj := x, snd := v x }<GOAL>Xor' (∃ T > 0, Function.Periodic γ T) (Function.Injective γ)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimits C<VAR>J : Type v<VAR>CategoryTheory.Category.{v, v} J<VAR>F : CategoryTheory.Functor J (AlgebraicGeometry.SheafedSpace C)<VAR>c : CategoryTheory.Limits.Cocone F<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>x : ↑↑c.pt.toPresheafedSpace<GOAL>∃ i y, (c.ι.app i).base y = x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasLimits C<VAR>J : Type v<VAR>CategoryTheory.Category.{v, v} J<VAR>F : CategoryTheory.Functor J (AlgebraicGeometry.SheafedSpace C)<VAR>x : ↑↑(CategoryTheory.Limits.colimit F).toPresheafedSpace<GOAL>∃ i y, (CategoryTheory.Limits.colimit.ι F i).base y = x
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.coequalizer f.val g.val).toPresheafedSpace<VAR>s : ↑((CategoryTheory.Limits.coequalizer f.val g.val).presheaf.obj (Opposite.op U))<GOAL>⇑(CategoryTheory.Limits.coequalizer.π f.val g.val).base ⁻¹' (⇑(CategoryTheory.Limits.coequalizer.π f.val g.val).base '' (AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen f g U s).carrier) = (AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen f g U s).carrier
<VAR>X Y : AlgebraicGeometry.LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>U : TopologicalSpace.Opens ↑↑(CategoryTheory.Limits.coequalizer f.val g.val).toPresheafedSpace<VAR>s : ↑((CategoryTheory.Limits.coequalizer f.val g.val).presheaf.obj (Opposite.op U))<GOAL>IsOpen (⇑(CategoryTheory.Limits.coequalizer.π f.val g.val).base '' (AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen f g U s).carrier)
<VAR>X Y : AlgebraicGeometry.RingedSpace<VAR>f g : X ⟶ Y<VAR>H : f = g<VAR>x : ↑↑X.toPresheafedSpace<VAR>h : IsLocalRingHom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x)<GOAL>IsLocalRingHom (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap g x)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c x y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hx : x ≠ c<VAR>hy : y ≠ c<GOAL>EuclideanGeometry.inversion c R x ∈ AffineSubspace.perpBisector c (EuclideanGeometry.inversion c R y) ↔ dist x y = dist y c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c x y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hy : y ≠ c<GOAL>EuclideanGeometry.inversion c R x ∈ AffineSubspace.perpBisector c (EuclideanGeometry.inversion c R y) ↔ dist x y = dist y c ∧ x ≠ c
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hy : y ≠ c<GOAL>EuclideanGeometry.inversion c R ⁻¹' ↑(AffineSubspace.perpBisector c (EuclideanGeometry.inversion c R y)) = Metric.sphere y (dist y c) \ {c}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hy : y ≠ c<GOAL>EuclideanGeometry.inversion c R ⁻¹' ↑(AffineSubspace.perpBisector c y) = Metric.sphere (EuclideanGeometry.inversion c R y) (R ^ 2 / dist y c) \ {c}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hy : y ≠ c<GOAL>EuclideanGeometry.inversion c R '' ↑(AffineSubspace.perpBisector c y) = Metric.sphere (EuclideanGeometry.inversion c R y) (R ^ 2 / dist y c) \ {c}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hy : y ≠ c<GOAL>EuclideanGeometry.inversion c R ⁻¹' Metric.sphere y (dist y c) = insert c ↑(AffineSubspace.perpBisector c (EuclideanGeometry.inversion c R y))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hy : y ≠ c<GOAL>EuclideanGeometry.inversion c R '' Metric.sphere y (dist y c) = insert c ↑(AffineSubspace.perpBisector c (EuclideanGeometry.inversion c R y))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c : P<VAR>R : ℝ<VAR>p : AffineSubspace ℝ P<VAR>hp : c ∈ p<GOAL>Set.MapsTo (EuclideanGeometry.inversion c R) ↑p ↑p
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>c : P<VAR>R : ℝ<VAR>p : AffineSubspace ℝ P<VAR>hR : R ≠ 0<VAR>hp : c ∈ p<GOAL>EuclideanGeometry.inversion c R '' ↑p = ↑p
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x : V × V<VAR>hx1 : x.1 ≠ 0<VAR>hx2 : x.2 ≠ 0<GOAL>ContinuousAt (fun y => InnerProductGeometry.angle y.1 y.2) x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>x y : V<GOAL>InnerProductGeometry.angle (c • x) (c • y) = InnerProductGeometry.angle x y
<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>InnerProductSpace ℝ E<VAR>InnerProductSpace ℝ F<VAR>f : E →ₗᵢ[ℝ] F<VAR>u v : E<GOAL>InnerProductGeometry.angle (f u) (f v) = InnerProductGeometry.angle u v
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>s : Submodule ℝ V<VAR>x y : ↥s<GOAL>InnerProductGeometry.angle ↑x ↑y = InnerProductGeometry.angle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>Real.cos (InnerProductGeometry.angle x y) = ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>InnerProductGeometry.angle x y = InnerProductGeometry.angle y x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>InnerProductGeometry.angle (-x) (-y) = InnerProductGeometry.angle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>0 ≤ InnerProductGeometry.angle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>InnerProductGeometry.angle x y ≤ π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>InnerProductGeometry.angle x (-y) = π - InnerProductGeometry.angle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>InnerProductGeometry.angle (-x) y = π - InnerProductGeometry.angle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x : V<GOAL>InnerProductGeometry.angle 0 x = π / 2
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x : V<GOAL>InnerProductGeometry.angle x 0 = π / 2
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>InnerProductGeometry.angle x x = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>InnerProductGeometry.angle x (-x) = π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>InnerProductGeometry.angle (-x) x = π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>InnerProductGeometry.angle x (r • y) = InnerProductGeometry.angle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>InnerProductGeometry.angle (r • x) y = InnerProductGeometry.angle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>r : ℝ<VAR>hr : r < 0<GOAL>InnerProductGeometry.angle x (r • y) = InnerProductGeometry.angle x (-y)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>r : ℝ<VAR>hr : r < 0<GOAL>InnerProductGeometry.angle (r • x) y = InnerProductGeometry.angle (-x) y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>Real.cos (InnerProductGeometry.angle x y) * (‖x‖ * ‖y‖) = ⟪x, y⟫_ℝ
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>Real.sin (InnerProductGeometry.angle x y) * (‖x‖ * ‖y‖) = √(⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ - ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>InnerProductGeometry.angle x y = 0 ↔ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>InnerProductGeometry.angle x y = π ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>z : V<VAR>h : InnerProductGeometry.angle x y = π<GOAL>InnerProductGeometry.angle x z + InnerProductGeometry.angle y z = π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>⟪x, y⟫_ℝ = 0 ↔ InnerProductGeometry.angle x y = π / 2
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : InnerProductGeometry.angle x y = π<GOAL>⟪x, y⟫_ℝ = -(‖x‖ * ‖y‖)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : InnerProductGeometry.angle x y = 0<GOAL>⟪x, y⟫_ℝ = ‖x‖ * ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>⟪x, y⟫_ℝ = -(‖x‖ * ‖y‖) ↔ InnerProductGeometry.angle x y = π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ ↔ InnerProductGeometry.angle x y = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : InnerProductGeometry.angle x y = π<GOAL>‖x - y‖ = ‖x‖ + ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : InnerProductGeometry.angle x y = 0<GOAL>‖x + y‖ = ‖x‖ + ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : InnerProductGeometry.angle x y = 0<GOAL>‖x - y‖ = |‖x‖ - ‖y‖|
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>‖x - y‖ = ‖x‖ + ‖y‖ ↔ InnerProductGeometry.angle x y = π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>‖x + y‖ = ‖x‖ + ‖y‖ ↔ InnerProductGeometry.angle x y = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>‖x - y‖ = |‖x‖ - ‖y‖| ↔ InnerProductGeometry.angle x y = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>‖x + y‖ = ‖x - y‖ ↔ InnerProductGeometry.angle x y = π / 2
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>Real.cos (InnerProductGeometry.angle x y) = 1 ↔ InnerProductGeometry.angle x y = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>Real.cos (InnerProductGeometry.angle x y) = 0 ↔ InnerProductGeometry.angle x y = π / 2
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>Real.cos (InnerProductGeometry.angle x y) = -1 ↔ InnerProductGeometry.angle x y = π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>Real.sin (InnerProductGeometry.angle x y) = 0 ↔ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>Real.sin (InnerProductGeometry.angle x y) = 1 ↔ InnerProductGeometry.angle x y = π / 2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>Module R M<VAR>TopologicalRing R<VAR>TopologicalAddGroup M<VAR>hmul : Filter.Tendsto (fun p => p.1 • p.2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)<VAR>hmulleft : ∀ (m : M), Filter.Tendsto (fun a => a • m) (𝓝 0) (𝓝 0)<VAR>hmulright : ∀ (a : R), Filter.Tendsto (fun m => a • m) (𝓝 0) (𝓝 0)<GOAL>ContinuousSMul R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>ContinuousAdd M<VAR>Module R M<VAR>ContinuousSMul R M<VAR>(𝓝[{x | IsUnit x}] 0).NeBot<VAR>s : Submodule R M<VAR>hs : (interior ↑s).Nonempty<GOAL>s = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>TopologicalSpace R<VAR>TopologicalSpace M<VAR>AddCommGroup M<VAR>ContinuousAdd M<VAR>Module R M<VAR>ContinuousSMul R M<VAR>Nontrivial M<VAR>(𝓝[≠] 0).NeBot<VAR>NoZeroSMulDivisors R M<VAR>x : M<GOAL>(𝓝[≠] x).NeBot
<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>Module R M₁<VAR>Module R M₂<VAR>u : TopologicalSpace R<VAR>t : TopologicalSpace M₂<VAR>ContinuousSMul R M₂<VAR>f : M₁ →ₗ[R] M₂<GOAL>ContinuousSMul R M₁