English
The composition u ∘ l defines a closure operator on α; i.e., there exists a closure operator on α equal to this composition.
Русский
Композиция u ∘ l определяет оператор замыкания на α; то есть существует оператор замыкания на α, равный этой композиции.
LaTeX
$$$\exists C:\mathrm{ClosureOperator}(\alpha),\ \forall x:\alpha,\ C(x)=u(l(x)).$$$
Lean4
/-- Every lower adjoint induces a closure operator given by the composition. This is the partial
order version of the statement that every adjunction induces a monad. -/
@[simps]
def closureOperator : ClosureOperator α where
toFun x := u (l x)
monotone' := l.monotone
le_closure' := l.le_closure
idempotent' x := l.gc.u_l_u_eq_u (l x)
