Mathlib Changelog
v4
Changelog
About
Github
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