Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-21 21:35 e739cf50

View on Github →

feat(order_dual): instances for order_dual and shortening proofs (#746)

  • feat(order_bot): instances for order_bot and shortening proofs
  • fix(topological_structure); remove unused import

Estimated changes

modified theorem Liminf_nhds
modified theorem Limsup_eq_of_le_nhds
modified theorem gt_mem_sets_of_Liminf_gt
modified theorem is_glb_of_is_lub_of_tendsto
modified theorem is_glb_of_mem_nhds