Theorems · Inductive type · order theory

Sublocale

(X : Type u_2) → [Order.Frame X] → Type u_2

A sublocale of a locale X is a set S which is closed under all meets and such that x ⇨ s ∈ S for all x : X and s ∈ S. Note that locales are the same thing as frames, but with reverse morphisms, which is why we assume Frame X. We only need to define locales categorically. See Locale.

Defined in

Mathlib.Order.Sublocale

Cited by

30 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

Order.Frame