ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>f : E'' → F''<VAR>x₀ : E''<VAR>n : ℕ<VAR>h : f =O[𝓝 x₀] fun x => ‖x - x₀‖ ^ n<VAR>hn : n ≠ 0<GOAL>f x₀ = 0
<VAR>E' : Type u_6<VAR>SeminormedAddCommGroup E'<VAR>x₀ : E'<VAR>n m : ℕ<VAR>h : n < m<GOAL>(fun x => ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x => ‖x - x₀‖ ^ n
<VAR>E' : Type u_6<VAR>SeminormedAddCommGroup E'<VAR>x₀ : E'<VAR>m : ℕ<VAR>h : 1 < m<GOAL>(fun x => ‖x - x₀‖ ^ m) =o[𝓝 x₀] fun x => x - x₀
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>SeminormedAddCommGroup E'<VAR>c : ℝ<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : Asymptotics.IsBigOWith c l f₁ f₂<VAR>hc : c < 1<GOAL>Asymptotics.IsBigOWith (1 / (1 - c)) l f₂ fun x => f₂ x - f₁ x
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>SeminormedAddCommGroup E'<VAR>c : ℝ<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : Asymptotics.IsBigOWith c l f₁ f₂<VAR>hc : c < 1<GOAL>Asymptotics.IsBigOWith (1 / (1 - c)) l f₂ fun x => f₁ x + f₂ x
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>SeminormedAddCommGroup E'<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : f₁ =o[l] f₂<GOAL>f₂ =O[l] fun x => f₂ x - f₁ x
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>SeminormedAddCommGroup E'<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : f₁ =o[l] f₂<GOAL>f₂ =O[l] fun x => f₁ x + f₂ x
<VAR>α : Type u_1<VAR>E' : Type u_6<VAR>SeminormedAddCommGroup E'<VAR>l : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : f₁ =o[l] f₂<GOAL>f₂ =O[l] (f₂ + f₁)
<VAR>α : Type u_1<VAR>E : Type u_3<VAR>F'' : Type u_10<VAR>Norm E<VAR>NormedAddCommGroup F''<VAR>f : α → E<VAR>g'' : α → F''<VAR>h : f =O[Filter.cofinite] g''<GOAL>∃ C > 0, ∀ ⦃x : α⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
<VAR>α : Type u_1<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>h : ∀ (x : α), g'' x = 0 → f'' x = 0<GOAL>f'' =O[Filter.cofinite] g'' ↔ ∃ C, ∀ (x : α), ‖f'' x‖ ≤ C * ‖g'' x‖
<VAR>E : Type u_3<VAR>E'' : Type u_9<VAR>Norm E<VAR>NormedAddCommGroup E''<VAR>f : ℕ → E<VAR>g'' : ℕ → E''<VAR>h : f =O[Filter.atTop] g''<GOAL>∃ C > 0, ∀ ⦃x : ℕ⦄, g'' x ≠ 0 → ‖f x‖ ≤ C * ‖g'' x‖
<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>NormedAddCommGroup E''<VAR>NormedAddCommGroup F''<VAR>f : ℕ → E''<VAR>g : ℕ → F''<VAR>h : ∀ (x : ℕ), g x = 0 → f x = 0<GOAL>f =O[Filter.atTop] g ↔ ∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖g x‖
<VAR>E'' : Type u_9<VAR>NormedAddCommGroup E''<VAR>f : ℕ → E''<GOAL>(f =O[Filter.atTop] fun _n => 1) ↔ ∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C
<VAR>α : Type u_1<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup F'<VAR>g' : α → F'<VAR>l : Filter α<VAR>ι : Type u_17<VAR>Fintype ι<VAR>E' : ι → Type u_18<VAR>(i : ι) → NormedAddCommGroup (E' i)<VAR>f : α → (i : ι) → E' i<VAR>C : ℝ<VAR>hC : 0 ≤ C<GOAL>Asymptotics.IsBigOWith C l f g' ↔ ∀ (i : ι), Asymptotics.IsBigOWith C l (fun x => f x i) g'
<VAR>α : Type u_1<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup F'<VAR>g' : α → F'<VAR>l : Filter α<VAR>ι : Type u_17<VAR>Fintype ι<VAR>E' : ι → Type u_18<VAR>(i : ι) → NormedAddCommGroup (E' i)<VAR>f : α → (i : ι) → E' i<GOAL>f =O[l] g' ↔ ∀ (i : ι), (fun x => f x i) =O[l] g'
<VAR>α : Type u_1<VAR>F' : Type u_7<VAR>SeminormedAddCommGroup F'<VAR>g' : α → F'<VAR>l : Filter α<VAR>ι : Type u_17<VAR>Fintype ι<VAR>E' : ι → Type u_18<VAR>(i : ι) → NormedAddCommGroup (E' i)<VAR>f : α → (i : ι) → E' i<GOAL>f =o[l] g' ↔ ∀ (i : ι), (fun x => f x i) =o[l] g'
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>R : Type u_17<VAR>StrictOrderedSemiring R<VAR>Archimedean R<VAR>f : R → E<VAR>g : R → F<VAR>h : f =O[Filter.atTop] g<GOAL>(fun n => f ↑n) =O[Filter.atTop] fun n => g ↑n
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>R : Type u_17<VAR>StrictOrderedSemiring R<VAR>Archimedean R<VAR>f : R → E<VAR>g : R → F<VAR>h : f =o[Filter.atTop] g<GOAL>(fun n => f ↑n) =o[Filter.atTop] fun n => g ↑n
<VAR>E : Type u_3<VAR>F : Type u_4<VAR>Norm E<VAR>Norm F<VAR>α : Type u_17<VAR>SemilatticeSup α<VAR>Nonempty α<VAR>f : α → E<VAR>g : α → F<GOAL>f =O[Filter.atTop] g ↔ ∀ᶠ (n₀ : α) in Filter.atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖
<VAR>G : Type u_5<VAR>G' : Type u_8<VAR>Norm G<VAR>SeminormedAddCommGroup G'<VAR>α : Type u_17<VAR>SemilatticeSup α<VAR>Nonempty α<VAR>f : α → G<VAR>g : α → G'<GOAL>f =O[Filter.atTop] g ↔ ∀ᶠ (n₀ : α) in Filter.atTop, ∃ c > 0, ∀ n ≥ n₀, c * ‖f n‖ ≤ ‖g n‖
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>CompleteSpace E<VAR>f : ι → E<VAR>g : ι → ℝ<VAR>hg : Summable g<VAR>h : f =O[Filter.cofinite] g<GOAL>Summable f
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>CompleteSpace E<VAR>f : ℕ → E<VAR>g : ℕ → ℝ<VAR>hg : Summable g<VAR>h : f =O[Filter.atTop] g<GOAL>Summable f
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>f : E → F<VAR>g : ι → E<VAR>hf : f =O[𝓝 0] id<VAR>hg : Summable fun x => ‖g x‖<GOAL>Summable fun x => ‖f (g x)‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>E : Type u_3<VAR>Norm E<VAR>F : Type u_4<VAR>Norm F<VAR>e : PartialHomeomorph α β<VAR>b : β<VAR>hb : b ∈ e.target<VAR>f : β → E<VAR>g : β → F<VAR>C : ℝ<GOAL>Asymptotics.IsBigOWith C (𝓝 b) f g ↔ Asymptotics.IsBigOWith C (𝓝 (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>E : Type u_3<VAR>Norm E<VAR>F : Type u_4<VAR>Norm F<VAR>e : PartialHomeomorph α β<VAR>b : β<VAR>hb : b ∈ e.target<VAR>f : β → E<VAR>g : β → F<GOAL>f =O[𝓝 b] g ↔ (f ∘ ↑e) =O[𝓝 (↑e.symm b)] (g ∘ ↑e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>E : Type u_3<VAR>Norm E<VAR>F : Type u_4<VAR>Norm F<VAR>e : PartialHomeomorph α β<VAR>b : β<VAR>hb : b ∈ e.target<VAR>f : β → E<VAR>g : β → F<GOAL>f =o[𝓝 b] g ↔ (f ∘ ↑e) =o[𝓝 (↑e.symm b)] (g ∘ ↑e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>E : Type u_3<VAR>Norm E<VAR>F : Type u_4<VAR>Norm F<VAR>e : α ≃ₜ β<VAR>b : β<VAR>f : β → E<VAR>g : β → F<VAR>C : ℝ<GOAL>Asymptotics.IsBigOWith C (𝓝 b) f g ↔ Asymptotics.IsBigOWith C (𝓝 (e.symm b)) (f ∘ ⇑e) (g ∘ ⇑e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>E : Type u_3<VAR>Norm E<VAR>F : Type u_4<VAR>Norm F<VAR>e : α ≃ₜ β<VAR>b : β<VAR>f : β → E<VAR>g : β → F<GOAL>f =O[𝓝 b] g ↔ (f ∘ ⇑e) =O[𝓝 (e.symm b)] (g ∘ ⇑e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>TopologicalSpace α<VAR>TopologicalSpace β<VAR>E : Type u_3<VAR>Norm E<VAR>F : Type u_4<VAR>Norm F<VAR>e : α ≃ₜ β<VAR>b : β<VAR>f : β → E<VAR>g : β → F<GOAL>f =o[𝓝 b] g ↔ (f ∘ ⇑e) =o[𝓝 (e.symm b)] (g ∘ ⇑e)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>x : WithLp 1 (Unitization 𝕜 A)<GOAL>‖x‖ = ‖((WithLp.equiv 1 (Unitization 𝕜 A)) x).fst‖ + ‖((WithLp.equiv 1 (Unitization 𝕜 A)) x).snd‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>x : WithLp 1 (Unitization 𝕜 A)<GOAL>‖x‖₊ = ‖((WithLp.equiv 1 (Unitization 𝕜 A)) x).fst‖₊ + ‖((WithLp.equiv 1 (Unitization 𝕜 A)) x).snd‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>x : A<GOAL>‖(WithLp.equiv 1 (Unitization 𝕜 A)).symm ↑x‖ = ‖x‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>x : A<GOAL>‖(WithLp.equiv 1 (Unitization 𝕜 A)).symm ↑x‖₊ = ‖x‖₊
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<GOAL>Isometry fun x => (WithLp.equiv 1 (Unitization 𝕜 A)).symm ↑x
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>x y : WithLp 1 (Unitization 𝕜 A)<GOAL>(WithLp.equiv 1 (Unitization 𝕜 A)) (x * y) = (WithLp.equiv 1 (Unitization 𝕜 A)) x * (WithLp.equiv 1 (Unitization 𝕜 A)) y
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>r : 𝕜<GOAL>(WithLp.equiv 1 (Unitization 𝕜 A)) ((algebraMap 𝕜 (WithLp 1 (Unitization 𝕜 A))) r) = (algebraMap 𝕜 (Unitization 𝕜 A)) r
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>R : Type u_3<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>DistribMulAction R A<VAR>IsScalarTower R 𝕜 A<VAR>a : WithLp 1 (Unitization 𝕜 A)<GOAL>(WithLp.unitizationAlgEquiv R) a = a
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>NormedField 𝕜<VAR>NonUnitalNormedRing A<VAR>NormedSpace 𝕜 A<VAR>IsScalarTower 𝕜 A A<VAR>SMulCommClass 𝕜 A A<VAR>R : Type u_3<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>DistribMulAction R A<VAR>IsScalarTower R 𝕜 A<VAR>a : WithLp 1 (Unitization 𝕜 A)<GOAL>(WithLp.unitizationAlgEquiv R).symm a = a
<VAR>R : Type u_4<VAR>NonUnitalNonAssocRing R<VAR>self : RingSeminorm R<VAR>x y : R<GOAL>self.toFun (x * y) ≤ self.toFun x * self.toFun y
<VAR>R : Type u_2<VAR>NonUnitalRing R<VAR>p : RingSeminorm R<GOAL>⇑p.toAddGroupSeminorm = ⇑p
<VAR>R : Type u_2<VAR>NonUnitalRing R<VAR>p q : RingSeminorm R<GOAL>(∀ (x : R), p x = q x) → p = q
<VAR>R : Type u_2<VAR>NonUnitalRing R<VAR>p : RingSeminorm R<GOAL>p = 0 ↔ ∀ (x : R), p x = 0
<VAR>R : Type u_2<VAR>NonUnitalRing R<VAR>p : RingSeminorm R<GOAL>p ≠ 0 ↔ ∃ x, p x ≠ 0
<VAR>R : Type u_2<VAR>NonUnitalRing R<VAR>DecidableEq R<VAR>x : R<GOAL>1 x = if x = 0 then 0 else 1
<VAR>R : Type u_2<VAR>Ring R<VAR>p : RingSeminorm R<VAR>hp : p 1 ≤ 1<GOAL>p 1 = 1 ↔ p ≠ 0
<VAR>R : Type u_2<VAR>NonUnitalRing R<VAR>p : RingNorm R<GOAL>p.toFun = ⇑p
<VAR>R : Type u_2<VAR>NonUnitalRing R<VAR>p q : RingNorm R<GOAL>(∀ (x : R), p x = q x) → p = q
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>p : MulRingSeminorm R<GOAL>⇑p.toAddGroupSeminorm = ⇑p
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>p q : MulRingSeminorm R<GOAL>(∀ (x : R), p x = q x) → p = q
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>DecidableEq R<VAR>NoZeroDivisors R<VAR>Nontrivial R<VAR>x : R<GOAL>1 x = if x = 0 then 0 else 1
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>p : MulRingNorm R<GOAL>p.toFun = ⇑p
<VAR>R : Type u_2<VAR>NonAssocRing R<VAR>p q : MulRingNorm R<GOAL>(∀ (x : R), p x = q x) → p = q
<VAR>R : Type u_4<VAR>Ring R<VAR>f : MulRingNorm R<GOAL>f.equiv f
<VAR>R : Type u_4<VAR>Ring R<VAR>f g : MulRingNorm R<VAR>hfg : f.equiv g<GOAL>g.equiv f
<VAR>R : Type u_4<VAR>Ring R<VAR>f g k : MulRingNorm R<VAR>hfg : f.equiv g<VAR>hgk : g.equiv k<GOAL>f.equiv k
<VAR>R : Type u_4<VAR>NonUnitalNormedRing R<GOAL>∀ (a : R), (normRingNorm R).toFun a = ‖a‖
<VAR>R : Type u_4<VAR>Ring R<VAR>n : ℕ<VAR>f : MulRingNorm R<GOAL>f ↑n ≤ ↑n
<VAR>R : Type u_4<VAR>Ring R<VAR>x : ℤ<VAR>f : MulRingNorm R<GOAL>f ↑x.natAbs = f ↑x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace 𝕜<VAR>n : ℕ∞<VAR>f : E → F →L[𝕜] G<VAR>s : Set E<VAR>FiniteDimensional 𝕜 F<GOAL>ContDiffOn 𝕜 n f s ↔ ∀ (y : F), ContDiffOn 𝕜 n (fun x => (f x) y) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>G : Type uG<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>CompleteSpace 𝕜<VAR>n : ℕ∞<VAR>f : E → F →L[𝕜] G<VAR>FiniteDimensional 𝕜 F<GOAL>ContDiff 𝕜 n f ↔ ∀ (y : F), ContDiff 𝕜 n fun x => (f x) y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>f : E → F<GOAL>ContDiff 𝕜 (↑(n + 1)) f ↔ Differentiable 𝕜 f ∧ ∀ (y : E), ContDiff 𝕜 ↑n fun x => (fderiv 𝕜 f x) y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>f : E → F<VAR>s : Set E<VAR>hf : DifferentiableOn 𝕜 f s<VAR>h : ∀ (y : E), ContDiffOn 𝕜 (↑n) (fun x => (fderivWithin 𝕜 f s x) y) s<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type uF<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>FiniteDimensional 𝕜 E<VAR>n : ℕ<VAR>f : E → F<VAR>s : Set E<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f s ↔ DifferentiableOn 𝕜 f s ∧ ∀ (y : E), ContDiffOn 𝕜 (↑n) (fun x => (fderivWithin 𝕜 f s x) y) s
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>t : R<VAR>h : ‖t‖ < 1<GOAL>↑(Units.oneSub t h) = 1 - t
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : Rˣ<VAR>t : R<VAR>h : ‖t‖ < ‖↑x⁻¹‖⁻¹<GOAL>↑(x.add t h) = ↑x + t
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : Rˣ<VAR>y : R<VAR>h : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹<GOAL>↑(x.ofNearby y h) = y
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<GOAL>IsOpen {x | IsUnit x}
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : Rˣ<GOAL>{x | IsUnit x} ∈ 𝓝 ↑x
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<GOAL>nonunits R ⊆ (Metric.ball 1 1)ᶜ
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<GOAL>IsClosed (nonunits R)
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>t : R<VAR>h : ‖t‖ < 1<GOAL>Ring.inverse (1 - t) = ↑(Units.oneSub t h)⁻¹
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : Rˣ<GOAL>∀ᶠ (t : R) in 𝓝 0, Ring.inverse (↑x + t) = Ring.inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>n : ℕ<VAR>t : R<VAR>ht : ‖t‖ < 1<GOAL>Ring.inverse (1 - t) = ∑ i ∈ Finset.range n, t ^ i + t ^ n * Ring.inverse (1 - t)
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>n : ℕ<GOAL>∀ᶠ (t : R) in 𝓝 0, Ring.inverse (1 - t) = ∑ i ∈ Finset.range n, t ^ i + t ^ n * Ring.inverse (1 - t)
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : Rˣ<VAR>n : ℕ<GOAL>∀ᶠ (t : R) in 𝓝 0, Ring.inverse (↑x + t) = (∑ i ∈ Finset.range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * Ring.inverse (↑x + t)
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<GOAL>(fun t => Ring.inverse (1 - t)) =O[𝓝 0] fun _t => 1
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : Rˣ<GOAL>(fun t => Ring.inverse (↑x + t)) =O[𝓝 0] fun _t => 1
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : Rˣ<VAR>n : ℕ<GOAL>(fun t => Ring.inverse (↑x + t) - (∑ i ∈ Finset.range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ n
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : Rˣ<GOAL>(fun t => Ring.inverse (↑x + t) - ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : Rˣ<GOAL>(fun t => Ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ 2
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>x : Rˣ<GOAL>ContinuousAt Ring.inverse ↑x
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<GOAL>OpenEmbedding Units.val
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<GOAL>IsOpenMap Units.val
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>I : Ideal R<VAR>x : R<VAR>hxI : x ∈ I<VAR>hx : ‖1 - x‖ < 1<GOAL>I = ⊤
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>I : Ideal R<VAR>hI : I ≠ ⊤<GOAL>I.closure ≠ ⊤
<VAR>R : Type u_1<VAR>NormedRing R<VAR>CompleteSpace R<VAR>I : Ideal R<VAR>hI : I.IsMaximal<GOAL>I.closure = I
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>x : R<GOAL>seminormFromConst_seq c f x = fun n => f (x * c ^ n) / f c ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>x : R<GOAL>0 ≤ seminormFromConst_seq c f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>x : R<GOAL>BddBelow (Set.range (seminormFromConst_seq c f x))
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf : f 0 = 0<GOAL>seminormFromConst_seq c f 0 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>n : ℕ<VAR>hn : 1 ≤ n<GOAL>seminormFromConst_seq c f 1 n = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<GOAL>Antitone (seminormFromConst_seq c f x)
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<GOAL>Filter.Tendsto (seminormFromConst_seq c f x) Filter.atTop (𝓝 (seminormFromConst' hf1 hc hpm x))
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<GOAL>seminormFromConst' hf1 hc hpm 1 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<GOAL>(seminormFromConst hf1 hc hpm) x = seminormFromConst' hf1 hc hpm x
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<GOAL>seminormFromConst' hf1 hc hpm 1 ≤ 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>hna : IsNonarchimedean ⇑f<GOAL>IsNonarchimedean (seminormFromConst' hf1 hc hpm)
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<GOAL>IsPowMul (seminormFromConst' hf1 hc hpm)
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<GOAL>seminormFromConst' hf1 hc hpm x ≤ f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<GOAL>seminormFromConst' hf1 hc hpm x = f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<VAR>y : R<GOAL>seminormFromConst' hf1 hc hpm (x * y) = seminormFromConst' hf1 hc hpm x * seminormFromConst' hf1 hc hpm y
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<GOAL>seminormFromConst' hf1 hc hpm c = f c
<VAR>R : Type u_1<VAR>CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<GOAL>seminormFromConst' hf1 hc hpm (c * x) = seminormFromConst' hf1 hc hpm c * seminormFromConst' hf1 hc hpm x
<VAR>K : Type u_1<VAR>Field K<VAR>k : K<VAR>g : RingSeminorm K<VAR>hg1 : g 1 ≤ 1<VAR>hg_k : g k ≠ 0<VAR>hg_pm : IsPowMul ⇑g<VAR>x : K<GOAL>(normFromConst hg1 hg_k hg_pm) x = seminormFromConst' hg1 hg_k hg_pm x
<VAR>F : Type u_2<VAR>E₁ : Type u_3<VAR>SeminormedAddCommGroup F<VAR>NormedAddCommGroup E₁<VAR>R₁ : Type u_4<VAR>Field R₁<VAR>Module R₁ E₁<VAR>Module R₁ F<VAR>FiniteDimensional R₁ E₁<VAR>FiniteDimensional R₁ F<VAR>li : E₁ →ₗᵢ[R₁] F<VAR>h : FiniteDimensional.finrank R₁ E₁ = FiniteDimensional.finrank R₁ F<GOAL>⇑(li.toLinearIsometryEquiv h) = ⇑li
<VAR>F : Type u_2<VAR>E₁ : Type u_3<VAR>SeminormedAddCommGroup F<VAR>NormedAddCommGroup E₁<VAR>R₁ : Type u_4<VAR>Field R₁<VAR>Module R₁ E₁<VAR>Module R₁ F<VAR>FiniteDimensional R₁ E₁<VAR>FiniteDimensional R₁ F<VAR>li : E₁ →ₗᵢ[R₁] F<VAR>h : FiniteDimensional.finrank R₁ E₁ = FiniteDimensional.finrank R₁ F<VAR>x : E₁<GOAL>(li.toLinearIsometryEquiv h) x = li x
<VAR>𝕜 : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>P₁ : Type u_4<VAR>P₂ : Type u_5<VAR>NormedField 𝕜<VAR>NormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₁<VAR>NormedSpace 𝕜 V₂<VAR>MetricSpace P₁<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₁ P₁<VAR>NormedAddTorsor V₂ P₂<VAR>FiniteDimensional 𝕜 V₁<VAR>FiniteDimensional 𝕜 V₂<VAR>Inhabited P₁<VAR>li : P₁ →ᵃⁱ[𝕜] P₂<VAR>h : FiniteDimensional.finrank 𝕜 V₁ = FiniteDimensional.finrank 𝕜 V₂<GOAL>⇑(li.toAffineIsometryEquiv h) = ⇑li
<VAR>𝕜 : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>P₁ : Type u_4<VAR>P₂ : Type u_5<VAR>NormedField 𝕜<VAR>NormedAddCommGroup V₁<VAR>SeminormedAddCommGroup V₂<VAR>NormedSpace 𝕜 V₁<VAR>NormedSpace 𝕜 V₂<VAR>MetricSpace P₁<VAR>PseudoMetricSpace P₂<VAR>NormedAddTorsor V₁ P₁<VAR>NormedAddTorsor V₂ P₂<VAR>FiniteDimensional 𝕜 V₁<VAR>FiniteDimensional 𝕜 V₂<VAR>Inhabited P₁<VAR>li : P₁ →ᵃⁱ[𝕜] P₂<VAR>h : FiniteDimensional.finrank 𝕜 V₁ = FiniteDimensional.finrank 𝕜 V₂<VAR>x : P₁<GOAL>(li.toAffineIsometryEquiv h) x = li x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>PE : Type u_1<VAR>PF : Type u_2<VAR>MetricSpace PE<VAR>NormedAddTorsor E PE<VAR>MetricSpace PF<VAR>NormedAddTorsor F PF<VAR>FiniteDimensional 𝕜 E<VAR>f : PE →ᵃ[𝕜] PF<GOAL>Continuous ⇑f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>PE : Type u_1<VAR>PF : Type u_2<VAR>MetricSpace PE<VAR>NormedAddTorsor E PE<VAR>MetricSpace PF<VAR>NormedAddTorsor F PF<VAR>FiniteDimensional 𝕜 E<VAR>f : PE ≃ᵃ[𝕜] PF<GOAL>Continuous ⇑f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>PE : Type u_1<VAR>PF : Type u_2<VAR>MetricSpace PE<VAR>NormedAddTorsor E PE<VAR>MetricSpace PF<VAR>NormedAddTorsor F PF<VAR>FiniteDimensional 𝕜 E<VAR>f : PE ≃ᵃ[𝕜] PF<GOAL>⇑f.toHomeomorphOfFiniteDimensional = ⇑f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>PE : Type u_1<VAR>PF : Type u_2<VAR>MetricSpace PE<VAR>NormedAddTorsor E PE<VAR>MetricSpace PF<VAR>NormedAddTorsor F PF<VAR>FiniteDimensional 𝕜 E<VAR>f : PE ≃ᵃ[𝕜] PF<GOAL>⇑f.toHomeomorphOfFiniteDimensional.symm = ⇑f.symm
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<GOAL>Continuous fun f => f.det
<VAR>E' : Type u_1<VAR>NormedAddCommGroup E'<VAR>NormedSpace ℝ E'<VAR>FiniteDimensional ℝ E'<GOAL>lipschitzExtensionConstant E' = let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv; max (‖↑A.symm‖₊ * ‖↑A‖₊) 1
<VAR>E' : Type u_1<VAR>NormedAddCommGroup E'<VAR>NormedSpace ℝ E'<VAR>FiniteDimensional ℝ E'<GOAL>0 < lipschitzExtensionConstant E'
<VAR>α : Type u_1<VAR>PseudoMetricSpace α<VAR>E' : Type u_2<VAR>NormedAddCommGroup E'<VAR>NormedSpace ℝ E'<VAR>FiniteDimensional ℝ E'<VAR>s : Set α<VAR>f : α → E'<VAR>K : ℝ≥0<VAR>hf : LipschitzOnWith K f s<GOAL>∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ Set.EqOn f g s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] F<VAR>hf : LinearMap.ker f = ⊥<GOAL>∃ K > 0, AntilipschitzWith K ⇑f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>FiniteDimensional 𝕜 E<VAR>f : E →ₗ[𝕜] F<GOAL>Function.Injective ⇑f ↔ ∃ K > 0, AntilipschitzWith K ⇑f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>FiniteDimensional 𝕜 E<GOAL>IsOpen {L | Function.Injective ⇑L}
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>Finite ι<VAR>f : ι → E<VAR>hf : LinearIndependent 𝕜 f<GOAL>∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace 𝕜<VAR>ι : Type u_1<VAR>Finite ι<GOAL>IsOpen {f | LinearIndependent 𝕜 f}
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type w<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace 𝕜<VAR>n : ℕ<GOAL>IsOpen {f | ↑n ≤ (↑f).rank}