Skip to content

Commit cfb4670

Browse files
committed
docs(Analysis.Analytic.IsolatedZeros): Fix name of referenced theorem (leanprover-community#30433)
Fix the docstring for AnalyticOnNhd.preimage_mem_codiscreteWithin, the theorem to see also was missing "mem" in its name.
1 parent 3da7809 commit cfb4670

1 file changed

Lines changed: 2 additions & 2 deletions

File tree

Mathlib/Analysis/Analytic/IsolatedZeros.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -342,8 +342,8 @@ theorem AnalyticAt.map_nhdsNE {x : 𝕜} {f : 𝕜 → E} (hfx : AnalyticAt 𝕜
342342
Preimages of codiscrete sets: if `f` is analytic on a neighbourhood of `U` and not locally constant,
343343
then the preimage of any subset codiscrete within `f '' U` is codiscrete within `U`.
344344
345-
See `AnalyticOnNhd.preimage_zero_codiscreteWithin` for the special case that `s` is the complement
346-
of zero. Applications might want to use the theorem `Filter.codiscreteWithin.mono`.
345+
See `AnalyticOnNhd.preimage_zero_mem_codiscreteWithin` for the special case that `s` is the
346+
complement of zero. Applications might want to use the theorem `Filter.codiscreteWithin.mono`.
347347
-/
348348
theorem AnalyticOnNhd.preimage_mem_codiscreteWithin {U : Set 𝕜} {s : Set E} {f : 𝕜 → E}
349349
(hfU : AnalyticOnNhd 𝕜 f U) (h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x))

0 commit comments

Comments
 (0)