Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-20 17:44 0d6bae76

View on Github →

refactor(order/filter): move directed to order.basic, swap definition directed means containing upper bounds, not lower bounds

Estimated changes

added theorem directed.finset_le
added def directed
added theorem directed_comp
added theorem directed_mono
added def directed_on
added theorem is_antisymm.swap
added theorem is_asymm.swap
modified theorem is_irrefl.swap
added theorem is_linear_order.swap
added theorem is_partial_order.swap
added theorem is_preorder.swap
added theorem is_refl.swap
added theorem is_total.swap
added theorem is_total_preorder.swap
added def order.preimage
deleted def directed
modified theorem directed_of_chain
deleted def directed_on
modified theorem directed_on_Union
modified theorem filter.infi_sets_eq'
modified theorem filter.infi_sets_eq
modified theorem filter.map_infi_eq
deleted def order.preimage