## Stream: Is there code for X?

### Topic: continuous_linear_equiv

#### Frédéric Dupuis (Oct 12 2020 at 03:30):

Is there a good way to define a continuous_linear_equiv (where by "good" I mean via a bound rather than by proving continuity directly)? Basically I'm looking for something similar to linear_map.mk_continuous.

#### Heather Macbeth (Oct 12 2020 at 03:33):

Do you have bounds in both directions? Or are you planning to use the Banach open mapping theorem?

#### Frédéric Dupuis (Oct 12 2020 at 03:49):

Let's say I have bounds in both directions -- are you aware of any lemmas I could use?

(deleted)

#### Heather Macbeth (Oct 12 2020 at 03:52):

There is docs#continuous_linear_equiv.equiv_of_inverse, to make a continuous linear equiv from two continuous linear maps.

#### Heather Macbeth (Oct 12 2020 at 03:53):

And then, as you said, there is docs#linear_map.mk_continuous to make each of the directions a continuous linear map, from the bounds.

#### Heather Macbeth (Oct 12 2020 at 03:54):

Would this work in your situation?

#### Yury G. Kudryashov (Oct 12 2020 at 03:54):

Probably you should wrap it into linear_equiv.to_continuous_linear_equiv_of_bounds.

#### Yury G. Kudryashov (Oct 12 2020 at 03:54):

And add this def to topology/algebra/module.

#### Heather Macbeth (Oct 12 2020 at 03:55):

Alternatively, if you have an existing linear equiv, by definition (docs#continuous_linear_equiv), it becomes a continuous linear equiv by checking that both directions are continuous. And you can use docs#linear_map.continuous_of_bound for this.

#### Frédéric Dupuis (Oct 12 2020 at 04:08):

Thanks! I was hoping for a way that involves fewer hoops to jump through, but I'll just code it as Yury suggests.

#### Yury G. Kudryashov (Oct 12 2020 at 04:35):

Heather explained two ways to write linear_equiv.to_continuous_linear_equiv.

#### Frédéric Dupuis (Oct 12 2020 at 13:49):

Yes -- or if anything these are two functions we would want to have!

#### Frédéric Dupuis (Oct 12 2020 at 13:51):

Also, I know you suggested putting them in topology/algebra/module, but wouldn't analysis/normed_space/operator_norm (alongside linear_map.mk_continuous) be a better place, given that there are norms involved?

#### Frédéric Dupuis (Oct 12 2020 at 15:55):

#4583

Last updated: May 17 2021 at 16:26 UTC