Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-19 21:00 e598894d

View on Github →

chore(topology/*): reverse order on topological and uniform spaces (#1138)

  • chore(topology/*): reverse order on topological and uniform spaces
  • fix(topology/order): private lemma hiding partial order oscillation, following Mario's suggestion
  • change a temporary name Co-Authored-By: Johan Commelin johan@commelin.net
  • forgotten rename

Estimated changes

modified theorem ennreal.measurable_sub
modified theorem nnreal.measurable_add
modified theorem nnreal.measurable_mul
modified theorem nnreal.measurable_sub
added theorem lattice.infi_pair
added theorem lattice.supr_pair
modified theorem nnreal.continuous_sub'
modified theorem nnreal.continuous_sub
added theorem coinduced_bot
deleted theorem coinduced_inf
deleted theorem coinduced_infi
added theorem coinduced_sup
added theorem coinduced_supr
deleted theorem coinduced_top
modified theorem continuous_Inf_dom
modified theorem continuous_Inf_rng
modified theorem continuous_Sup_dom
modified theorem continuous_Sup_rng
modified theorem continuous_bot
deleted theorem continuous_iff_induced_le
deleted theorem continuous_inf_dom
added theorem continuous_inf_rng
deleted theorem continuous_inf_rng_left
deleted theorem continuous_inf_rng_right
modified theorem continuous_infi_dom
modified theorem continuous_infi_rng
added theorem continuous_sup_dom
deleted theorem continuous_sup_dom_left
deleted theorem continuous_sup_dom_right
deleted theorem continuous_sup_rng
modified theorem continuous_supr_dom
modified theorem continuous_supr_rng
modified theorem continuous_top
modified theorem eq_of_nhds_eq_nhds
deleted theorem eq_top_of_singletons_open
added theorem gc_coinduced_induced
deleted theorem gc_induced_coinduced
deleted theorem generate_from_le
deleted theorem induced_bot
added theorem induced_inf
added theorem induced_infi
deleted theorem induced_sup
deleted theorem induced_supr
added theorem induced_top
modified theorem is_closed_infi_iff
deleted theorem is_open_infi_iff
added theorem is_open_supr_iff
added theorem le_generate_from
modified theorem le_of_nhds_le_nhds
added theorem nhds_Inf
deleted theorem nhds_Sup
modified theorem nhds_bot
added theorem nhds_inf
added theorem nhds_infi
deleted theorem nhds_sup
deleted theorem nhds_supr
modified theorem nhds_top
added def tmp_order
modified theorem dense_embedding_pure
added theorem inf_uniformity
added theorem infi_uniformity
deleted theorem sup_uniformity
deleted theorem supr_uniformity
deleted theorem to_topological_space_Sup
modified theorem to_topological_space_bot
deleted theorem to_topological_space_sup
deleted theorem to_topological_space_supr
modified theorem to_topological_space_top