Preimage theorem

Stream: Is there code for X?

[Uni Marx]

Has the preimage theorem (e.g. that $f^{-1}(c)$ is a $C^n$ manifold for $f$ a $C^n$ function and $c$ a regular point) been implemented yet?

[Johan Commelin]

I'm not aware of it. But @Sebastien Gouezel will be able to confirm...

[Eric Wieser]

(double $$s for math in Zulip)

[Uni Marx]

In Mathlib.Analysis.Calculus.Implicit (how do you link these?) there's the todo note "Prove that in a real vector space the implicit function has the same smoothness as the original one" and I'm pretty sure you won't get around this statement all that easily (unless maybe there's similar theory redeveloped in the manifold bits), so it seems like it's nowhere close, sadly

[Johan Commelin]

file#Mathlib.Analysis.Calculus.Implicit

[Johan Commelin]

hmm, that didn't work

[Eric Wieser]

file#Mathlib/Analysis/Calculus/Implicit

[Eric Wieser]

file#Mathlib/Mathlib/Analysis/Calculus/Implicit