Theorems · Theorem · potential theory

InnerProductSpace.HarmonicAt.eventually

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {x : E},
  InnerProductSpace.HarmonicAt f x → ∀ᶠ (y : E) in nhds x, InnerProductSpace.HarmonicAt f y

If f is harmonic at x, then it is harmonic at all points in a neighborhood of x.

Defined in: Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 244 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup InnerProductSpace FiniteDimensional NormedAddCommGroup NormedSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
NormedSpacestatement and proof · cited by 12,499
Top.topproof · cited by 9,680
nhdsstatement and proof · cited by 5,554
InnerProductSpacestatement and proof · cited by 3,523
Filter.Eventuallystatement and proof · cited by 3,134
FiniteDimensionalstatement and proof · cited by 1,854
Filter.univ_mem'proof · cited by 1,672
Filter.mp_memproof · cited by 1,537
ContDiffAtproof · cited by 262
Laplacian.laplacianproof · cited by 40

Cited by1

Results whose statement or proof uses this declaration.

InnerProductSpace.isOpen_setOfPred_harmonicAtproof · cited by 5