Theorems · Definition · general topology

PrimitiveSpectrum.hull

{α : Type u_1} → [SemilatticeInf α] → (T : Set α) → α → Set ↑T

For a of type α the set of element of T which dominate a is the hull of a in T.

Defined in

Mathlib.Topology.Order.HullKernel

Cited by

13 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

SemilatticeInf