Theorems · Theorem · general topology

PrimitiveSpectrum.hull_finsetInf

∀ {α : Type u_1} [inst : SemilatticeInf α] {T : Set α} [inst_1 : OrderTop α],
  (∀ p ∈ T, InfPrime p) → ∀ (F : Finset α), PrimitiveSpectrum.hull T (F.inf id) = Subtype.val ⁻¹' ↑(upperClosure ↑F)

Every relative-closed set of the form T ↓∩ (↑(upperClosure F)) for F finite is a relative-closed set of the form hull T a where a = ⨅ F.

Defined in

Mathlib.Topology.Order.HullKernel

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemilatticeInfOrderTop