def well_inside {E : Type u_3} [e_frm : Order.Frame E] (U V : Open E) : Prop

Equations

• U ≪ V = (U.closure.toSublocale ≤ V.toSublocale)

def «term_≪_» : Lean.TrailingParserDescr

Equations

• «term_≪_» = Lean.ParserDescr.trailingNode `«term_≪_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≪ ") (Lean.ParserDescr.cat `term 101))

theorem le_of_well_inside {E : Type u_3} [e_frm : Order.Frame E] (U V : Open E) (h : U ≪ V) : U ≤ V

def well_inside_iff {E : Type u_3} [e_frm : Order.Frame E] (U V : Open E) : U ≪ V ↔ ∃ (c : Open E), c ⊓ U = ⊥ ∧ c ⊔ V = ⊤

Stone spaces s.80 und auch Sketches of an Elephant 501...

Equations

• ⋯ = ⋯

def regular (E : Type u_4) [Order.Frame E] : Prop

Leroy definition Steht auch in Sketches of an Elephant 501

Equations

• regular E = ∀ (U : Open E), U = sSup {V : Open E | V ≪ U}

theorem Closed.eq_intersection_opens {E : Type u_4} [e_frm : Order.Frame E] [e_regular : Fact (regular E)] (U : Open E) : U.compl.toSublocale = ⨅ (V : Open E), ⨅ (_ : V ≪ U), { element := V.elementᶜ }.toSublocale

theorem Sublocale.intersection_Opens {E : Type u_4} [e_frm : Order.Frame E] [e_regular : Fact (regular E)] (a : Sublocale E) : ∃ (s : Set (Open E)), a = sInf (Open.toSublocale '' s)

theorem Sublocale.intersection_Open_Neighbourhhood {E : Type u_4} [e_frm : Order.Frame E] [e_regular : Fact (regular E)] (a : Sublocale E) : a = sInf (Open.toSublocale '' a.Open_Neighbourhood)

Leroy Lemme 2.2 TODO stone spaces als quelle vlt Seite 81. 1.2 Maybe depends on: Nucleus.eq_join_open_closed

theorem Sublocale.intersection_Neighbourhood {E : Type u_4} [e_frm : Order.Frame E] [e_regular : Fact (regular E)] (a : Sublocale E) : a = sInf a.Neighbourhood

theorem Measure.add_complement {E : Type u_4} [e_frm : Order.Frame E] [e_regular : Fact (regular E)] {m : Measure} (U : Open E) : m.toFun U + caratheodory U.compl.toSublocale = m.toFun ⊤

Leroy Lemme 3

noncomputable def Measure.restrict_open {E : Type u_4} [e_frm : Order.Frame E] (m : Measure) (w : Open E) : Open E → NNReal

Equations

• m.restrict_open w x = m.toFun (x ⊓ w)

theorem Measure.restrict_mono {E : Type u_4} [e_frm : Order.Frame E] {m : Measure} {w : Open E} (U V : Open E) : U ≤ V → m.restrict_open w U ≤ m.restrict_open w V

theorem Measure.restrict_pseudosymm {E : Type u_4} [e_frm : Order.Frame E] {m : Measure} {w U V : Open E} : m.restrict_open w (U ⊔ V) = m.restrict_open w U + m.restrict_open w V - m.restrict_open w (U ⊓ V)

theorem Measure.restrict_filtered {E : Type u_4} [e_frm : Order.Frame E] {m : Measure} {w : Open E} (s : Set (Open E)) : increasingly_filtered s → m.restrict_open w (sSup s) = sSup (m.restrict_open w '' s)

noncomputable def Measure.restrict_open_measure {E : Type u_4} [e_frm : Order.Frame E] (m : Measure) (w : Open E) : Measure

Equations

• m.restrict_open_measure w = { toFun := m.restrict_open w, empty := ⋯, mono := ⋯, strictly_additive := ⋯, filtered := ⋯ }

def Open_Interiors {E : Type u_4} [e_frm : Order.Frame E] (u : Sublocale E) : Set (Open E)

Equations

• Open_Interiors u = {w : Open E | w.toSublocale ≤ u}

theorem Measure.add_complement_inf {E : Type u_4} [e_frm : Order.Frame E] [e_regular : Fact (regular E)] {m : Measure} (u : Open E) (a : Sublocale E) : caratheodory a = caratheodory (a ⊓ u.toSublocale) + caratheodory (a ⊓ u.compl.toSublocale)

leroy Lemme 4:

theorem Measure.restrict_subadditive {E : Type u_4} [e_frm : Order.Frame E] [e_regular : Fact (regular E)] {m : Measure} {U V : Open E} {A : Sublocale E} : caratheodory (A ⊓ (U.toSublocale ⊔ V.toSublocale)) = caratheodory (A ⊓ U.toSublocale) + caratheodory (A ⊓ V.toSublocale) - caratheodory (A ⊓ U.toSublocale ⊓ V.toSublocale)

Leroy Corollary 1

theorem le_iSup_mem {E : Type u_4} [e_frm : Order.Frame E] (s : Set (Open E)) (a : NNReal) (f : Open E → NNReal) : (∀ b ∈ s, f b ≤ a) → ⨆ b ∈ s, f b ≤ a

theorem iSup_mem_eq {E : Type u_4} [e_frm : Order.Frame E] (s : Set (Open E)) (f : Open E → NNReal) (h_top : ∀ (a : Open E), f a ≤ f ⊤) : ⨆ b ∈ s, f b = sSup (Set.range fun (b : ↑s) => f ↑b)

theorem Measure.inf_filtered {E : Type u_4} [e_frm : Order.Frame E] [e_regular : Fact (regular E)] {m : Measure} (A : Sublocale E) (s : Set (Open E)) (h : increasingly_filtered s) : caratheodory (A ⊓ (sSup s).toSublocale) = ⨆ b ∈ s, caratheodory (A ⊓ b.toSublocale)

Leroy Lemme5

theorem Measure.inf_commutes_sSup {E : Type u_4} [e_frm : Order.Frame E] [e_regular : Fact (regular E)] {m : Measure} (A : Sublocale E) (s : Set (Open E)) (h : increasingly_filtered s) : caratheodory (A ⊓ (sSup s).toSublocale) = caratheodory (⨆ b ∈ s, A ⊓ b.toSublocale)