Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-02-06 08:48
b5813cc1
View on Github →
feat: port Topology.Order.Priestley (
#2070
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Topology/Order/Priestley.lean
added
theorem
exists_clopen_lower_of_not_le
added
theorem
exists_clopen_upper_of_not_le
added
theorem
exists_clopen_upper_or_lower_of_ne