Loogle!
Result
Found 50 definitions mentioning ContinuousLinearMap, IsOpen, RingHom.id and Semiring.toNonAssocSemiring. Of these, 50 match your pattern(s).
- ContinuousLinearEquiv.isOpen Mathlib.Analysis.NormedSpace.BoundedLinearMaps
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] [inst_5 : CompleteSpace E], IsOpen (Set.range ContinuousLinearEquiv.toContinuousLinearMap) - isOpen_setOf_nat_le_rank Mathlib.Analysis.NormedSpace.FiniteDimension
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] [inst_5 : CompleteSpace π] (n : β), IsOpen {f | βn β€ f.rank} - ContinuousLinearMap.isOpen_injective Mathlib.Analysis.NormedSpace.FiniteDimension
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type v} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] [inst_5 : CompleteSpace π] [inst_6 : FiniteDimensional π E], IsOpen {L | Function.Injective βL} - geometric_hahn_banach_open_point Mathlib.Analysis.NormedSpace.HahnBanach.Separation
β {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : TopologicalAddGroup E] [inst_3 : Module β E] [inst_4 : ContinuousSMul β E] {s : Set E} {x : E}, Convex β s β IsOpen s β x β s β β f, β a β s, f a < f x - geometric_hahn_banach_point_open Mathlib.Analysis.NormedSpace.HahnBanach.Separation
β {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : TopologicalAddGroup E] [inst_3 : Module β E] [inst_4 : ContinuousSMul β E] {t : Set E} {x : E}, Convex β t β IsOpen t β x β t β β f, β b β t, f x < f b - separate_convex_open_set Mathlib.Analysis.NormedSpace.HahnBanach.Separation
β {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : TopologicalAddGroup E] [inst_3 : Module β E] [inst_4 : ContinuousSMul β E] {s : Set E}, 0 β s β Convex β s β IsOpen s β β {xβ : E}, xβ β s β β f, f xβ = 1 β§ β x β s, f x < 1 - geometric_hahn_banach_open Mathlib.Analysis.NormedSpace.HahnBanach.Separation
β {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : TopologicalAddGroup E] [inst_3 : Module β E] [inst_4 : ContinuousSMul β E] {s t : Set E}, Convex β s β IsOpen s β Convex β t β Disjoint s t β β f u, (β a β s, f a < u) β§ β b β t, u β€ f b - geometric_hahn_banach_open_open Mathlib.Analysis.NormedSpace.HahnBanach.Separation
β {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : TopologicalAddGroup E] [inst_3 : Module β E] [inst_4 : ContinuousSMul β E] {s t : Set E}, Convex β s β IsOpen s β Convex β t β IsOpen t β Disjoint s t β β f u, (β a β s, f a < u) β§ β b β t, u < f b - fderivWithin_of_isOpen Mathlib.Analysis.Calculus.FDeriv.Basic
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F} {x : E} {s : Set E}, IsOpen s β x β s β fderivWithin π f s x = fderiv π f x - hasFDerivWithinAt_of_isOpen Mathlib.Analysis.Calculus.FDeriv.Basic
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : Set E}, IsOpen s β x β s β (HasFDerivWithinAt f f' s x β HasFDerivAt f f' x) - ContDiffOn.continuousOn_fderiv_of_isOpen Mathlib.Analysis.Calculus.ContDiff.Defs
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E} {f : E β F} {n : ββ}, ContDiffOn π n f s β IsOpen s β 1 β€ n β ContinuousOn (fun x => fderiv π f x) s - contDiffOn_top_iff_fderiv_of_isOpen Mathlib.Analysis.Calculus.ContDiff.Defs
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E} {f : E β F}, IsOpen s β (ContDiffOn π β€ f s β DifferentiableOn π f s β§ ContDiffOn π β€ (fun y => fderiv π f y) s) - contDiffOn_succ_iff_fderiv_of_isOpen Mathlib.Analysis.Calculus.ContDiff.Defs
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E} {f : E β F} {n : β}, IsOpen s β (ContDiffOn π (β(n + 1)) f s β DifferentiableOn π f s β§ ContDiffOn π (βn) (fun y => fderiv π f y) s) - ContDiffOn.fderiv_of_isOpen Mathlib.Analysis.Calculus.ContDiff.Defs
β {π : Type u} [inst : NontriviallyNormedField π] {E : Type uE} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {s : Set E} {f : E β F} {m n : ββ}, ContDiffOn π n f s β IsOpen s β m + 1 β€ n β ContDiffOn π m (fun y => fderiv π f y) s - FDerivMeasurableAux.isOpen_A Mathlib.Analysis.Calculus.FDeriv.Measurable
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F} (L : E βL[π] F) (r Ξ΅ : β), IsOpen (FDerivMeasurableAux.A f L r Ξ΅) - FDerivMeasurableAux.isOpen_B Mathlib.Analysis.Calculus.FDeriv.Measurable
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F} {K : Set (E βL[π] F)} {r s Ξ΅ : β}, IsOpen (FDerivMeasurableAux.B f K r s Ξ΅) - FDerivMeasurableAux.isOpen_A_with_param Mathlib.Analysis.Calculus.FDeriv.Measurable
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] [inst_3 : LocallyCompactSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace π F] {Ξ± : Type u_4} [inst_6 : TopologicalSpace Ξ±] {f : Ξ± β E β F} {r s : β}, Continuous (Function.uncurry f) β β (L : E βL[π] F), IsOpen {p | p.2 β FDerivMeasurableAux.A (f p.1) L r s} - FDerivMeasurableAux.isOpen_B_with_param Mathlib.Analysis.Calculus.FDeriv.Measurable
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] [inst_3 : LocallyCompactSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace π F] {Ξ± : Type u_4} [inst_6 : TopologicalSpace Ξ±] {f : Ξ± β E β F} {r s t : β}, Continuous (Function.uncurry f) β β (K : Set (E βL[π] F)), IsOpen {p | p.2 β FDerivMeasurableAux.B (f p.1) K r s t} - WeakSpace.isOpen_of_isOpen Mathlib.Topology.Algebra.Module.WeakDual
β {π : Type u_2} {E : Type u_5} [inst : CommSemiring π] [inst_1 : TopologicalSpace π] [inst_2 : ContinuousAdd π] [inst_3 : ContinuousConstSMul π π] [inst_4 : AddCommMonoid E] [inst_5 : Module π E] [inst_6 : TopologicalSpace E] (V : Set E), IsOpen (β(continuousLinearMapToWeakSpace π E) '' V) β IsOpen V - MeasureTheory.contDiffOn_convolution_right_with_param_comp Mathlib.Analysis.Convolution
β {π : Type uπ} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike π] [inst_4 : NormedSpace π E] [inst_5 : NormedSpace π E'] [inst_6 : NormedSpace β F] [inst_7 : NormedSpace π F] [inst_8 : CompleteSpace F] [inst_9 : MeasurableSpace G] [inst_10 : NormedAddCommGroup G] [inst_11 : BorelSpace G] [inst_12 : NormedSpace π G] [inst_13 : NormedAddCommGroup P] [inst_14 : NormedSpace π P] {ΞΌ : MeasureTheory.Measure G} {n : ββ} (L : E βL[π] E' βL[π] F) {s : Set P} {v : P β G}, ContDiffOn π n v s β β {f : G β E} {g : P β G β E'} {k : Set G}, IsOpen s β IsCompact k β (β (p : P) (x : G), p β s β x β k β g p x = 0) β MeasureTheory.LocallyIntegrable f ΞΌ β ContDiffOn π n (βΏg) (s ΓΛ’ Set.univ) β ContDiffOn π n (fun x => MeasureTheory.convolution f (g x) L ΞΌ (v x)) s - MeasureTheory.contDiffOn_convolution_right_with_param Mathlib.Analysis.Convolution
β {π : Type uπ} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike π] [inst_4 : NormedSpace π E] [inst_5 : NormedSpace π E'] [inst_6 : NormedSpace β F] [inst_7 : NormedSpace π F] [inst_8 : CompleteSpace F] [inst_9 : MeasurableSpace G] [inst_10 : NormedAddCommGroup G] [inst_11 : BorelSpace G] [inst_12 : NormedSpace π G] [inst_13 : NormedAddCommGroup P] [inst_14 : NormedSpace π P] {ΞΌ : MeasureTheory.Measure G} {f : G β E} {n : ββ} (L : E βL[π] E' βL[π] F) {g : P β G β E'} {s : Set P} {k : Set G}, IsOpen s β IsCompact k β (β (p : P) (x : G), p β s β x β k β g p x = 0) β MeasureTheory.LocallyIntegrable f ΞΌ β ContDiffOn π n (βΏg) (s ΓΛ’ Set.univ) β ContDiffOn π n (fun q => MeasureTheory.convolution f (g q.1) L ΞΌ q.2) (s ΓΛ’ Set.univ) - MeasureTheory.contDiffOn_convolution_right_with_param_aux Mathlib.Analysis.Convolution
β {π : Type uπ} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : RCLike π] [inst_2 : NormedSpace π E] {G E' F P : Type uP} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace π E'] [inst_6 : NormedSpace β F] [inst_7 : NormedSpace π F] [inst_8 : CompleteSpace F] [inst_9 : MeasurableSpace G] {ΞΌ : MeasureTheory.Measure G} [inst_10 : NormedAddCommGroup G] [inst_11 : BorelSpace G] [inst_12 : NormedSpace π G] [inst_13 : NormedAddCommGroup P] [inst_14 : NormedSpace π P] {f : G β E} {n : ββ} (L : E βL[π] E' βL[π] F) {g : P β G β E'} {s : Set P} {k : Set G}, IsOpen s β IsCompact k β (β (p : P) (x : G), p β s β x β k β g p x = 0) β MeasureTheory.LocallyIntegrable f ΞΌ β ContDiffOn π n (βΏg) (s ΓΛ’ Set.univ) β ContDiffOn π n (fun q => MeasureTheory.convolution f (g q.1) L ΞΌ q.2) (s ΓΛ’ Set.univ) - MeasureTheory.contDiffOn_convolution_left_with_param_comp Mathlib.Analysis.Convolution
β {π : Type uπ} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike π] [inst_4 : NormedSpace π E] [inst_5 : NormedSpace π E'] [inst_6 : NormedSpace β F] [inst_7 : NormedSpace π F] [inst_8 : CompleteSpace F] [inst_9 : MeasurableSpace G] [inst_10 : NormedAddCommGroup G] [inst_11 : BorelSpace G] [inst_12 : NormedSpace π G] [inst_13 : NormedAddCommGroup P] [inst_14 : NormedSpace π P] {ΞΌ : MeasureTheory.Measure G} [inst_15 : ΞΌ.IsAddLeftInvariant] [inst_16 : ΞΌ.IsNegInvariant] (L : E' βL[π] E βL[π] F) {s : Set P} {n : ββ} {v : P β G}, ContDiffOn π n v s β β {f : G β E} {g : P β G β E'} {k : Set G}, IsOpen s β IsCompact k β (β (p : P) (x : G), p β s β x β k β g p x = 0) β MeasureTheory.LocallyIntegrable f ΞΌ β ContDiffOn π n (βΏg) (s ΓΛ’ Set.univ) β ContDiffOn π n (fun x => MeasureTheory.convolution (g x) f L ΞΌ (v x)) s - MeasureTheory.contDiffOn_convolution_left_with_param Mathlib.Analysis.Convolution
β {π : Type uπ} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike π] [inst_4 : NormedSpace π E] [inst_5 : NormedSpace π E'] [inst_6 : NormedSpace β F] [inst_7 : NormedSpace π F] [inst_8 : CompleteSpace F] [inst_9 : MeasurableSpace G] [inst_10 : NormedAddCommGroup G] [inst_11 : BorelSpace G] [inst_12 : NormedSpace π G] [inst_13 : NormedAddCommGroup P] [inst_14 : NormedSpace π P] {ΞΌ : MeasureTheory.Measure G} [inst_15 : ΞΌ.IsAddLeftInvariant] [inst_16 : ΞΌ.IsNegInvariant] (L : E' βL[π] E βL[π] F) {f : G β E} {n : ββ} {g : P β G β E'} {s : Set P} {k : Set G}, IsOpen s β IsCompact k β (β (p : P) (x : G), p β s β x β k β g p x = 0) β MeasureTheory.LocallyIntegrable f ΞΌ β ContDiffOn π n (βΏg) (s ΓΛ’ Set.univ) β ContDiffOn π n (fun q => MeasureTheory.convolution (g q.1) f L ΞΌ q.2) (s ΓΛ’ Set.univ) - MeasureTheory.hasFDerivAt_convolution_right_with_param Mathlib.Analysis.Convolution
β {π : Type uπ} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G β E} [inst_3 : RCLike π] [inst_4 : NormedSpace π E] [inst_5 : NormedSpace π E'] [inst_6 : NormedSpace β F] [inst_7 : NormedSpace π F] [inst_8 : MeasurableSpace G] [inst_9 : NormedAddCommGroup G] [inst_10 : BorelSpace G] [inst_11 : NormedSpace π G] [inst_12 : NormedAddCommGroup P] [inst_13 : NormedSpace π P] {ΞΌ : MeasureTheory.Measure G} (L : E βL[π] E' βL[π] F) {g : P β G β E'} {s : Set P} {k : Set G}, IsOpen s β IsCompact k β (β (p : P) (x : G), p β s β x β k β g p x = 0) β MeasureTheory.LocallyIntegrable f ΞΌ β ContDiffOn π 1 (βΏg) (s ΓΛ’ Set.univ) β β (qβ : P Γ G), qβ.1 β s β HasFDerivAt (fun q => MeasureTheory.convolution f (g q.1) L ΞΌ q.2) (MeasureTheory.convolution f (fun x => fderiv π (βΏg) (qβ.1, x)) (ContinuousLinearMap.precompR (P Γ G) L) ΞΌ qβ.2) qβ - cauchy_map_of_uniformCauchySeqOn_fderiv Mathlib.Analysis.Calculus.UniformLimitsDeriv
β {ΞΉ : Type u_1} {l : Filter ΞΉ} {E : Type u_2} [inst : NormedAddCommGroup E] {π : Type u_3} [inst_1 : RCLike π] [inst_2 : NormedSpace π E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace π G] {f : ΞΉ β E β G} {f' : ΞΉ β E β E βL[π] G} {s : Set E}, IsOpen s β IsPreconnected s β UniformCauchySeqOn f' l s β (β (n : ΞΉ), β y β s, HasFDerivAt (f n) (f' n y) y) β β {xβ x : E}, xβ β s β x β s β Cauchy (Filter.map (fun n => f n xβ) l) β Cauchy (Filter.map (fun n => f n x) l) - hasFDerivAt_of_tendstoUniformlyOn Mathlib.Analysis.Calculus.UniformLimitsDeriv
β {ΞΉ : Type u_1} {l : Filter ΞΉ} {E : Type u_2} [inst : NormedAddCommGroup E] {π : Type u_3} [inst_1 : RCLike π] [inst_2 : NormedSpace π E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace π G] {f : ΞΉ β E β G} {g : E β G} {f' : ΞΉ β E β E βL[π] G} {g' : E β E βL[π] G} [inst_5 : l.NeBot] {s : Set E}, IsOpen s β TendstoUniformlyOn f' g' l s β (β (n : ΞΉ), β x β s, HasFDerivAt (f n) (f' n x) x) β (β x β s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) β β x β s, HasFDerivAt g (g' x) x - hasFDerivAt_of_tendstoLocallyUniformlyOn Mathlib.Analysis.Calculus.UniformLimitsDeriv
β {ΞΉ : Type u_1} {l : Filter ΞΉ} {E : Type u_2} [inst : NormedAddCommGroup E] {π : Type u_3} [inst_1 : RCLike π] [inst_2 : NormedSpace π E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace π G] {f : ΞΉ β E β G} {g : E β G} {f' : ΞΉ β E β E βL[π] G} {g' : E β E βL[π] G} {x : E} [inst_5 : l.NeBot] {s : Set E}, IsOpen s β TendstoLocallyUniformlyOn f' g' l s β (β (n : ΞΉ), β x β s, HasFDerivAt (f n) (f' n x) x) β (β x β s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) β x β s β HasFDerivAt g (g' x) x - hasFDerivAt_of_tendsto_locally_uniformly_on' Mathlib.Analysis.Calculus.UniformLimitsDeriv
β {ΞΉ : Type u_1} {l : Filter ΞΉ} {E : Type u_2} [inst : NormedAddCommGroup E] {π : Type u_3} [inst_1 : RCLike π] [inst_2 : NormedSpace π E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace π G] {f : ΞΉ β E β G} {g : E β G} {g' : E β E βL[π] G} {x : E} [inst_5 : l.NeBot] {s : Set E}, IsOpen s β TendstoLocallyUniformlyOn (fderiv π β f) g' l s β (β (n : ΞΉ), DifferentiableOn π (f n) s) β (β x β s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) β x β s β HasFDerivAt g (g' x) x - summable_of_summable_hasFDerivAt_of_isPreconnected Mathlib.Analysis.Calculus.SmoothSeries
β {Ξ± : Type u_1} {π : Type u_3} {E : Type u_4} {F : Type u_5} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] [inst_3 : NormedAddCommGroup F] [inst_4 : CompleteSpace F] {u : Ξ± β β} [inst_5 : NormedSpace π F] {f : Ξ± β E β F} {f' : Ξ± β E β E βL[π] F} {s : Set E} {xβ x : E}, Summable u β IsOpen s β IsPreconnected s β (β (n : Ξ±), β x β s, HasFDerivAt (f n) (f' n x) x) β (β (n : Ξ±), β x β s, βf' n xβ β€ u n) β xβ β s β (Summable fun x => f x xβ) β x β s β Summable fun n => f n x - hasFDerivAt_tsum_of_isPreconnected Mathlib.Analysis.Calculus.SmoothSeries
β {Ξ± : Type u_1} {π : Type u_3} {E : Type u_4} {F : Type u_5} [inst : RCLike π] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] [inst_3 : NormedAddCommGroup F] [inst_4 : CompleteSpace F] {u : Ξ± β β} [inst_5 : NormedSpace π F] {f : Ξ± β E β F} {f' : Ξ± β E β E βL[π] F} {s : Set E} {xβ x : E}, Summable u β IsOpen s β IsPreconnected s β (β (n : Ξ±), β x β s, HasFDerivAt (f n) (f' n x) x) β (β (n : Ξ±), β x β s, βf' n xβ β€ u n) β xβ β s β (Summable fun n => f n xβ) β x β s β HasFDerivAt (fun y => β' (n : Ξ±), f n y) (β' (n : Ξ±), f' n x) x - has_fderiv_at_boundary_of_tendsto_fderiv Mathlib.Analysis.Calculus.FDeriv.Extend
β {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace β E] {F : Type u_2} [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace β F] {f : E β F} {s : Set E} {x : E} {f' : E βL[β] F}, DifferentiableOn β f s β Convex β s β IsOpen s β (β y β closure s, ContinuousWithinAt f s y) β Filter.Tendsto (fun y => fderiv β f y) (nhdsWithin x s) (nhds f') β HasFDerivWithinAt f f' (closure s) x - ApproximatesLinearOn.open_image Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] [inst_5 : CompleteSpace E] {f : E β F} {s : Set E} {c : NNReal} {f' : E βL[π] F}, ApproximatesLinearOn f f' s c β β (f'symm : f'.NonlinearRightInverse), IsOpen s β Subsingleton F β¨ c < f'symm.nnnormβ»ΒΉ β IsOpen (f '' s) - ApproximatesLinearOn.toPartialHomeomorph Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
{π : Type u_1} β [inst : NontriviallyNormedField π] β {E : Type u_2} β [inst_1 : NormedAddCommGroup E] β [inst_2 : NormedSpace π E] β {F : Type u_3} β [inst_3 : NormedAddCommGroup F] β [inst_4 : NormedSpace π F] β [inst_5 : CompleteSpace E] β (f : E β F) β {f' : E βL[π] F} β (s : Set E) β {c : NNReal} β ApproximatesLinearOn f (βf') s c β Subsingleton E β¨ c < ββf'.symmβββ»ΒΉ β IsOpen s β PartialHomeomorph E F - ApproximatesLinearOn.toPartialHomeomorph_coe Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] [inst_5 : CompleteSpace E] (f : E β F) {f' : E βL[π] F} (s : Set E) {c : NNReal} (hf : ApproximatesLinearOn f (βf') s c) (hc : Subsingleton E β¨ c < ββf'.symmβββ»ΒΉ) (hs : IsOpen s), β(ApproximatesLinearOn.toPartialHomeomorph f s hf hc hs) = f - ApproximatesLinearOn.toPartialHomeomorph_source Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] [inst_5 : CompleteSpace E] (f : E β F) {f' : E βL[π] F} (s : Set E) {c : NNReal} (hf : ApproximatesLinearOn f (βf') s c) (hc : Subsingleton E β¨ c < ββf'.symmβββ»ΒΉ) (hs : IsOpen s), (ApproximatesLinearOn.toPartialHomeomorph f s hf hc hs).source = s - ApproximatesLinearOn.toPartialHomeomorph_target Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] [inst_5 : CompleteSpace E] (f : E β F) {f' : E βL[π] F} (s : Set E) {c : NNReal} (hf : ApproximatesLinearOn f (βf') s c) (hc : Subsingleton E β¨ c < ββf'.symmβββ»ΒΉ) (hs : IsOpen s), (ApproximatesLinearOn.toPartialHomeomorph f s hf hc hs).target = f '' s - ApproximatesLinearOn.closedBall_subset_target Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {Ξ΅ : β} [inst_5 : CompleteSpace E] {f : E β F} {f' : E βL[π] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f (βf') s c) (hc : Subsingleton E β¨ c < ββf'.symmβββ»ΒΉ) (hs : IsOpen s) {b : E}, 0 β€ Ξ΅ β Metric.closedBall b Ξ΅ β s β Metric.closedBall (f b) ((βββf'.symmβββ»ΒΉ - βc) * Ξ΅) β (ApproximatesLinearOn.toPartialHomeomorph f s hf hc hs).target - HasStrictFDerivAt.approximates_deriv_on_open_nhds Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace π F] {f : E β F} {f' : E βL[π] F} {a : E}, HasStrictFDerivAt f (βf') a β β s, a β s β§ IsOpen s β§ ApproximatesLinearOn f (βf') s (ββf'.symmβββ»ΒΉ / 2) - FiberwiseLinear.partialHomeomorph Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
{π : Type u_1} β {B : Type u_2} β {F : Type u_3} β [inst : TopologicalSpace B] β [inst_1 : NontriviallyNormedField π] β [inst_2 : NormedAddCommGroup F] β [inst_3 : NormedSpace π F] β {U : Set B} β (Ο : B β F βL[π] F) β IsOpen U β ContinuousOn (fun x => β(Ο x)) U β ContinuousOn (fun x => β(Ο x).symm) U β PartialHomeomorph (B Γ F) (B Γ F) - FiberwiseLinear.source_trans_partialHomeomorph Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
β {π : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField π] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace π F] {Ο Ο' : B β F βL[π] F} {U U' : Set B} (hU : IsOpen U) (hΟ : ContinuousOn (fun x => β(Ο x)) U) (h2Ο : ContinuousOn (fun x => β(Ο x).symm) U) (hU' : IsOpen U') (hΟ' : ContinuousOn (fun x => β(Ο' x)) U') (h2Ο' : ContinuousOn (fun x => β(Ο' x).symm) U'), ((FiberwiseLinear.partialHomeomorph Ο hU hΟ h2Ο).trans (FiberwiseLinear.partialHomeomorph Ο' hU' hΟ' h2Ο')).source = (U β© U') ΓΛ’ Set.univ - FiberwiseLinear.target_trans_partialHomeomorph Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
β {π : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField π] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace π F] {Ο Ο' : B β F βL[π] F} {U U' : Set B} (hU : IsOpen U) (hΟ : ContinuousOn (fun x => β(Ο x)) U) (h2Ο : ContinuousOn (fun x => β(Ο x).symm) U) (hU' : IsOpen U') (hΟ' : ContinuousOn (fun x => β(Ο' x)) U') (h2Ο' : ContinuousOn (fun x => β(Ο' x).symm) U'), ((FiberwiseLinear.partialHomeomorph Ο hU hΟ h2Ο).trans (FiberwiseLinear.partialHomeomorph Ο' hU' hΟ' h2Ο')).target = (U β© U') ΓΛ’ Set.univ - FiberwiseLinear.trans_partialHomeomorph_apply Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
β {π : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField π] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace π F] {Ο Ο' : B β F βL[π] F} {U U' : Set B} (hU : IsOpen U) (hΟ : ContinuousOn (fun x => β(Ο x)) U) (h2Ο : ContinuousOn (fun x => β(Ο x).symm) U) (hU' : IsOpen U') (hΟ' : ContinuousOn (fun x => β(Ο' x)) U') (h2Ο' : ContinuousOn (fun x => β(Ο' x).symm) U') (b : B) (v : F), β((FiberwiseLinear.partialHomeomorph Ο hU hΟ h2Ο).trans (FiberwiseLinear.partialHomeomorph Ο' hU' hΟ' h2Ο')) (b, v) = (b, (Ο' b) ((Ο b) v)) - mem_smoothFiberwiseLinear_iff Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
β {π : Type u_1} (B : Type u_2) (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField π] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace π F] {EB : Type u_4} [inst_4 : NormedAddCommGroup EB] [inst_5 : NormedSpace π EB] {HB : Type u_5} [inst_6 : TopologicalSpace HB] [inst_7 : ChartedSpace HB B] (IB : ModelWithCorners π EB HB) (e : PartialHomeomorph (B Γ F) (B Γ F)), e β smoothFiberwiseLinear B F IB β β Ο U, β (hU : IsOpen U) (hΟ : SmoothOn IB (modelWithCornersSelf π (F βL[π] F)) (fun x => β(Ο x)) U) (h2Ο : SmoothOn IB (modelWithCornersSelf π (F βL[π] F)) (fun x => β(Ο x).symm) U), e.EqOnSource (FiberwiseLinear.partialHomeomorph Ο hU β― β―) - SmoothFiberwiseLinear.locality_auxβ Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
β {π : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField π] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace π F] {EB : Type u_4} [inst_4 : NormedAddCommGroup EB] [inst_5 : NormedSpace π EB] {HB : Type u_5} [inst_6 : TopologicalSpace HB] [inst_7 : ChartedSpace HB B] {IB : ModelWithCorners π EB HB} (e : PartialHomeomorph (B Γ F) (B Γ F)) (U : Set B), e.source = U ΓΛ’ Set.univ β (β x β U, β Ο u, β (hu : IsOpen u) (_ : u β U) (_ : x β u) (hΟ : SmoothOn IB (modelWithCornersSelf π (F βL[π] F)) (fun x => β(Ο x)) u) (h2Ο : SmoothOn IB (modelWithCornersSelf π (F βL[π] F)) (fun x => β(Ο x).symm) u), (e.restr (u ΓΛ’ Set.univ)).EqOnSource (FiberwiseLinear.partialHomeomorph Ο hu β― β―)) β β Ξ¦ U, β (hUβ : IsOpen U) (hΞ¦ : SmoothOn IB (modelWithCornersSelf π (F βL[π] F)) (fun x => β(Ξ¦ x)) U) (h2Ξ¦ : SmoothOn IB (modelWithCornersSelf π (F βL[π] F)) (fun x => β(Ξ¦ x).symm) U), e.EqOnSource (FiberwiseLinear.partialHomeomorph Ξ¦ hUβ β― β―) - SmoothFiberwiseLinear.locality_auxβ Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
β {π : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField π] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace π F] {EB : Type u_4} [inst_4 : NormedAddCommGroup EB] [inst_5 : NormedSpace π EB] {HB : Type u_5} [inst_6 : TopologicalSpace HB] [inst_7 : ChartedSpace HB B] {IB : ModelWithCorners π EB HB} (e : PartialHomeomorph (B Γ F) (B Γ F)), (β p β e.source, β s, IsOpen s β§ p β s β§ β Ο u, β (hu : IsOpen u) (hΟ : SmoothOn IB (modelWithCornersSelf π (F βL[π] F)) (fun x => β(Ο x)) u) (h2Ο : SmoothOn IB (modelWithCornersSelf π (F βL[π] F)) (fun x => β(Ο x).symm) u), (e.restr s).EqOnSource (FiberwiseLinear.partialHomeomorph Ο hu β― β―)) β β U, e.source = U ΓΛ’ Set.univ β§ β x β U, β Ο u, β (hu : IsOpen u) (_ : u β U) (_ : x β u) (hΟ : SmoothOn IB (modelWithCornersSelf π (F βL[π] F)) (fun x => β(Ο x)) u) (h2Ο : SmoothOn IB (modelWithCornersSelf π (F βL[π] F)) (fun x => β(Ο x).symm) u), (e.restr (u ΓΛ’ Set.univ)).EqOnSource (FiberwiseLinear.partialHomeomorph Ο hu β― β―) - VectorBundleCore.mk Mathlib.Topology.VectorBundle.Basic
{R : Type u_1} β {B : Type u_2} β {F : Type u_3} β [inst : NontriviallyNormedField R] β [inst_1 : NormedAddCommGroup F] β [inst_2 : NormedSpace R F] β [inst_3 : TopologicalSpace B] β {ΞΉ : Type u_5} β (baseSet : ΞΉ β Set B) β (β (i : ΞΉ), IsOpen (baseSet i)) β (indexAt : B β ΞΉ) β (β (x : B), x β baseSet (indexAt x)) β (coordChange : ΞΉ β ΞΉ β B β F βL[R] F) β (β (i : ΞΉ), β x β baseSet i, β (v : F), (coordChange i i x) v = v) β (β (i j : ΞΉ), ContinuousOn (coordChange i j) (baseSet i β© baseSet j)) β (β (i j k : ΞΉ), β x β baseSet i β© baseSet j β© baseSet k, β (v : F), (coordChange j k x) ((coordChange i j x) v) = (coordChange i k x) v) β VectorBundleCore R B F ΞΉ - VectorBundleCore.mk.sizeOf_spec Mathlib.Topology.VectorBundle.Basic
β {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ΞΉ : Type u_5} [inst_4 : SizeOf R] [inst_5 : SizeOf B] [inst_6 : SizeOf F] [inst_7 : SizeOf ΞΉ] (baseSet : ΞΉ β Set B) (isOpen_baseSet : β (i : ΞΉ), IsOpen (baseSet i)) (indexAt : B β ΞΉ) (mem_baseSet_at : β (x : B), x β baseSet (indexAt x)) (coordChange : ΞΉ β ΞΉ β B β F βL[R] F) (coordChange_self : β (i : ΞΉ), β x β baseSet i, β (v : F), (coordChange i i x) v = v) (continuousOn_coordChange : β (i j : ΞΉ), ContinuousOn (coordChange i j) (baseSet i β© baseSet j)) (coordChange_comp : β (i j k : ΞΉ), β x β baseSet i β© baseSet j β© baseSet k, β (v : F), (coordChange j k x) ((coordChange i j x) v) = (coordChange i k x) v), sizeOf { baseSet := baseSet, isOpen_baseSet := isOpen_baseSet, indexAt := indexAt, mem_baseSet_at := mem_baseSet_at, coordChange := coordChange, coordChange_self := coordChange_self, continuousOn_coordChange := continuousOn_coordChange, coordChange_comp := coordChange_comp } = 1 - VectorBundleCore.mk.injEq Mathlib.Topology.VectorBundle.Basic
β {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ΞΉ : Type u_5} (baseSet : ΞΉ β Set B) (isOpen_baseSet : β (i : ΞΉ), IsOpen (baseSet i)) (indexAt : B β ΞΉ) (mem_baseSet_at : β (x : B), x β baseSet (indexAt x)) (coordChange : ΞΉ β ΞΉ β B β F βL[R] F) (coordChange_self : β (i : ΞΉ), β x β baseSet i, β (v : F), (coordChange i i x) v = v) (continuousOn_coordChange : β (i j : ΞΉ), ContinuousOn (coordChange i j) (baseSet i β© baseSet j)) (coordChange_comp : β (i j k : ΞΉ), β x β baseSet i β© baseSet j β© baseSet k, β (v : F), (coordChange j k x) ((coordChange i j x) v) = (coordChange i k x) v) (baseSet_1 : ΞΉ β Set B) (isOpen_baseSet_1 : β (i : ΞΉ), IsOpen (baseSet_1 i)) (indexAt_1 : B β ΞΉ) (mem_baseSet_at_1 : β (x : B), x β baseSet_1 (indexAt_1 x)) (coordChange_1 : ΞΉ β ΞΉ β B β F βL[R] F) (coordChange_self_1 : β (i : ΞΉ), β x β baseSet_1 i, β (v : F), (coordChange_1 i i x) v = v) (continuousOn_coordChange_1 : β (i j : ΞΉ), ContinuousOn (coordChange_1 i j) (baseSet_1 i β© baseSet_1 j)) (coordChange_comp_1 : β (i j k : ΞΉ), β x β baseSet_1 i β© baseSet_1 j β© baseSet_1 k, β (v : F), (coordChange_1 j k x) ((coordChange_1 i j x) v) = (coordChange_1 i k x) v), ({ baseSet := baseSet, isOpen_baseSet := isOpen_baseSet, indexAt := indexAt, mem_baseSet_at := mem_baseSet_at, coordChange := coordChange, coordChange_self := coordChange_self, continuousOn_coordChange := continuousOn_coordChange, coordChange_comp := coordChange_comp } = { baseSet := baseSet_1, isOpen_baseSet := isOpen_baseSet_1, indexAt := indexAt_1, mem_baseSet_at := mem_baseSet_at_1, coordChange := coordChange_1, coordChange_self := coordChange_self_1, continuousOn_coordChange := continuousOn_coordChange_1, coordChange_comp := coordChange_comp_1 }) = (baseSet = baseSet_1 β§ indexAt = indexAt_1 β§ coordChange = coordChange_1) - mfderivWithin_of_isOpen Mathlib.Geometry.Manifold.MFDeriv.Basic
β {π : Type u_1} [inst : NontriviallyNormedField π] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace π E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners π E H} {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E'] [inst_7 : NormedSpace π E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners π E' H'} {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M β M'} {x : M} {s : Set M} [Is : SmoothManifoldWithCorners I M] [I's : SmoothManifoldWithCorners I' M'], IsOpen s β x β s β mfderivWithin I I' f s x = mfderiv I I' f x
Did you maybe mean
About
Loogle searches of Lean and Mathlib definitions and theorems.
You may also want to try the CLI version, the VS
Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
πReal.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
π"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.By subexpression:
π_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
πReal.sqrt ?a * Real.sqrt ?a
If the pattern has parameters, they are matched in any order. Both of these will find
List.map
:
π(?a -> ?b) -> List ?a -> List ?b
πList ?a -> (?a -> ?b) -> List ?b
By main conclusion:
π|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of allβ
andβ
) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
π|- _ < _ β tsum _ < tsum _
will findtsum_lt_tsum
even though the hypothesisf i < g i
is not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
π Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ β _
woould find all lemmas which mention the constants Real.sin
and tsum
, have "two"
as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _
(if
there were any such lemmas). Metavariables (?a
) are
assigned independently in each filter.
The #lucky
button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is currently provided by Joachim Breitner <mail@joachim-breitner.de>.
This is Loogle revision fa2ddf5
serving mathlib revision 38aa2fc