Theorems · Definition · general topology

PrimitiveSpectrum.kernel

{α : Type u_1} → [CompleteLattice α] → {T : Set α} → Set ↑T → α

For a subset S of T, kernel S is the infimum of S (considered as a set of α)

Defined in

Mathlib.Topology.Order.HullKernel

Cited by

5 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

CompleteLattice