Theorems · Definition · general topology

PrimitiveSpectrum.gi

{α : Type u_1} →
  [inst : CompleteLattice α] →
    {T : Set α} →
      PrimitiveSpectrum.OrderGenerates T →
        GaloisInsertion (⇑OrderDual.toDual ∘ PrimitiveSpectrum.kernel) (PrimitiveSpectrum.hull T ∘ ⇑OrderDual.ofDual)

When T is order generating, the kernel and the hull form a Galois insertion

Defined in

Mathlib.Topology.Order.HullKernel

Cited by

1 results in Mathlib

Foundations

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

Assumes

CompleteLattice