Commit 2022-01-11 20:49 94fd004d

View on Github →

feat(order/minimal): Subset of minimal/maximal elements (#11268) This defines minimals r s/maximals r s the minimal/maximal elements of s with respect to relation r.

Estimated changes

Modified src/data/set/basic.lean

added theorem set.sep_empty

Modified src/order/antichain.lean

added theorem is_antichain.eq_of_related'

deleted theorem is_antichain.mk_is_antichain

deleted theorem is_antichain.mk_max

deleted theorem is_antichain.mk_subset

Modified src/order/basic.lean

added theorem ge_antisymm

Created src/order/minimal.lean

added theorem inter_maximals_subset

added theorem inter_minimals_subset

added theorem is_antichain.max_maximals

added theorem is_antichain.max_minimals

added theorem is_antichain.maximals_eq

added theorem is_antichain.minimals_eq

added theorem is_greatest.maximals_eq

added theorem is_greatest.mem_maximals

added theorem is_least.mem_minimals

added theorem is_least.minimals_eq

added def maximals

added theorem maximals_antichain

added theorem maximals_empty

added theorem maximals_eq_minimals

added theorem maximals_idem

added theorem maximals_inter_subset

added theorem maximals_mono

added theorem maximals_singleton

added theorem maximals_subset

added theorem maximals_swap

added theorem maximals_union

added def minimals

added theorem minimals_antichain

added theorem minimals_empty

added theorem minimals_idem

added theorem minimals_inter_subset

added theorem minimals_mono

added theorem minimals_singleton

added theorem minimals_subset

added theorem minimals_swap

added theorem minimals_union

added theorem set.subsingleton.maximals_eq

added theorem set.subsingleton.minimals_eq

Modified src/order/rel_classes.lean

added theorem comm

added theorem comm_of