def Sublocale.embed {E' : Type u_1} [Order.Frame E'] {A : Sublocale E'} (b : Sublocale ↑(Image A)) : Sublocale E'

Equations

• Sublocale.embed b = { toFun := fun (x : E') => f_untenstern (Nucleus.frameHom A) (b ((Nucleus.frameHom A) x)), map_inf' := ⋯, idempotent' := ⋯, le_apply' := ⋯ }

theorem Sublocale.embed_top {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') : embed ⊤ = A

theorem Sublocale.embed_bot {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') : embed ⊥ = ⊥

theorem Sublocale.embed_open_eq_inf {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') (u : Open ↑(Image A)) : embed u.toSublocale = A ⊓ { element := ↑u.element }.toSublocale

theorem Sublocale.embed_open_sup {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') (u v : Open ↑(Image A)) : embed (u.toSublocale ⊔ v.toSublocale) = embed u.toSublocale ⊔ embed v.toSublocale

theorem Sublocale.embed_open_sSup {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') (s : Set (Open ↑(Image A))) : embed (sSup s).toSublocale = ⨆ a ∈ s, embed a.toSublocale

theorem Sublocale.embed.mono {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') : Monotone embed

theorem Image_himp_closed {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') (a b : E') (h1 : a ∈ Image A) (h2 : b ∈ Image A) : a ⇨ b ∈ Image A

@[simp]

theorem Nucleus.frameHom.of_coe {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') (i : ↑(Image A)) : (frameHom A) ↑i = i

def Sublocale.restrict {E' : Type u_1} [Order.Frame E'] (A b : Sublocale E') (h : b ≤ A) : Sublocale ↑(Image A)

Equations

• A.restrict b h = { toFun := fun (x : ↑(Image A)) => (Nucleus.frameHom A) (b ↑x), map_inf' := ⋯, idempotent' := ⋯, le_apply' := ⋯ }

theorem Sublocale.embed_le {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') (b : Sublocale ↑(Image A)) : embed b ≤ A

theorem Sublocale.restrict_mono {E' : Type u_1} [Order.Frame E'] (A b a : Sublocale E') (h1 : b ≤ A) (h2 : a ≤ A) : a ≤ b → A.restrict a h2 ≤ A.restrict b h1

theorem Sublocale.restrict_embed {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') (b : Sublocale ↑(Image A)) : A.restrict (embed b) ⋯ = b

theorem Sublocale.embed_restrict {E' : Type u_1} [Order.Frame E'] (A b : Sublocale E') (h : b ≤ A) : embed (A.restrict b h) = b

def Sublocale.restrict_open {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') (u : Open E') : Open ↑(Image A)

Equations

• A.restrict_open u = { element := (Nucleus.frameHom A) u.element }

theorem Sublocale.embed_restrict_open {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') (u : Open E') : embed (A.restrict_open u).toSublocale = A ⊓ u.toSublocale

theorem Sublocale.embed_orderiso {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') (a b : Sublocale ↑(Image A)) : embed a ≤ embed b → a ≤ b

theorem Sublocale.restrict_orderiso {E' : Type u_1} [Order.Frame E'] (A a b : Sublocale E') (h1 : a ≤ A) (h2 : b ≤ A) : A.restrict a h1 ≤ A.restrict b h2 → a ≤ b

theorem Sublocale.restrict_open_eq_restrict {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') (u : Open E') : (A.restrict_open u).toSublocale = A.restrict (A ⊓ u.toSublocale) ⋯

theorem Sublocale.Image_regular' {E' : Type u_1} [Order.Frame E'] [e_regular : Fact (regular E')] (A : Sublocale E') : regular ↑(Image A)

TODO woanders

noncomputable def Measure.restrict_sublocale {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') (m : Measure) : Open ↑(Image A) → NNReal

Equations

• Measure.restrict_sublocale A m x = Measure.caratheodory (Sublocale.embed x.toSublocale)

noncomputable def Measure.restrict_sublocale_measure {E' : Type u_1} [Order.Frame E'] (A : Sublocale E') (m : Measure) [Fact (regular E')] : Measure

Equations

• Measure.restrict_sublocale_measure A m = { toFun := Measure.restrict_sublocale A m, empty := ⋯, mono := ⋯, strictly_additive := ⋯, filtered := ⋯ }