Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-16 14:15 cd53e272

View on Github →

chore(topology/algebra/ordered): use interval notation here and there (#1802)

  • chore(topology/algebra/ordered): use interval notation here and there Also prove a slightly more general version of mem_nhds_orderable_dest
  • Fix a few compile errors
  • Rename a lemma, fix compile, add docs and dual_I?? lemmas
  • Fix names, add comments
  • Make some lemmas simp

Estimated changes

added theorem set.Ici_subset_Ioi
added theorem set.Iic_subset_Iio
added theorem set.dual_Icc
added theorem set.dual_Ici
added theorem set.dual_Ico
added theorem set.dual_Iic
added theorem set.dual_Iio
added theorem set.dual_Ioc
added theorem set.dual_Ioi
added theorem set.dual_Ioo
modified theorem set.nonempty_Icc
modified theorem set.nonempty_Ico
modified theorem set.nonempty_Ioc
added theorem filter.binfi_sets_eq
deleted theorem filter.infi_sets_eq'
added theorem filter.mem_binfi
added theorem closure_lt_subset_le
deleted theorem mem_nhds_orderable_dest
modified theorem nhds_eq_orderable