Commit 2021-05-21 00:33 c63c6d10

View on Github →

feat(order/closure): make closure operators implementable (#7608) introduce lower_adjoint as a way to talk about closure operators whose input and output types do not match

Estimated changes

Modified src/order/closure.lean

modified theorem closure_operator.closure_bsupr_closure

modified theorem closure_operator.closure_inf_le

modified theorem closure_operator.closure_sup_closure

modified theorem closure_operator.closure_sup_closure_le

modified theorem closure_operator.closure_sup_closure_left

modified theorem closure_operator.closure_sup_closure_right

modified theorem closure_operator.closure_supr_closure

modified theorem closure_operator.closure_top

modified def closure_operator.gi

modified def closure_operator.simps.apply

modified theorem closure_operator.top_mem_closed

modified structure closure_operator

modified theorem closure_operator_gi_self

modified def galois_connection.closure_operator

added def galois_connection.lower_adjoint

added def lower_adjoint.closed

added theorem lower_adjoint.closed_eq_range_close

added theorem lower_adjoint.closure_Union_closure

added theorem lower_adjoint.closure_bUnion_closure

added theorem lower_adjoint.closure_bsupr_closure

added theorem lower_adjoint.closure_eq_self_of_mem_closed

added theorem lower_adjoint.closure_inf_le

added theorem lower_adjoint.closure_is_closed

added theorem lower_adjoint.closure_le_closed_iff_le

added def lower_adjoint.closure_operator

added theorem lower_adjoint.closure_sup_closure

added theorem lower_adjoint.closure_sup_closure_le

added theorem lower_adjoint.closure_sup_closure_left

added theorem lower_adjoint.closure_sup_closure_right

added theorem lower_adjoint.closure_supr_closure

added theorem lower_adjoint.closure_top

added theorem lower_adjoint.closure_union_closure

added theorem lower_adjoint.closure_union_closure_left

added theorem lower_adjoint.closure_union_closure_right

added theorem lower_adjoint.closure_union_closure_subset

added theorem lower_adjoint.eq_of_le

added theorem lower_adjoint.ext

added theorem lower_adjoint.gc

added theorem lower_adjoint.idempotent

added theorem lower_adjoint.le_closure

added theorem lower_adjoint.le_closure_iff

added theorem lower_adjoint.le_iff_subset

added theorem lower_adjoint.mem_closed_iff

added theorem lower_adjoint.mem_closed_iff_closure_le

added theorem lower_adjoint.mem_iff

added theorem lower_adjoint.monotone

added def lower_adjoint.simps.apply

added theorem lower_adjoint.subset_closure

added def lower_adjoint.to_closed

added structure lower_adjoint