Commit 2021-01-14 22:10 975f41a4

View on Github →

feat(order): closure operators (#5524) Adds closure operators on a partial order, as in wikipedia. I made them bundled for no particular reason, I don't mind unbundling.

Estimated changes

Created src/order/closure.lean

added def closure_operator.closed

added theorem closure_operator.closed_eq_range_close

added theorem closure_operator.closure_eq_self_of_mem_closed

added theorem closure_operator.closure_inter_le

added theorem closure_operator.closure_is_closed

added theorem closure_operator.closure_le_closed_iff_le

added theorem closure_operator.closure_top

added theorem closure_operator.closure_union_closure_le

added theorem closure_operator.ext

added def closure_operator.gi

added def closure_operator.id

added theorem closure_operator.idempotent

added theorem closure_operator.le_closure

added theorem closure_operator.le_closure_iff

added theorem closure_operator.mem_closed_iff

added theorem closure_operator.mem_closed_iff_closure_le

added theorem closure_operator.monotone

added def closure_operator.to_closed

added theorem closure_operator.top_mem_closed

added structure closure_operator