lowerAdjoint — Mathlib

English

Every Galois connection between α and β induces a closure operator on α by composing the two maps, namely cl(a) = u(l(a)).

Русский

Каждое сопряжение Галуа между α и β порождает замыкательный оператор на α, задаваемый как cl(a) = u(l(a)).

LaTeX

$$$\text{closureOperator} = u \circ l\quad\text{is a closure operator on } \alpha$$$

Lean4

/-- Every Galois connection induces a lower adjoint. -/
@[simps]
def lowerAdjoint [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : LowerAdjoint u
    where
  toFun := l
  gc' := gc

Похожие утверждения