Theorem ENNReal.isEmbedding_coe

Modification history

2025-01-13 14:29

Mathlib/Topology/Instances/ENNReal/Defs.lean

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

Modified ENNReal.isEmbedding_coe View on Github →

2024-10-28 08:46

Mathlib/Topology/Instances/ENNReal.lean

chore: Rename `Embedding` to `IsEmbedding` (#18133) …

Added ENNReal.isEmbedding_coe View on Github →