Mathlib v3 is deprecated. Go to Mathlib v4

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 def closure_operator.gi
modified structure closure_operator
modified theorem closure_operator_gi_self
added theorem lower_adjoint.eq_of_le
added theorem lower_adjoint.ext
added theorem lower_adjoint.gc
added theorem lower_adjoint.mem_iff
added theorem lower_adjoint.monotone
added structure lower_adjoint