Theorem ENNReal.isOpenEmbedding_coe

Modification history

2025-01-13 14:29

Mathlib/Topology/Instances/ENNReal/Defs.lean

chore: split Mathlib.Topology.Instances.*Real (#20707) …

Modified ENNReal.isOpenEmbedding_coe View on Github →

2024-10-18 21:29

Mathlib/Topology/Instances/ENNReal.lean

chore: Rename `OpenEmbedding` to `IsOpenEmbedding` (#17898) …

Added ENNReal.isOpenEmbedding_coe View on Github →