Commit 2023-02-01 11:14 b9372103

View on Github →

feat: port Order.Minimal (#1914)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Minimal.lean

added theorem IsAntichain.max_maximals

added theorem IsAntichain.max_minimals

added theorem IsAntichain.maximals_eq

added theorem IsAntichain.maximals_lowerClosure

added theorem IsAntichain.minimals_eq

added theorem IsAntichain.minimals_upperClosure

added theorem IsGreatest.maximals_eq

added theorem IsGreatest.mem_maximals

added theorem IsLeast.mem_minimals

added theorem IsLeast.minimals_eq

added theorem Set.Subsingleton.maximals_eq

added theorem Set.Subsingleton.minimals_eq

added theorem eq_of_mem_maximals

added theorem eq_of_mem_minimals

added theorem inter_maximals_subset

added theorem inter_minimals_subset

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_of_symm

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_of_symm

added theorem minimals_singleton

added theorem minimals_subset

added theorem minimals_swap

added theorem minimals_union