@[reducible, inline]

abbrev Sublocale (E : Type u_2) [Order.Frame E] : Type u_2

Equations

• Sublocale E = (Nucleus E)ᵒᵈ

instance instFunLikeSublocale {E : Type u_1} [Order.Frame E] : FunLike (Sublocale E) E E

Equations

• instFunLikeSublocale = { coe := fun (x : Sublocale E) => x.toFun, coe_injective' := ⋯ }

theorem Sublocale.le_iff {E : Type u_1} [Order.Frame E] (u v : Sublocale E) : u ≤ v ↔ ∀ (i : E), v i ≤ u i

theorem ext {E : Type u_1} [Order.Frame E] (a b : Sublocale E) (h : ∀ (x : E), a x = b x) : a = b

@[simp]

theorem Sublocale.sSup_apply {E : Type u_1} [Order.Frame E] (s : Set (Sublocale E)) (x : E) : (sSup s) x = ⨅ j ∈ s, j x

@[simp]

theorem Sublocale.iSup_apply {E : Type u_1} [Order.Frame E] {ι : Type u_2} (f : ι → Sublocale E) (x : E) : (iSup f) x = ⨅ (j : ι), (f j) x

@[simp]

theorem Sublocale.sup_apply {E : Type u_1} [Order.Frame E] (u v : Sublocale E) (x : E) : (u ⊔ v) x = u x ⊓ v x

@[simp]

theorem Sublocale.inf_apply {E : Type u_1} [Order.Frame E] (u v : Sublocale E) (x : E) : (u ⊓ v) x = ⨅ j ∈ lowerBounds {u, v}, j x

@[simp]

theorem Sublocale.top_apply {E : Type u_1} [Order.Frame E] (x : E) : ⊤ x = x

@[simp]

theorem Sublocale.bot_apply {E : Type u_1} [Order.Frame E] (x : E) : ⊥ x = ⊤

structure Open (E : Type u_2) [Order.Frame E] : Type u_2

• element : E

theorem Open.ext {E : Type u_2} {inst✝ : Order.Frame E} {x y : Open E} (element : x.element = y.element) : x = y

def Open.toSublocale {E : Type u_1} [Order.Frame E] (U : Open E) : Sublocale E

Equations

• U.toSublocale = { toFun := fun (x : E) => U.element ⇨ x, map_inf' := ⋯, idempotent' := ⋯, le_apply' := ⋯ }

instance Open.instCoe {E : Type u_1} [Order.Frame E] : Coe (Open E) E

Equations

• Open.instCoe = { coe := fun (x : Open E) => x.element }

instance Open.instCoeSublocale {E : Type u_1} [Order.Frame E] : Coe (Open E) (Sublocale E)

Equations

• Open.instCoeSublocale = { coe := fun (x : Open E) => x.toSublocale }

instance Open.instLE {E : Type u_1} [Order.Frame E] : LE (Open E)

Equations

• Open.instLE = { le := fun (x y : Open E) => x.element ≤ y.element }

instance Open.instPartialOrder {E : Type u_1} [Order.Frame E] : PartialOrder (Open E)

Equations

• Open.instPartialOrder = PartialOrder.mk ⋯

theorem Open.le_def {E : Type u_1} [Order.Frame E] {U V : Open E} : U ≤ V ↔ U.element ≤ V.element

theorem Open.lt_def {E : Type u_1} [Order.Frame E] {U V : Open E} : U < V ↔ U.element < V.element

theorem Open.toSublocale.mono {E : Type u_1} [Order.Frame E] : Monotone Open.toSublocale

theorem Open.mk_mono {E : Type u_1} [Order.Frame E] : Monotone mk

instance Open.instBoundedOrder {E : Type u_1} [Order.Frame E] : BoundedOrder (Open E)

Equations

• Open.instBoundedOrder = BoundedOrder.mk

@[simp]

theorem Open.top_element {E : Type u_1} [Order.Frame E] : ⊤.element = ⊤

@[simp]

theorem Open.bot_element {E : Type u_1} [Order.Frame E] : ⊥.element = ⊥

@[simp]

theorem Open.top_toSublocale {E : Type u_1} [Order.Frame E] : ⊤.toSublocale = ⊤

@[simp]

theorem Open.bot_toSublocale {E : Type u_1} [Order.Frame E] : ⊥.toSublocale = ⊥

instance Open.instCompleteSemilatticeSup {E : Type u_1} [Order.Frame E] : CompleteSemilatticeSup (Open E)

Equations

• Open.instCompleteSemilatticeSup = CompleteSemilatticeSup.mk ⋯ ⋯

theorem Open.sSup_def {E : Type u_1} [Order.Frame E] (s : Set (Open E)) : sSup s = { element := sSup (element '' s) }

instance Open.instSemilatticeInf {E : Type u_1} [Order.Frame E] : SemilatticeInf (Open E)

Equations

• Open.instSemilatticeInf = SemilatticeInf.mk (fun (x y : Open E) => { element := x.element ⊓ y.element }) ⋯ ⋯ ⋯

instance Open.instCompleteLattice {E : Type u_1} [Order.Frame E] : CompleteLattice (Open E)

Equations

• Open.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem Open.sup_def {E : Type u_1} [Order.Frame E] (u v : Open E) : u ⊔ v = { element := u.element ⊔ v.element }

theorem Open.inf_def {E : Type u_1} [Order.Frame E] (u v : Open E) : u ⊓ v = { element := u.element ⊓ v.element }

@[simp]

theorem Open.mk_element {E : Type u_1} [Order.Frame E] (U : Open E) : { element := U.element } = U

@[simp]

theorem Open.toSublocale_apply {E : Type u_1} [Order.Frame E] (U : Open E) (x : E) : U.toSublocale x = U.element ⇨ x

@[simp]

theorem Open.apply_self {E : Type u_1} [Order.Frame E] (U : Open E) : U.toSublocale U.element = ⊤

theorem Open.le_iff {E : Type u_1} [Order.Frame E] {U V : Open E} : U ≤ V ↔ U.toSublocale ≤ V.toSublocale

theorem Open.toSublocale_injective {E : Type u_1} [Order.Frame E] : Function.Injective Open.toSublocale

theorem Open.eq_iff {E : Type u_1} [Order.Frame E] {U V : Open E} : U = V ↔ U.toSublocale = V.toSublocale

@[simp]

theorem Open.Sublocale.coe_mk {E : Type u_1} [Order.Frame E] (f : InfHom E E) (h2 : ∀ (x : E), f.toFun (f.toFun x) ≤ f.toFun x) (h3 : ∀ (x : E), x ≤ f.toFun x) : { toFun := ⇑{ toInfHom := f, idempotent' := h2, le_apply' := h3 }, map_inf' := ⋯ } = f

theorem Open.preserves_inf {E : Type u_1} [Order.Frame E] (U V : Open E) : (U ⊓ V).toSublocale = U.toSublocale ⊓ V.toSublocale

theorem Open.preserves_sSup {E : Type u_1} [Order.Frame E] (s : Set (Open E)) : (sSup s).toSublocale = sSup (Open.toSublocale '' s)

theorem Open.preserves_iSup {E : Type u_1} [Order.Frame E] {ι : Sort u_2} (f : ι → Open E) : (iSup f).toSublocale = ⨆ (i : ι), (f i).toSublocale

theorem Open.preserves_sup {E : Type u_1} [Order.Frame E] {U V : Open E} : (U ⊔ V).toSublocale = U.toSublocale ⊔ V.toSublocale

def complement {E : Type u_1} [Order.Frame E] (U : Open E) : Sublocale E

Equations

• complement U = { toFun := fun (x : E) => U.element ⊔ x, map_inf' := ⋯, idempotent' := ⋯, le_apply' := ⋯ }

structure Closed (E : Type u_2) [Order.Frame E] : Type u_2

• element : E

theorem Closed.ext {E : Type u_2} {inst✝ : Order.Frame E} {x y : Closed E} (element : x.element = y.element) : x = y

def Closed.toSublocale {E : Type u_1} [Order.Frame E] (c : Closed E) : Sublocale E

Equations

• c.toSublocale = complement { element := c.element }

theorem Closed.toSublocale_apply {E : Type u_1} [Order.Frame E] (c : Closed E) (x : E) : c.toSublocale x = c.element ⊔ x

instance Closed.instCoeSublocale {E : Type u_1} [Order.Frame E] : Coe (Closed E) (Sublocale E)

Equations

• Closed.instCoeSublocale = { coe := fun (x : Closed E) => x.toSublocale }

instance Closed.instLE {E : Type u_1} [Order.Frame E] : LE (Closed E)

Equations

• Closed.instLE = { le := fun (x y : Closed E) => y.element ≤ x.element }

theorem Closed.le_def {E : Type u_1} [Order.Frame E] (x y : Closed E) : x ≤ y ↔ y.element ≤ x.element

theorem Closed.le_iff {E : Type u_1} [Order.Frame E] (x y : Closed E) : x ≤ y ↔ x.toSublocale ≤ y.toSublocale

def Closed.compl {E : Type u_1} [Order.Frame E] (c : Closed E) : Open E

Equations

• c.compl = { element := c.element }

@[simp]

theorem Closed.element_compl {E : Type u_1} [Order.Frame E] (c : Closed E) : c.compl.element = { element := c.element }.element

instance Closed.instInfSet {E : Type u_1} [Order.Frame E] : InfSet (Closed E)

Equations

• Closed.instInfSet = { sInf := fun (x : Set (Closed E)) => { element := sSup (Closed.element '' x) } }

theorem Closed.sInf_def {E : Type u_1} [Order.Frame E] (s : Set (Closed E)) : sInf s = { element := sSup (element '' s) }

theorem Closed.preserves_sInf {E : Type u_1} [Order.Frame E] (s : Set (Closed E)) : (sInf s).toSublocale = sInf (Closed.toSublocale '' s)

instance Closed.instCompleteSemilatticeInf {E : Type u_1} [Order.Frame E] : CompleteSemilatticeInf (Closed E)

Equations

• Closed.instCompleteSemilatticeInf = CompleteSemilatticeInf.mk ⋯ ⋯

instance Closed.instSemilatticeInf {E : Type u_1} [Order.Frame E] : SemilatticeInf (Closed E)

Equations

• Closed.instSemilatticeInf = SemilatticeInf.mk (fun (x y : Closed E) => { element := x.element ⊔ y.element }) ⋯ ⋯ ⋯

def Closed.inf_def {E : Type u_1} [Order.Frame E] (x y : Closed E) : x ⊓ y = { element := x.element ⊔ y.element }

Equations

• ⋯ = ⋯

def Closed.preserves_inf {E : Type u_1} [Order.Frame E] (x y : Closed E) : (x ⊓ y).toSublocale = x.toSublocale ⊓ y.toSublocale

Equations

• ⋯ = ⋯

def Open.compl {E : Type u_1} [Order.Frame E] (U : Open E) : Closed E

Equations

• U.compl = { element := U.element }

@[simp]

theorem Open.compl_element {E : Type u_1} [Order.Frame E] (U : Open E) : U.compl.element = U.element

theorem Open.inf_compl_eq_bot {E : Type u_1} [Order.Frame E] (U : Open E) : U.toSublocale ⊓ U.compl.toSublocale = ⊥

theorem Open.sup_compl_eq_top {E : Type u_1} [Order.Frame E] (U : Open E) : U.toSublocale ⊔ U.compl.toSublocale = ⊤

theorem Open.compl_le_compl {E : Type u_1} [Order.Frame E] (U V : Open E) (h : U ≤ V) : V.compl ≤ U.compl

theorem Closed.compl_le_compl {E : Type u_1} [Order.Frame E] (c d : Closed E) (h : c ≤ d) : d.compl ≤ c.compl

theorem Closed_compl_le_Open_compl {E : Type u_1} [Order.Frame E] (U : Open E) (c : Closed E) (h : U.toSublocale ≤ c.toSublocale) : c.compl.toSublocale ≤ U.compl.toSublocale