Theorems · Definition · general topology

PrimitiveSpectrum.OrderGenerates

{α : Type u_1} → [CompleteLattice α] → Set α → Prop

T order generates α if, for every a in α, there exists a subset of T such that a is the kernel of S.

Defined in

Mathlib.Topology.Order.HullKernel

Cited by

3 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

CompleteLattice