Theorems · Theorem · general topology

PrimitiveSpectrum.gc

∀ {α : Type u_1} [inst : CompleteLattice α] {T : Set α},
  GaloisConnection (fun S => OrderDual.toDual (PrimitiveSpectrum.kernel S)) fun a =>
    PrimitiveSpectrum.hull T (OrderDual.ofDual a)

The pair of maps kernel and hull form an antitone Galois connection between the subsets of T and α.

Defined in

Mathlib.Topology.Order.HullKernel

Cited by

2 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompleteLattice