Documentation

Leroy.Further_Topology

def Sublocale.Open_Neighbourhood {X : Type u} [Order.Frame X] (u : Sublocale X) :

Equations

u.Open_Neighbourhood = {v : Open X | u ≤ v.toSublocale}

Instances For

def Sublocale.Neighbourhood {X : Type u} [Order.Frame X] (u : Sublocale X) :

Set (Sublocale X)

Equations

u.Neighbourhood = {v : Sublocale X | ∃ w ∈ u.Open_Neighbourhood, w.toSublocale ≤ v}

Instances For

theorem Sublocale.Neighourhood.le {E : Type u} [e_frm : Order.Frame E] {a : Sublocale E} (x : Sublocale E) :

x ∈ a.Neighbourhood → a ≤ x

theorem Sublocale.Open_Neighbourhood.top_mem {X : Type u} [Order.Frame X] {x : Sublocale X} :

⊤ ∈ x.Open_Neighbourhood

@[simp]

theorem Sublocale.Open_Neighbourhood.Nonempty {X : Type u} [Order.Frame X] (x : Sublocale X) :

x.Open_Neighbourhood.Nonempty

@[simp]

theorem Sublocale.Nonempty_Open_Neighbourhood {X : Type u} [Order.Frame X] (x : Sublocale X) :

Nonempty ↑x.Open_Neighbourhood

theorem Sublocale.Neighbourhood.top_mem {X : Type u} [Order.Frame X] (x : Sublocale X) :

⊤ ∈ x.Neighbourhood

theorem Sublocale.Nonempty_Neighbourhood {X : Type u} [Order.Frame X] (x : Sublocale X) :

Nonempty ↑x.Neighbourhood

theorem Sublocale.Open_Neighbourhood.inf_closed {E : Type u} [e_frm : Order.Frame E] {x : Sublocale E} (U : Open E) :

U ∈ x.Open_Neighbourhood → ∀ V ∈ x.Open_Neighbourhood, U ⊓ V ∈ x.Open_Neighbourhood

theorem Sublocale.Neighbourhood.inf_closed {E : Type u} [e_frm : Order.Frame E] (x U : Sublocale E) :

U ∈ x.Neighbourhood → ∀ V ∈ x.Neighbourhood, U ⊓ V ∈ x.Neighbourhood

Properties of Complement

theorem sup_eq_top_iff_compl_le {E : Type u} [e_frm : Order.Frame E] (V : Open E) (x : Sublocale E) :

V.toSublocale ⊔ x = ⊤ ↔ V.compl.toSublocale ≤ x

Leroy Lemme 8

theorem inf_eq_bot_iff_le_compl {E : Type u} [e_frm : Order.Frame E] (V : Open E) (x : Sublocale E) :

V.toSublocale ⊓ x = ⊥ ↔ x ≤ V.compl.toSublocale

theorem sup_compl_eq_top_iff {E : Type u} [e_frm : Order.Frame E] {x : Sublocale E} {u : Open E} :

u.toSublocale ≤ x ↔ x ⊔ u.compl.toSublocale = ⊤

Leroy Lemme 8 bis

theorem compl_sup_eq_inf_compl {E : Type u} [e_frm : Order.Frame E] {U V : Open E} :

(U ⊔ V).compl = U.compl ⊓ V.compl

Definitions

def Sublocale.interior {E : Type u} [e_frm : Order.Frame E] (x : Sublocale E) :

Equations

x.interior = sSup {z : Open E | z.toSublocale ≤ x}

Instances For

theorem Open_interior_eq_id {E : Type u} [e_frm : Order.Frame E] (a : Open E) :

a.toSublocale.interior = a

def Open.interior {E : Type u} [e_frm : Order.Frame E] (x : Sublocale E) :

Equations

Open.interior x = x

Instances For

noncomputable def Closed.interior {E : Type u} [e_frm : Order.Frame E] (x : Closed E) :

Equations

x.interior = x.toSublocale.interior

Instances For

def Sublocale.closure {E : Type u} [e_frm : Order.Frame E] (x : Sublocale E) :

Equations

x.closure = sInf {z : Closed E | x ≤ z.toSublocale}

Instances For

def Open.closure {E : Type u} [e_frm : Order.Frame E] (x : Open E) :

Equations

x.closure = sInf {z : Closed E | x.toSublocale ≤ z.toSublocale}

Instances For

noncomputable def Sublocale.rand {E : Type u} [e_frm : Order.Frame E] (x : Sublocale E) :

Equations

x.rand = x.closure.toSublocale ⊓ complement x.interior

Instances For

def Sublocale.exterior {E : Type u} [e_frm : Order.Frame E] (x : Sublocale E) :

Equations

x.exterior = sSup {z : Open E | z.toSublocale ⊓ x = ⊥}

Instances For

def Open.exterior {E : Type u} [e_frm : Order.Frame E] (x : Open E) :

Equations

x.exterior = sSup {z : Open E | z ⊓ x = ⊥}

Instances For

def Closed.exterior {E : Type u} [e_frm : Order.Frame E] (x : Closed E) :

Equations

x.exterior = sSup {z : Open E | z.toSublocale ⊓ x.toSublocale = ⊥}

Instances For

theorem Open.inf_Exterior_eq_bot {E : Type u} [e_frm : Order.Frame E] (x : Open E) :

x ⊓ x.exterior = ⊥

theorem Closure_compl_eq_exterior {E : Type u} [e_frm : Order.Frame E] (U : Open E) :

U.closure.compl = U.exterior

theorem Sublocale.compl_element_eq_compl_closure {E : Type u} [e_frm : Order.Frame E] (V : Open E) :

{ element := V.elementᶜ } = V.closure.compl

theorem Open.compl_element_eq_exterior {E : Type u} [e_frm : Order.Frame E] (U : Open E) :

{ element := U.elementᶜ } = U.exterior

theorem Open.le_exterior_exterior {E : Type u} [e_frm : Order.Frame E] (x : Open E) :

x ≤ x.exterior.exterior

theorem Open_compl_le_Closed_compl {E : Type u} [e_frm : Order.Frame E] (U : Open E) (c : Closed E) (h : c.toSublocale ≤ U.toSublocale) :

U.compl.toSublocale ≤ c.compl.toSublocale

theorem compl_element_le_compl {E : Type u} [e_frm : Order.Frame E] (V : Open E) :

{ element := V.elementᶜ }.toSublocale ≤ V.compl.toSublocale

theorem Sublocale.eq_intersection_open_closed {E : Type u} [e_frm : Order.Frame E] (j : Sublocale E) :

j = ⨅ (a : E), { element := a }.toSublocale ⊔ { element := j a }.toSublocale

Quelle: Johnstone Lemma C 1.1.17 (S. 485)