Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-12 06:48 c5d91bc7

View on Github →

feat(topology/algebra/ordered): add order topology for partial orders… (#1276)

  • feat(topology/algebra/ordered): doc, add convergence in ordered groups criterion
  • docstring
  • reviewer's comments

Estimated changes

modified theorem Inf_mem_closure
modified theorem Inf_mem_of_is_closed
modified theorem Sup_mem_closure
modified theorem Sup_mem_of_is_closed
modified theorem cInf_mem_closure
modified theorem cInf_mem_of_is_closed
modified theorem cSup_mem_closure
modified theorem cSup_mem_of_is_closed
added theorem induced_order_topology
modified theorem infi_eq_of_tendsto
added theorem nhds_bot_order
deleted theorem nhds_bot_orderable
added theorem nhds_eq_order
deleted theorem nhds_eq_orderable
added theorem nhds_order_unbounded
deleted theorem nhds_orderable_unbounded
added theorem nhds_top_order
deleted theorem nhds_top_orderable
modified theorem supr_eq_of_tendsto
modified theorem tendsto_at_top_infi_nat
modified theorem tendsto_at_top_supr_nat
added theorem tendsto_order
deleted theorem tendsto_orderable