Theorem ContDiffAt.laplacianWithin_sub_nhdsWithin

Modification history

2026-02-25 19:11
Mathlib/Analysis/InnerProductSpace/Laplacian.lean
feat: introduce `HarmonicContOnCl` (#35564) …
Added ContDiffAt.laplacianWithin_sub_nhdsWithinView on Github →