def Image {X : Type u_1} [Order.Frame X] (e : Nucleus X) : Set X

Equations

• Image e = {v : X | e v = v}

instance instCoeNucleusSet_leroy {X : Type u_1} [Order.Frame X] : Coe (Nucleus X) (Set X)

Equations

• instCoeNucleusSet_leroy = { coe := fun (x : Nucleus X) => Image x }

instance image_frame {E : Type u_3} [Order.Frame E] (n : Nucleus E) : Order.Frame ↑(Image n)

Equations

• image_frame n = Order.Frame.ofMinimalAxioms (Order.Frame.MinimalAxioms.mk ⋯)

instance inst_frame {E : Type u_3} [Order.Frame E] (n : Nucleus E) : Order.Frame ↑(Image n)

Equations

• inst_frame n = image_frame n

def Nucleus.frameHom {E : Type u_3} [Order.Frame E] (n : Nucleus E) : FrameHom E ↑(Image n)

Equations

• n.frameHom = { toFun := Set.codRestrict (⇑n) (Image n) ⋯, map_inf' := ⋯, map_top' := ⋯, map_sSup' := ⋯ }

def f_untenstern {X : Type u_1} {Y : Type u_2} [Order.Frame X] [Order.Frame Y] (f : FrameHom X Y) (y : Y) : X

Equations

• f_untenstern f y = sSup {w : X | f w ≤ y}

theorem Nucleus.gc {E : Type u_3} [Order.Frame E] (n : Nucleus E) : GaloisConnection (⇑n.frameHom) (f_untenstern n.frameHom)

theorem Nucleus.gc' {E : Type u_3} [Order.Frame E] (n : Nucleus E) : GaloisConnection (⇑n.frameHom) Subtype.val

theorem f_untenstern_eq_val {E : Type u_3} [Order.Frame E] (n : Nucleus E) : f_untenstern n.frameHom = Subtype.val