Commit 2023-03-14 07:09 d962f0fa

View on Github →

feat: port Topology.Instances.Ereal (#2796)

API changes

  • Add ENNReal.range_coe, ENNReal.range_coe', and ENNReal.coe_strictMono.
  • Add instances for DenselyOrdered EReal, T5Space EReal, ContinuousNeg EReal, and CanLift EReal ENNReal _ _.
  • Add EReal.range_coe, EReal.range_coe_eq_Ioo, EReal.range_coe_ennreal.
  • Add EReal.denseRange_ratCast, EReal.nhds_top_basis, EReal.nhds_bot_basis.
  • Deprecate EReal.negHomeo and EReal.continuous_neg.
  • Generalize orderTopology_of_ordConnected to StrictMono.induced_topology_eq_preorder and StrictMono.embedding_of_ordConnected, use it to prove that some coercions are embeddings.
  • Prove TopologicalSpace.SecondCountableTopology.of_separableSpace_orderTopology and helper lemmas Dense.topology_eq_generateFrom, Dense.Ioi_eq_bunionᵢ, and Dense.Iio_eq_bunionᵢ.

Estimated changes

added theorem ENNReal.coe_strictMono
added theorem ENNReal.range_coe'
added theorem ENNReal.range_coe
added theorem EReal.range_coe
added theorem EReal.range_coe_eq_Ioo
modified theorem ENNReal.embedding_coe
added theorem EReal.continuousAt_add
added theorem EReal.embedding_coe
added theorem EReal.mem_nhds_bot_iff
added theorem EReal.mem_nhds_top_iff
added def EReal.negHomeo
added theorem EReal.nhds_bot'
added theorem EReal.nhds_bot
added theorem EReal.nhds_bot_basis
added theorem EReal.nhds_coe
added theorem EReal.nhds_coe_coe
added theorem EReal.nhds_top'
added theorem EReal.nhds_top
added theorem EReal.tendsto_coe
added theorem EReal.tendsto_toReal
added theorem Dense.Iio_eq_bunionᵢ
added theorem Dense.Ioi_eq_bunionᵢ