Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-19 07:18 d673bafe

View on Github →

feat(topology/algebra/ordered): add lemmas, golf (#16343)

  • add lemmas about nhds_within_Ici/nhds_within_Iic;
  • move order_separated and order_topology.to_order_closed_topology up;
  • use new lemmas to golf some proofs.

Estimated changes

added theorem nhds_within_Ici_basis'
added theorem nhds_within_Ici_basis
added theorem nhds_within_Ici_eq''
added theorem nhds_within_Ici_eq'
added theorem nhds_within_Iic_basis'
added theorem nhds_within_Iic_basis
added theorem nhds_within_Iic_eq''
added theorem nhds_within_Iic_eq'
deleted theorem order_topology.t2_space