Commit 2020-01-15 07:24 819939fb

View on Github →

refactor(order/lattice): generalize directed_of_mono (#1879) It suffices to have semilattice_sup, not decidable_linear_order. Also add directed_of_antimono.

Estimated changes

Modified src/order/basic.lean

deleted theorem directed_of_mono

Modified src/order/lattice.lean

added theorem lattice.directed_of_antimono

added theorem lattice.directed_of_mono

Modified src/topology/bases.lean

Modified src/topology/sequences.lean