ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>(i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>(i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<GOAL>‖g.compContinuousLinearMapLRight‖ ≤ ‖g‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>(i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>(i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : (i : ι) → E i ≃L[𝕜] E₁ i<GOAL>(ContinuousMultilinearMap.compContinuousLinearMapEquivL G f).symm = ContinuousMultilinearMap.compContinuousLinearMapEquivL G fun i => (f i).symm
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>(i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>(i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : ContinuousMultilinearMap 𝕜 E₁ G<VAR>f : (i : ι) → E i ≃L[𝕜] E₁ i<GOAL>(ContinuousMultilinearMap.compContinuousLinearMapEquivL G f) g = g.compContinuousLinearMap fun i => ↑(f i)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E₁ : ι → Type wE₁<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>(i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>α : Type u_1<VAR>Fintype α<VAR>f : ContinuousMultilinearMap 𝕜 E₁ G<VAR>s : Set ι<VAR>e : α ≃ ↑s<VAR>DecidablePred fun x => x ∈ s<VAR>v : (i : { a // a ∉ s }) → E₁ ↑i<VAR>w : α → (i : ι) → E₁ i<GOAL>((f.iteratedFDerivComponent e) v) w = f fun j => if h : j ∈ s then w (e.symm ⟨j, h⟩) j else v ⟨j, h⟩
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E₁ : ι → Type wE₁<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>(i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>α : Type u_1<VAR>Fintype α<VAR>f : ContinuousMultilinearMap 𝕜 E₁ G<VAR>s : Set ι<VAR>e : α ≃ ↑s<VAR>DecidablePred fun x => x ∈ s<VAR>x : (i : ι) → E₁ i<GOAL>‖(f.iteratedFDerivComponent e) fun x_1 => x ↑x_1‖ ≤ ‖f‖ * ‖x‖ ^ (Fintype.card ι - Fintype.card α)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E₁ : ι → Type wE₁<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>(i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E₁ G<VAR>k : ℕ<VAR>x : (i : ι) → E₁ i<GOAL>‖f.iteratedFDeriv k x‖ ≤ ↑((Fintype.card ι).descFactorial k) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>‖f‖ = 0 ↔ f = 0
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>Subsingleton ι<VAR>Nontrivial G<VAR>i : ι<GOAL>‖(ContinuousMultilinearMap.ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖ = 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>Subsingleton ι<VAR>Nontrivial G<VAR>i : ι<GOAL>‖(ContinuousMultilinearMap.ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖₊ = 1
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → NormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E G<VAR>ε : ι → ℝ<VAR>C : ℝ<VAR>hε : ∀ (i : ι), 0 < ε i<VAR>c : ι → 𝕜<VAR>hc : ∀ (i : ι), 1 < ‖c i‖<VAR>hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<VAR>m : (i : ι) → E i<GOAL>‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>p : 𝕜[X]<VAR>x : 𝕜<GOAL>HasStrictDerivAt (fun x => Polynomial.eval x p) (Polynomial.eval x (Polynomial.derivative p)) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>q : R[X]<VAR>x : 𝕜<GOAL>HasStrictDerivAt (fun x => (Polynomial.aeval x) q) ((Polynomial.aeval x) (Polynomial.derivative q)) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>p : 𝕜[X]<VAR>x : 𝕜<GOAL>HasDerivAt (fun x => Polynomial.eval x p) (Polynomial.eval x (Polynomial.derivative p)) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>q : R[X]<VAR>x : 𝕜<GOAL>HasDerivAt (fun x => (Polynomial.aeval x) q) ((Polynomial.aeval x) (Polynomial.derivative q)) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>p : 𝕜[X]<VAR>x : 𝕜<VAR>s : Set 𝕜<GOAL>HasDerivWithinAt (fun x => Polynomial.eval x p) (Polynomial.eval x (Polynomial.derivative p)) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>q : R[X]<VAR>x : 𝕜<VAR>s : Set 𝕜<GOAL>HasDerivWithinAt (fun x => (Polynomial.aeval x) q) ((Polynomial.aeval x) (Polynomial.derivative q)) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>p : 𝕜[X]<GOAL>DifferentiableAt 𝕜 (fun x => Polynomial.eval x p) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>q : R[X]<GOAL>DifferentiableAt 𝕜 (fun x => (Polynomial.aeval x) q) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>p : 𝕜[X]<GOAL>DifferentiableWithinAt 𝕜 (fun x => Polynomial.eval x p) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>q : R[X]<GOAL>DifferentiableWithinAt 𝕜 (fun x => (Polynomial.aeval x) q) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>p : 𝕜[X]<GOAL>Differentiable 𝕜 fun x => Polynomial.eval x p
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>q : R[X]<GOAL>Differentiable 𝕜 fun x => (Polynomial.aeval x) q
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>s : Set 𝕜<VAR>p : 𝕜[X]<GOAL>DifferentiableOn 𝕜 (fun x => Polynomial.eval x p) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>s : Set 𝕜<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>q : R[X]<GOAL>DifferentiableOn 𝕜 (fun x => (Polynomial.aeval x) q) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>p : 𝕜[X]<GOAL>deriv (fun x => Polynomial.eval x p) x = Polynomial.eval x (Polynomial.derivative p)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>q : R[X]<GOAL>deriv (fun x => (Polynomial.aeval x) q) x = (Polynomial.aeval x) (Polynomial.derivative q)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>p : 𝕜[X]<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => Polynomial.eval x p) s x = Polynomial.eval x (Polynomial.derivative p)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>q : R[X]<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => (Polynomial.aeval x) q) s x = (Polynomial.aeval x) (Polynomial.derivative q)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>p : 𝕜[X]<VAR>x : 𝕜<GOAL>HasFDerivAt (fun x => Polynomial.eval x p) (ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>q : R[X]<VAR>x : 𝕜<GOAL>HasFDerivAt (fun x => (Polynomial.aeval x) q) (ContinuousLinearMap.smulRight 1 ((Polynomial.aeval x) (Polynomial.derivative q))) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>s : Set 𝕜<VAR>p : 𝕜[X]<VAR>x : 𝕜<GOAL>HasFDerivWithinAt (fun x => Polynomial.eval x p) (ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>s : Set 𝕜<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>q : R[X]<VAR>x : 𝕜<GOAL>HasFDerivWithinAt (fun x => (Polynomial.aeval x) q) (ContinuousLinearMap.smulRight 1 ((Polynomial.aeval x) (Polynomial.derivative q))) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>p : 𝕜[X]<GOAL>fderiv 𝕜 (fun x => Polynomial.eval x p) x = ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>q : R[X]<GOAL>fderiv 𝕜 (fun x => (Polynomial.aeval x) q) x = ContinuousLinearMap.smulRight 1 ((Polynomial.aeval x) (Polynomial.derivative q))
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>p : 𝕜[X]<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun x => Polynomial.eval x p) s x = ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Algebra R 𝕜<VAR>q : R[X]<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun x => (Polynomial.aeval x) q) s x = ContinuousLinearMap.smulRight 1 ((Polynomial.aeval x) (Polynomial.derivative q))
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>self : f.NonlinearRightInverse<VAR>y : F<GOAL>‖self.toFun y‖ ≤ ↑self.nnnorm * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>self : f.NonlinearRightInverse<VAR>y : F<GOAL>f (self.toFun y) = y
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>fsymm : f.NonlinearRightInverse<VAR>y : F<GOAL>f (fsymm.toFun y) = y
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>fsymm : f.NonlinearRightInverse<VAR>y : F<GOAL>‖fsymm.toFun y‖ ≤ ↑fsymm.nnnorm * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>CompleteSpace F<VAR>surj : Function.Surjective ⇑f<GOAL>∃ C ≥ 0, ∀ (y : F), ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>surj : Function.Surjective ⇑f<GOAL>∃ C > 0, ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>surj : Function.Surjective ⇑f<GOAL>IsOpenMap ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>surj : Function.Surjective ⇑f<GOAL>QuotientMap ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_5<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>MetricSpace P<VAR>NormedAddTorsor E P<VAR>MetricSpace Q<VAR>NormedAddTorsor F Q<VAR>f : P →ᵃ[𝕜] Q<VAR>hf : Continuous ⇑f<VAR>surj : Function.Surjective ⇑f<GOAL>IsOpenMap ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>hsurj : Function.Surjective ⇑f<VAR>s : Set F<GOAL>interior (⇑f ⁻¹' s) = ⇑f ⁻¹' interior s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>hsurj : Function.Surjective ⇑f<VAR>s : Set F<GOAL>closure (⇑f ⁻¹' s) = ⇑f ⁻¹' closure s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>hsurj : Function.Surjective ⇑f<VAR>s : Set F<GOAL>frontier (⇑f ⁻¹' s) = ⇑f ⁻¹' frontier s
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hsurj : LinearMap.range f = ⊤<GOAL>∃ fsymm, 0 < fsymm.nnnorm
<VAR>𝕜 : Type u_5<VAR>𝕜' : Type u_6<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hsurj : LinearMap.range f = ⊤<GOAL>f.nonlinearRightInverseOfSurjective hsurj = Classical.choose ⋯
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hsurj : LinearMap.range f = ⊤<GOAL>0 < (f.nonlinearRightInverseOfSurjective hsurj).nnnorm
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>e : E ≃ₛₗ[σ] F<VAR>h : Continuous ⇑e<GOAL>Continuous ⇑e.symm
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>e : E ≃ₛₗ[σ] F<VAR>h : Continuous ⇑e<GOAL>⇑(e.toContinuousLinearEquivOfContinuous h) = ⇑e
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>e : E ≃ₛₗ[σ] F<VAR>h : Continuous ⇑e<GOAL>⇑(e.toContinuousLinearEquivOfContinuous h).symm = ⇑e.symm
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hinj : Function.Injective ⇑f<VAR>hclo : IsClosed (Set.range ⇑f)<GOAL>↑(f.equivRange hinj hclo) = f.rangeRestrict
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hinj : Function.Injective ⇑f<VAR>hclo : IsClosed (Set.range ⇑f)<GOAL>⇑(f.equivRange hinj hclo) = ⇑f.rangeRestrict
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hinj : LinearMap.ker f = ⊥<VAR>hsurj : LinearMap.range f = ⊤<GOAL>⇑(ContinuousLinearEquiv.ofBijective f hinj hsurj) = ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hinj : LinearMap.ker f = ⊥<VAR>hsurj : LinearMap.range f = ⊤<GOAL>↑(ContinuousLinearEquiv.ofBijective f hinj hsurj) = f
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hinj : LinearMap.ker f = ⊥<VAR>hsurj : LinearMap.range f = ⊤<VAR>x : E<GOAL>(ContinuousLinearEquiv.ofBijective f hinj hsurj).symm (f x) = x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>RingHomIsometric σ<VAR>RingHomIsometric σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace F<VAR>CompleteSpace E<VAR>f : E →SL[σ] F<VAR>hinj : LinearMap.ker f = ⊥<VAR>hsurj : LinearMap.range f = ⊤<VAR>y : F<GOAL>f ((ContinuousLinearEquiv.ofBijective f hinj hsurj).symm y) = y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>f : E →L[𝕜] E<GOAL>IsUnit f ↔ Function.Bijective ⇑f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_5<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E →L[𝕜] F<VAR>G : Submodule 𝕜 F<VAR>h : IsCompl (LinearMap.range f) G<VAR>CompleteSpace ↥G<VAR>hker : LinearMap.ker f = ⊥<GOAL>LinearMap.range f = Submodule.map (↑↑(f.coprodSubtypeLEquivOfIsCompl h hker)) (⊤.prod ⊥)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_5<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : E →L[𝕜] F<VAR>G : Submodule 𝕜 F<VAR>h : IsCompl (LinearMap.range f) G<VAR>hG : IsClosed ↑G<VAR>hker : LinearMap.ker f = ⊥<GOAL>IsClosed ↑(LinearMap.range f)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_5<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : IsClosed ↑g.graph<GOAL>Continuous ⇑g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_5<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : ∀ (u : ℕ → E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (𝓝 x) → Filter.Tendsto (⇑g ∘ u) Filter.atTop (𝓝 y) → y = g x<GOAL>Continuous ⇑g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_5<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : IsClosed ↑g.graph<GOAL>⇑(ContinuousLinearMap.ofIsClosedGraph hg) = ⇑g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_5<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : IsClosed ↑g.graph<GOAL>↑(ContinuousLinearMap.ofIsClosedGraph hg) = g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_5<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : ∀ (u : ℕ → E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (𝓝 x) → Filter.Tendsto (⇑g ∘ u) Filter.atTop (𝓝 y) → y = g x<GOAL>⇑(ContinuousLinearMap.ofSeqClosedGraph hg) = ⇑g
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>CompleteSpace E<VAR>F : Type u_5<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : ∀ (u : ℕ → E) (x : E) (y : F), Filter.Tendsto u Filter.atTop (𝓝 x) → Filter.Tendsto (⇑g ∘ u) Filter.atTop (𝓝 y) → y = g x<GOAL>↑(ContinuousLinearMap.ofSeqClosedGraph hg) = g
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>RingHomInvPair σ σ'<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜' F<VAR>CompleteSpace E<VAR>f : E →SL[σ] F<VAR>c : ℝ≥0<VAR>hf : AntilipschitzWith c ⇑f<GOAL>(LinearMap.range f).topologicalClosure = LinearMap.range f