Zulip Chat Archive

Stream: maths

Topic: open immersions

Johan Commelin (Jan 03 2019 at 08:46):

Do we have open immersions in mathlib? We have embedding, but do we also have open maps?

Patrick Massot (Jan 03 2019 at 09:02):

we have open maps, yes https://github.com/leanprover/mathlib/blob/a04c7e20c8a19018201bc772c414f7b2cd0d00b9/analysis/topology/continuity.lean#L412

Last updated: May 02 2025 at 03:31 UTC