closureOperator — Mathlib

English

Let f,g form a Galois connection. If s ⊆ α is cofinal, then g''s is cofinal in β.

Русский

Пусть f,g образуют сопряжение Галуа. Если s ⊆ α является софинальным, то образ g''s является софинальным в β.

LaTeX

$$$\text{IsCofinal}(s) \rightarrow \text{IsCofinal}(g''s)$$$

Lean4

/-- Every Galois connection 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 [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
    ClosureOperator α :=
  gc.lowerAdjoint.closureOperator

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