gc_upperClosure_coe — Mathlib

English

The upper closure operator and the coercion from upper sets to sets form a Galois connection.

Русский

Оператор верхнего замыкания и отображение из верхних множеств в множества образуют галуа‑связь.

LaTeX

$$GaloisConnection (toDual \circ \mathrm{upperClosure} : Set α \to (UpperSet α)^{\mathrm{op}}) ((↑) \circ ofDual)$$

Lean4

theorem gc_upperClosure_coe : GaloisConnection (toDual ∘ upperClosure : Set α → (UpperSet α)ᵒᵈ) ((↑) ∘ ofDual) :=
  fun _s _t ↦ le_upperClosure

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