Invertibility is an open condition for bounded linear operat

Stream: Is there code for X?

[Michael Rothgang]

Given Banach spaces $E$ and $F$ over a field $k$, the set of invertible bounded linear operators $E\to F$ is open (in the topology induced by the operator norm). This follows from Neumann series, which I couldn't find in mathlib either.

This is a key step for developing the theory of Fredholm operators --- which has all kinds of applications, such as proving the Sard's theorem for infinite-dimensional Banach manifolds.

[Kevin Buzzard]

Fredholm operators on p-adic Banach spaces also play a role in the proof of the Weil conjectures and the theory of p-adic modular forms

[Sebastien Gouezel]

@loogle IsOpen, _ →L[_] _

[loogle]

:exclamation: unknown identifier 'sOpen'

[Sebastien Gouezel]

@loogle IsOpen, _ →L[_] _

[loogle]

:search: isOpen_setOf_nat_le_rank, ContinuousLinearEquiv.isOpen, and 42 more

[Sebastien Gouezel]

I think you're looking for docs#ContinuousLinearEquiv.isOpen

[Anatole Dedecker]

More generally we also have docs#Units.isOpen

[Michael Rothgang]

I hadn't realised how I could use loogle for that. (I search for e.g. Neumann series, without results)... Thanks for the tip.
Thanks for all the help!

[Jireh Loreaux]

Anatole, that's not quite "more general", more like, "differently general"

[Anatole Dedecker]

Ah right it’s not an algebra