Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-08 19:13 5c6d3bce

View on Github →

feat(topology/instances/ereal): more on ereal, notably its topology (#7765)

Estimated changes

Modified src/algebra/ordered_monoid.lean

Modified src/data/real/ereal.lean

added def ennreal.to_ereal

added theorem ereal.ad_eq_top_iff

added theorem ereal.add_lt_add

added theorem ereal.add_lt_add_left_coe

added theorem ereal.add_lt_add_of_lt_of_le

added theorem ereal.add_lt_add_right_coe

added theorem ereal.add_lt_top_iff

added theorem ereal.add_top

added theorem ereal.bot_add_bot

added theorem ereal.bot_add_coe

added theorem ereal.bot_lt_coe

added theorem ereal.bot_lt_coe_ennreal

added theorem ereal.bot_lt_top

added theorem ereal.bot_lt_zero

added theorem ereal.bot_ne_coe

added theorem ereal.bot_ne_top

added theorem ereal.bot_ne_zero

added theorem ereal.coe_add

added theorem ereal.coe_add_bot

added theorem ereal.coe_ennreal_add

added theorem ereal.coe_ennreal_eq_coe_ennreal_iff

added theorem ereal.coe_ennreal_eq_top_iff

added theorem ereal.coe_ennreal_le_coe_ennreal_iff

added theorem ereal.coe_ennreal_lt_coe_ennreal_iff

added theorem ereal.coe_ennreal_ne_bot

added theorem ereal.coe_ennreal_nonneg

added theorem ereal.coe_ennreal_top

added theorem ereal.coe_ennreal_zero

added theorem ereal.coe_lt_top

added theorem ereal.coe_ne_bot

added theorem ereal.coe_ne_top

added theorem ereal.coe_neg

added theorem ereal.coe_nnreal_eq_coe_real

added theorem ereal.coe_nnreal_lt_top

added theorem ereal.coe_nnreal_ne_top

added theorem ereal.coe_real_ereal_eq_coe_to_nnreal_sub_coe_to_nnreal

added theorem ereal.coe_zero

added theorem ereal.exists_rat_btwn_of_lt

added theorem ereal.lt_iff_exists_rat_btwn

added def ereal.ne_top_bot_equiv_real

added theorem ereal.neg_bot

added theorem ereal.neg_eg_bot_iff

added theorem ereal.neg_eg_top_iff

added theorem ereal.neg_eg_zero_iff

added theorem ereal.neg_eq_neg_iff

modified theorem ereal.neg_inj

added theorem ereal.neg_le_neg_iff

added theorem ereal.neg_lt_iff_neg_lt

added theorem ereal.neg_lt_of_neg_lt

added def ereal.neg_order_iso

added theorem ereal.neg_top

added theorem ereal.neg_zero

added theorem ereal.sub_eq_add_neg

added theorem ereal.sub_le_sub

added theorem ereal.sub_lt_sub_of_lt_of_le

added theorem ereal.sub_zero

added def ereal.to_real

added theorem ereal.to_real_add

added theorem ereal.to_real_bot

added theorem ereal.to_real_coe

added theorem ereal.to_real_coe_ennreal

added theorem ereal.to_real_le_to_real

added theorem ereal.to_real_neg

added theorem ereal.to_real_sub

added theorem ereal.to_real_top

added theorem ereal.to_real_zero

added theorem ereal.top_add

added theorem ereal.top_ne_coe

added theorem ereal.top_ne_zero

added theorem ereal.zero_lt_top

added theorem ereal.zero_ne_bot

added theorem ereal.zero_ne_top

added theorem ereal.zero_sub

added def real.to_ereal

Modified src/order/conditionally_complete_lattice.lean

Created src/topology/instances/ereal.lean

added theorem continuous_coe_ennreal_ereal

added theorem continuous_coe_real_ereal

added theorem ereal.continuous_at_add

added theorem ereal.continuous_at_add_bot_bot

added theorem ereal.continuous_at_add_bot_coe

added theorem ereal.continuous_at_add_coe_bot

added theorem ereal.continuous_at_add_coe_coe

added theorem ereal.continuous_at_add_coe_top

added theorem ereal.continuous_at_add_top_coe

added theorem ereal.continuous_at_add_top_top

added theorem ereal.continuous_coe_ennreal_iff

added theorem ereal.continuous_coe_iff

added theorem ereal.continuous_neg

added theorem ereal.continuous_on_to_real

added theorem ereal.embedding_coe

added theorem ereal.embedding_coe_ennreal

added theorem ereal.mem_nhds_bot_iff

added theorem ereal.mem_nhds_top_iff

added def ereal.ne_bot_top_homeomorph_real

added def ereal.neg_homeo

added theorem ereal.nhds_bot'

added theorem ereal.nhds_bot

added theorem ereal.nhds_coe

added theorem ereal.nhds_coe_coe

added theorem ereal.nhds_top'

added theorem ereal.nhds_top

added theorem ereal.open_embedding_coe

added theorem ereal.tendsto_coe

added theorem ereal.tendsto_coe_ennreal

added theorem ereal.tendsto_nhds_bot_iff_real

added theorem ereal.tendsto_nhds_top_iff_real

added theorem ereal.tendsto_to_real