ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>s t : ℂ<VAR>a : ℝ<VAR>ha : 0 < a<GOAL>∫ (x : ℝ) in 0 ..a, ↑x ^ (s - 1) * (↑a - ↑x) ^ (t - 1) = ↑a ^ (s + t - 1) * s.betaIntegral t
<VAR>s t : ℂ<VAR>hs : 0 < s.re<VAR>ht : 0 < t.re<GOAL>Complex.Gamma s * Complex.Gamma t = Complex.Gamma (s + t) * s.betaIntegral t
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<GOAL>u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v
<VAR>u : ℂ<VAR>hu : 0 < u.re<VAR>n : ℕ<GOAL>u.betaIntegral (↑n + 1) = ↑n ! / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>n : ℕ<GOAL>s.GammaSeq n = ↑n ^ s * s.betaIntegral (↑n + 1)
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>Filter.Tendsto (fun n => ∫ (x : ℝ) in 0 ..↑n, ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) Filter.atTop (𝓝 (Complex.Gamma s))
<VAR>s : ℂ<GOAL>Filter.Tendsto s.GammaSeq Filter.atTop (𝓝 (Complex.Gamma s))
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>z.GammaSeq n * (1 - z).GammaSeq n = ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
<VAR>z : ℂ<GOAL>Complex.Gamma z * Complex.Gamma (1 - z) = ↑π / Complex.sin (↑π * z)
<VAR>s : ℂ<VAR>hs : ∀ (m : ℕ), s ≠ -↑m<GOAL>Complex.Gamma s ≠ 0
<VAR>s : ℂ<GOAL>Complex.Gamma s = 0 ↔ ∃ m, s = -↑m
<VAR>s : ℂ<VAR>hs : 0 < s.re<GOAL>Complex.Gamma s ≠ 0
<VAR>s : ℝ<GOAL>Filter.Tendsto s.GammaSeq Filter.atTop (𝓝 (Real.Gamma s))
<VAR>s : ℝ<GOAL>Real.Gamma s * Real.Gamma (1 - s) = π / Real.sin (π * s)
<VAR>s : ℂ<GOAL>(Complex.Gamma s)⁻¹ = s * (Complex.Gamma (s + 1))⁻¹
<GOAL>Differentiable ℂ fun s => (Complex.Gamma s)⁻¹
<VAR>s : ℂ<GOAL>Complex.Gamma s * Complex.Gamma (s + 1 / 2) = Complex.Gamma (2 * s) * 2 ^ (1 - 2 * s) * ↑√π
<VAR>s : ℝ<GOAL>Real.Gamma s * Real.Gamma (s + 1 / 2) = Real.Gamma (2 * s) * 2 ^ (1 - 2 * s) * √π
<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>NormedAddCommGroup W<VAR>MetricSpace Q<VAR>NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 W<VAR>s : AffineSubspace 𝕜 Q<GOAL>IsClosed ↑s.direction ↔ IsClosed ↑s
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist p₁ ((AffineMap.homothety p₁ c) p₂) = ‖c‖ * dist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>nndist p₁ ((AffineMap.homothety p₁ c) p₂) = ‖c‖₊ * nndist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist ((AffineMap.homothety p₁ c) p₂) p₁ = ‖c‖ * dist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>nndist ((AffineMap.homothety p₁ c) p₂) p₁ = ‖c‖₊ * nndist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c₁ c₂ : 𝕜<GOAL>dist ((AffineMap.lineMap p₁ p₂) c₁) ((AffineMap.lineMap p₁ p₂) c₂) = dist c₁ c₂ * dist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c₁ c₂ : 𝕜<GOAL>nndist ((AffineMap.lineMap p₁ p₂) c₁) ((AffineMap.lineMap p₁ p₂) c₂) = nndist c₁ c₂ * nndist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<GOAL>LipschitzWith (nndist p₁ p₂) ⇑(AffineMap.lineMap p₁ p₂)
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist ((AffineMap.lineMap p₁ p₂) c) p₁ = ‖c‖ * dist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>nndist ((AffineMap.lineMap p₁ p₂) c) p₁ = ‖c‖₊ * nndist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist p₁ ((AffineMap.lineMap p₁ p₂) c) = ‖c‖ * dist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>nndist p₁ ((AffineMap.lineMap p₁ p₂) c) = ‖c‖₊ * nndist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist ((AffineMap.lineMap p₁ p₂) c) p₂ = ‖1 - c‖ * dist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>nndist ((AffineMap.lineMap p₁ p₂) c) p₂ = ‖1 - c‖₊ * nndist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist p₂ ((AffineMap.lineMap p₁ p₂) c) = ‖1 - c‖ * dist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>nndist p₂ ((AffineMap.lineMap p₁ p₂) c) = ‖1 - c‖₊ * nndist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist ((AffineMap.homothety p₁ c) p₂) p₂ = ‖1 - c‖ * dist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>nndist ((AffineMap.homothety p₁ c) p₂) p₂ = ‖1 - c‖₊ * nndist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>dist p₂ ((AffineMap.homothety p₁ c) p₂) = ‖1 - c‖ * dist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p₁ p₂ : P<VAR>c : 𝕜<GOAL>nndist p₂ ((AffineMap.homothety p₁ c) p₂) = ‖1 - c‖₊ * nndist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>Invertible 2<VAR>p₁ p₂ : P<GOAL>dist p₁ (midpoint 𝕜 p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>Invertible 2<VAR>p₁ p₂ : P<GOAL>nndist p₁ (midpoint 𝕜 p₁ p₂) = ‖2‖₊⁻¹ * nndist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>Invertible 2<VAR>p₁ p₂ : P<GOAL>dist (midpoint 𝕜 p₁ p₂) p₁ = ‖2‖⁻¹ * dist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>Invertible 2<VAR>p₁ p₂ : P<GOAL>nndist (midpoint 𝕜 p₁ p₂) p₁ = ‖2‖₊⁻¹ * nndist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>Invertible 2<VAR>p₁ p₂ : P<GOAL>dist (midpoint 𝕜 p₁ p₂) p₂ = ‖2‖⁻¹ * dist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>Invertible 2<VAR>p₁ p₂ : P<GOAL>nndist (midpoint 𝕜 p₁ p₂) p₂ = ‖2‖₊⁻¹ * nndist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>Invertible 2<VAR>p₁ p₂ : P<GOAL>dist p₂ (midpoint 𝕜 p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>Invertible 2<VAR>p₁ p₂ : P<GOAL>nndist p₂ (midpoint 𝕜 p₁ p₂) = ‖2‖₊⁻¹ * nndist p₁ p₂
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>Invertible 2<VAR>p₁ p₂ p₃ p₄ : P<GOAL>dist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / ‖2‖
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>Invertible 2<VAR>p₁ p₂ p₃ p₄ : P<GOAL>nndist (midpoint 𝕜 p₁ p₂) (midpoint 𝕜 p₃ p₄) ≤ (nndist p₁ p₃ + nndist p₂ p₄) / ‖2‖₊
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p q : P<GOAL>dist ((Equiv.pointReflection p) q) p = dist p q
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>p q : P<GOAL>dist p ((Equiv.pointReflection p) q) = dist p q
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p q : P<GOAL>dist ((Equiv.pointReflection p) q) q = ‖2‖ * dist p q
<VAR>V : Type u_2<VAR>P : Type u_3<VAR>SeminormedAddCommGroup V<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor V P<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>p q : P<GOAL>dist q ((Equiv.pointReflection p) q) = ‖2‖ * dist p q
<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>NormedAddCommGroup W<VAR>MetricSpace Q<VAR>NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 W<VAR>p₁ p₂ : Q<VAR>h : p₁ ≠ p₂<GOAL>AntilipschitzWith (nndist p₁ p₂)⁻¹ ⇑(AffineMap.lineMap p₁ p₂)
<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>NormedAddCommGroup W<VAR>MetricSpace Q<VAR>NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 W<VAR>x : Q<VAR>s : Set Q<VAR>y : Q<VAR>hy : y ∈ interior s<GOAL>∀ᶠ (δ : 𝕜) in nhds 1, (AffineMap.homothety x δ) y ∈ s
<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>NormedAddCommGroup W<VAR>MetricSpace Q<VAR>NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>NormedField 𝕜<VAR>NormedSpace 𝕜 W<VAR>x : Q<VAR>s t : Set Q<VAR>ht : t.Finite<VAR>h : t ⊆ interior s<GOAL>∀ᶠ (δ : 𝕜) in nhds 1, ⇑(AffineMap.homothety x δ) '' t ⊆ s
<VAR>V : Type u_2<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>p₁ p₂ p₃ p₄ : V<GOAL>dist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (dist p₁ p₃ + dist p₂ p₄) / 2
<VAR>V : Type u_2<VAR>SeminormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>p₁ p₂ p₃ p₄ : V<GOAL>nndist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (nndist p₁ p₃ + nndist p₂ p₄) / 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedDivisionRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>P : Type u_3<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>k : 𝕜<VAR>hk : k ≠ 0<GOAL>∀ (x : E), (DilationEquiv.smulTorsor c hk) x = k • x +ᵥ c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedDivisionRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>P : Type u_3<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>k : 𝕜<VAR>hk : k ≠ 0<GOAL>∀ (x : P), (DilationEquiv.smulTorsor c hk).symm x = (k⁻¹ • fun x => x -ᵥ c) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedDivisionRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>P : Type u_3<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>k : 𝕜<VAR>hk : k ≠ 0<VAR>x y : E<VAR>h : dist x y ≠ 0<GOAL>Dilation.ratio (DilationEquiv.smulTorsor c hk) = ‖k‖₊
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NormedDivisionRing 𝕜<VAR>SeminormedAddCommGroup E<VAR>Module 𝕜 E<VAR>BoundedSMul 𝕜 E<VAR>P : Type u_3<VAR>PseudoMetricSpace P<VAR>NormedAddTorsor E P<VAR>c : P<VAR>k : 𝕜<VAR>hk : k ≠ 0<GOAL>⇑(DilationEquiv.smulTorsor c hk) ⁻¹' Metric.ball c ‖k‖ = Metric.ball 0 1
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<GOAL>IsPathConnected sᶜ
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>s : Set E<VAR>hs : s.Countable<GOAL>IsConnected sᶜ
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>x : E<GOAL>IsPathConnected {x}ᶜ
<VAR>E : Type u_1<VAR>AddCommGroup E<VAR>Module ℝ E<VAR>TopologicalSpace E<VAR>ContinuousAdd E<VAR>ContinuousSMul ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>x : E<GOAL>IsConnected {x}ᶜ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>IsPathConnected (Metric.sphere x r)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>IsConnected (Metric.sphere x r)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>h : 1 < Module.rank ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>IsPreconnected (Metric.sphere x r)
<VAR>F : Type u_1<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul ℝ F<VAR>E : Submodule ℝ F<VAR>hcodim : 1 < Module.rank ℝ (F ⧸ E)<GOAL>IsPathConnected (↑E)ᶜ
<VAR>F : Type u_1<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul ℝ F<VAR>E : Submodule ℝ F<VAR>hcodim : 1 < Module.rank ℝ (F ⧸ E)<GOAL>IsConnected (↑E)ᶜ
<VAR>F : Type u_1<VAR>AddCommGroup F<VAR>Module ℝ F<VAR>TopologicalSpace F<VAR>TopologicalAddGroup F<VAR>ContinuousSMul ℝ F<VAR>E : Submodule ℝ F<VAR>hcodim : 1 < Module.rank ℝ (F ⧸ E)<VAR>x : F<VAR>hx : x ∉ E<GOAL>connectedComponentIn (↑E)ᶜ x = (↑E)ᶜ
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → E<VAR>l : Filter α<VAR>c : α<VAR>y : E<VAR>h : IsMaxFilter (norm ∘ f) l c<VAR>hy : SameRay ℝ (f c) y<GOAL>IsMaxFilter (fun x => ‖f x + y‖) l c
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → E<VAR>l : Filter α<VAR>c : α<VAR>h : IsMaxFilter (norm ∘ f) l c<GOAL>IsMaxFilter (fun x => ‖f x + f c‖) l c
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → E<VAR>s : Set α<VAR>c : α<VAR>y : E<VAR>h : IsMaxOn (norm ∘ f) s c<VAR>hy : SameRay ℝ (f c) y<GOAL>IsMaxOn (fun x => ‖f x + y‖) s c
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : α → E<VAR>s : Set α<VAR>c : α<VAR>h : IsMaxOn (norm ∘ f) s c<GOAL>IsMaxOn (fun x => ‖f x + f c‖) s c
<VAR>X : Type u_2<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>TopologicalSpace X<VAR>f : X → E<VAR>s : Set X<VAR>c : X<VAR>y : E<VAR>h : IsLocalMaxOn (norm ∘ f) s c<VAR>hy : SameRay ℝ (f c) y<GOAL>IsLocalMaxOn (fun x => ‖f x + y‖) s c
<VAR>X : Type u_2<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>TopologicalSpace X<VAR>f : X → E<VAR>s : Set X<VAR>c : X<VAR>h : IsLocalMaxOn (norm ∘ f) s c<GOAL>IsLocalMaxOn (fun x => ‖f x + f c‖) s c
<VAR>X : Type u_2<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>TopologicalSpace X<VAR>f : X → E<VAR>c : X<VAR>y : E<VAR>h : IsLocalMax (norm ∘ f) c<VAR>hy : SameRay ℝ (f c) y<GOAL>IsLocalMax (fun x => ‖f x + y‖) c
<VAR>X : Type u_2<VAR>E : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>TopologicalSpace X<VAR>f : X → E<VAR>c : X<VAR>h : IsLocalMax (norm ∘ f) c<GOAL>IsLocalMax (fun x => ‖f x + f c‖) c
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>z : E<GOAL>‖↑‖z‖‖ = ‖z‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>hx : x ≠ 0<GOAL>‖(↑‖x‖)⁻¹ • x‖ = 1
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_nonneg : 0 ≤ r<VAR>x : E<VAR>hx : x ≠ 0<GOAL>‖(↑r * (↑‖x‖)⁻¹) • x‖ = r
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] 𝕜<VAR>h : ∀ z ∈ Metric.sphere 0 r, ‖f z‖ ≤ c<VAR>z : E<GOAL>‖f z‖ ≤ c / r * ‖z‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] 𝕜<VAR>h : ∀ z ∈ Metric.closedBall 0 r, ‖f z‖ ≤ c<VAR>z : E<GOAL>‖f z‖ ≤ c / r * ‖z‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →L[𝕜] 𝕜<VAR>h : ∀ z ∈ Metric.closedBall 0 r, ‖f z‖ ≤ c<GOAL>‖f‖ ≤ c / r
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>Nontrivial E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>Nonempty ↑(Metric.sphere 0 r)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>self : ENorm 𝕜 V<VAR>x : V<GOAL>↑self x = 0 → x = 0
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>self : ENorm 𝕜 V<VAR>c : 𝕜<VAR>x : V<GOAL>↑self (c • x) ≤ ↑‖c‖₊ * ↑self x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>self : ENorm 𝕜 V<VAR>x y : V<GOAL>↑self (x + y) ≤ ↑self x + ↑self y
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<GOAL>Function.Injective ENorm.toFun
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e₁ e₂ : ENorm 𝕜 V<VAR>h : ∀ (x : V), ↑e₁ x = ↑e₂ x<GOAL>e₁ = e₂
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e₁ e₂ : ENorm 𝕜 V<GOAL>e₁ = e₂ ↔ ∀ (x : V), ↑e₁ x = ↑e₂ x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e₁ e₂ : ENorm 𝕜 V<GOAL>↑e₁ = ↑e₂ ↔ e₁ = e₂
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>c : 𝕜<VAR>x : V<GOAL>↑e (c • x) = ↑‖c‖₊ * ↑e x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e : ENorm 𝕜 V<GOAL>↑e 0 = 0
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>x : V<GOAL>↑e x = 0 ↔ x = 0
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>x : V<GOAL>↑e (-x) = ↑e x
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>x y : V<GOAL>↑e (x - y) = ↑e (y - x)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>x y : V<GOAL>↑e (x + y) ≤ ↑e x + ↑e y
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>x y : V<GOAL>↑e (x - y) ≤ ↑e x + ↑e y
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>↑⊤ x = ⊤
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e₁ e₂ : ENorm 𝕜 V<GOAL>↑(e₁ ⊔ e₂) = fun x => max (↑e₁ x) (↑e₂ x)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e₁ e₂ : ENorm 𝕜 V<VAR>x : V<GOAL>↑(e₁ ⊔ e₂) x = max (↑e₁ x) (↑e₂ x)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>x y : ↥e.finiteSubspace<GOAL>dist x y = (↑e (↑x - ↑y)).toReal
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>x y : ↥e.finiteSubspace<GOAL>edist x y = ↑e (↑x - ↑y)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>NormedField 𝕜<VAR>AddCommGroup V<VAR>Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>x : ↥e.finiteSubspace<GOAL>‖x‖ = (↑e ↑x).toReal
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>f : E →ₛₗ[σ₁₂] F<VAR>ε C : ℝ<VAR>ε_pos : 0 < ε<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hf : ∀ (x : E), ε / ‖c‖ ≤ ‖x‖ → ‖x‖ < ε → ‖f x‖ ≤ C * ‖x‖<VAR>x : E<GOAL>‖f x‖ ≤ C * ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Fₗ : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup Fₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Fₗ<VAR>r : ℝ<VAR>r_pos : 0 < r<VAR>c : ℝ<VAR>f : E →ₗ[𝕜] Fₗ<VAR>h : ∀ z ∈ Metric.ball 0 r, ‖f z‖ ≤ c<GOAL>∃ C, ∀ (z : E), ‖f z‖ ≤ C * ‖z‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>h : RingHomIsometric σ₁₂<VAR>f : E →ₛₗ[σ₁₂] F<VAR>hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0<GOAL>∃ K, AntilipschitzWith K ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>f : E →SL[σ₁₂] F<VAR>RingHomIsometric σ₁₂<GOAL>‖f‖ = 0 ↔ f = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>Nontrivial E<GOAL>‖ContinuousLinearMap.id 𝕜 E‖ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>Nontrivial E<GOAL>‖ContinuousLinearMap.id 𝕜 E‖₊ = 1
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>Nontrivial E<VAR>f : E →SL[σ₁₂] F<VAR>a : ℝ<VAR>hf : ∀ (x : E), ‖f x‖ = a * ‖x‖<GOAL>‖f‖ = a
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Fₗ : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup Fₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Fₗ<VAR>f : E →L[𝕜] Fₗ<VAR>hf : Embedding ⇑f<GOAL>∃ K, AntilipschitzWith K ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>Nontrivial E<VAR>RingHomIsometric σ₁₂<VAR>f : E →ₛₗᵢ[σ₁₂] F<GOAL>‖f.toContinuousLinearMap‖ = 1
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>F : Type u_6<VAR>G : Type u_8<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NontriviallyNormedField 𝕜₃<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomIsometric σ₁₂<VAR>f : F →ₛₗᵢ[σ₂₃] G<VAR>g : E →SL[σ₁₂] F<GOAL>‖f.toContinuousLinearMap.comp g‖ = ‖g‖