Documentation

Mathlib.Order.Closure

Closure operators between preorders #

We define (bundled) closure operators on a preorder as monotone (increasing), extensive (inflationary) and idempotent functions. We define closed elements for the operator as elements which are fixed by it.

Lower adjoints to a function between preorders u : β → α allow to generalise closure operators to situations where the closure operator we are dealing with naturally decomposes as u ∘ l where l is a worthy function to have on its own. Typical examples include l : Set G → Subgroup G := Subgroup.closure, u : Subgroup G → Set G := (↑), where G is a group. This shows there is a close connection between closure operators, lower adjoints and Galois connections/insertions: every Galois connection induces a lower adjoint which itself induces a closure operator by composition (see GaloisConnection.lowerAdjoint and LowerAdjoint.closureOperator), and every closure operator on a partial order induces a Galois insertion from the set of closed elements to the underlying type (see ClosureOperator.gi).

Main definitions #

Implementation details #

Although LowerAdjoint is technically a generalisation of ClosureOperator (by defining toFun := id), it is desirable to have both as otherwise ids would be carried all over the place when using concrete closure operators such as ConvexHull.

LowerAdjoint really is a semibundled structure version of GaloisConnection.

References #

Closure operator #

structure ClosureOperator (α : Type u_1) [Preorder α] extends α →o α :
Type u_1

A closure operator on the preorder α is a monotone function which is extensive (every x is less than its closure) and idempotent.

  • toFun : αα
  • le_closure' (x : α) : x self.toFun x

    An element is less than or equal its closure

  • idempotent' (x : α) : self.toFun (self.toFun x) = self.toFun x

    Closures are idempotent

  • IsClosed (x : α) : Prop

    Predicate for an element to be closed.

    By default, this is defined as c.IsClosed x := (c x = x) (see isClosed_iff). We allow an override to fix definitional equalities.

  • isClosed_iff {x : α} : self.IsClosed x self.toFun x = x
Instances For
    instance ClosureOperator.instFunLike (α : Type u_1) [Preorder α] :
    Equations
      def ClosureOperator.conjBy {α : Type u_4} {β : Type u_5} [Preorder α] [Preorder β] (c : ClosureOperator α) (e : α ≃o β) :

      If c is a closure operator on α and e an order-isomorphism between α and β then e ∘ c ∘ e⁻¹ is a closure operator on β.

      Equations
        Instances For
          @[simp]
          theorem ClosureOperator.conjBy_apply {α : Type u_4} {β : Type u_5} [Preorder α] [Preorder β] (c : ClosureOperator α) (e : α ≃o β) (a : β) :
          (c.conjBy e) a = (e.conj c) a
          theorem ClosureOperator.conjBy_trans {α : Type u_4} {β : Type u_5} {γ : Type u_6} [Preorder α] [Preorder β] [Preorder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ) (c : ClosureOperator α) :
          c.conjBy (e₁.trans e₂) = (c.conjBy e₁).conjBy e₂

          The identity function as a closure operator.

          Equations
            Instances For
              @[simp]
              theorem ClosureOperator.id_apply (α : Type u_1) [PartialOrder α] (a : α) :
              (id α) a = a
              @[simp]
              theorem ClosureOperator.id_isClosed (α : Type u_1) [PartialOrder α] (x✝ : α) :
              (id α).IsClosed x✝ = True
              theorem ClosureOperator.ext {α : Type u_1} [PartialOrder α] (c₁ c₂ : ClosureOperator α) :
              (∀ (x : α), c₁ x = c₂ x)c₁ = c₂
              theorem ClosureOperator.ext_iff {α : Type u_1} [PartialOrder α] {c₁ c₂ : ClosureOperator α} :
              c₁ = c₂ ∀ (x : α), c₁ x = c₂ x
              def ClosureOperator.mk' {α : Type u_1} [PartialOrder α] (f : αα) (hf₁ : Monotone f) (hf₂ : ∀ (x : α), x f x) (hf₃ : ∀ (x : α), f (f x) f x) :

              Constructor for a closure operator using the weaker idempotency axiom: f (f x) ≤ f x.

              Equations
                Instances For
                  @[simp]
                  theorem ClosureOperator.mk'_apply {α : Type u_1} [PartialOrder α] (f : αα) (hf₁ : Monotone f) (hf₂ : ∀ (x : α), x f x) (hf₃ : ∀ (x : α), f (f x) f x) (a✝ : α) :
                  (mk' f hf₁ hf₂ hf₃) a✝ = f a✝
                  @[simp]
                  theorem ClosureOperator.mk'_isClosed {α : Type u_1} [PartialOrder α] (f : αα) (hf₁ : Monotone f) (hf₂ : ∀ (x : α), x f x) (hf₃ : ∀ (x : α), f (f x) f x) (x : α) :
                  (mk' f hf₁ hf₂ hf₃).IsClosed x = (f x = x)
                  def ClosureOperator.mk₂ {α : Type u_1} [PartialOrder α] (f : αα) (hf : ∀ (x : α), x f x) (hmin : ∀ ⦃x y : α⦄, x f yf x f y) :

                  Convenience constructor for a closure operator using the weaker minimality axiom: x ≤ f y → f x ≤ f y, which is sometimes easier to prove in practice.

                  Equations
                    Instances For
                      @[simp]
                      theorem ClosureOperator.mk₂_apply {α : Type u_1} [PartialOrder α] (f : αα) (hf : ∀ (x : α), x f x) (hmin : ∀ ⦃x y : α⦄, x f yf x f y) (a✝ : α) :
                      (mk₂ f hf hmin) a✝ = f a✝
                      @[simp]
                      theorem ClosureOperator.mk₂_isClosed {α : Type u_1} [PartialOrder α] (f : αα) (hf : ∀ (x : α), x f x) (hmin : ∀ ⦃x y : α⦄, x f yf x f y) (x : α) :
                      (mk₂ f hf hmin).IsClosed x = (f x = x)
                      def ClosureOperator.ofPred {α : Type u_1} [PartialOrder α] (f : αα) (p : αProp) (hf : ∀ (x : α), x f x) (hfp : ∀ (x : α), p (f x)) (hmin : ∀ ⦃x y : α⦄, x yp yf x y) :

                      Construct a closure operator from an inflationary function f and a "closedness" predicate p witnessing minimality of f x among closed elements greater than x.

                      Equations
                        Instances For
                          @[simp]
                          theorem ClosureOperator.ofPred_apply {α : Type u_1} [PartialOrder α] (f : αα) (p : αProp) (hf : ∀ (x : α), x f x) (hfp : ∀ (x : α), p (f x)) (hmin : ∀ ⦃x y : α⦄, x yp yf x y) (a✝ : α) :
                          (ofPred f p hf hfp hmin) a✝ = f a✝
                          @[simp]
                          theorem ClosureOperator.ofPred_isClosed {α : Type u_1} [PartialOrder α] (f : αα) (p : αProp) (hf : ∀ (x : α), x f x) (hfp : ∀ (x : α), p (f x)) (hmin : ∀ ⦃x y : α⦄, x yp yf x y) (a✝ : α) :
                          (ofPred f p hf hfp hmin).IsClosed a✝ = p a✝
                          theorem ClosureOperator.le_closure {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) (x : α) :
                          x c x

                          Every element is less than its closure. This property is sometimes referred to as extensivity or inflationarity.

                          @[simp]
                          theorem ClosureOperator.idempotent {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) (x : α) :
                          c (c x) = c x
                          @[simp]
                          theorem ClosureOperator.isClosed_closure {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) (x : α) :
                          c.IsClosed (c x)
                          @[reducible, inline]
                          abbrev ClosureOperator.Closeds {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) :
                          Type u_1

                          The type of elements closed under a closure operator.

                          Equations
                            Instances For
                              def ClosureOperator.toCloseds {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) (x : α) :

                              Send an element to a closed element (by taking the closure).

                              Equations
                                Instances For
                                  theorem ClosureOperator.IsClosed.closure_eq {α : Type u_1} [PartialOrder α] {c : ClosureOperator α} {x : α} :
                                  c.IsClosed xc x = x

                                  The set of closed elements for c is exactly its range.

                                  theorem ClosureOperator.le_closure_iff {α : Type u_1} [PartialOrder α] {c : ClosureOperator α} {x y : α} :
                                  x c y c x c y
                                  @[simp]
                                  theorem ClosureOperator.IsClosed.closure_le_iff {α : Type u_1} [PartialOrder α] {c : ClosureOperator α} {x y : α} (hy : c.IsClosed y) :
                                  c x y x y
                                  theorem ClosureOperator.closure_min {α : Type u_1} [PartialOrder α] {c : ClosureOperator α} {x y : α} (hxy : x y) (hy : c.IsClosed y) :
                                  c x y
                                  theorem ClosureOperator.closure_isGLB {α : Type u_1} [PartialOrder α] {c : ClosureOperator α} (x : α) :
                                  IsGLB {y : α | x y c.IsClosed y} (c x)
                                  theorem ClosureOperator.ext_isClosed {α : Type u_1} [PartialOrder α] (c₁ c₂ : ClosureOperator α) (h : ∀ (x : α), c₁.IsClosed x c₂.IsClosed x) :
                                  c₁ = c₂
                                  theorem ClosureOperator.eq_ofPred_closed {α : Type u_1} [PartialOrder α] (c : ClosureOperator α) :
                                  c = ofPred (⇑c) c.IsClosed

                                  A closure operator is equal to the closure operator obtained by feeding c.closed into the ofPred constructor.

                                  @[simp]
                                  theorem ClosureOperator.closure_inf_le {α : Type u_1} [SemilatticeInf α] (c : ClosureOperator α) (x y : α) :
                                  c (xy) c xc y
                                  theorem ClosureOperator.closure_sup_closure_le {α : Type u_1} [SemilatticeSup α] (c : ClosureOperator α) (x y : α) :
                                  c xc y c (xy)
                                  theorem ClosureOperator.closure_sup_closure_left {α : Type u_1} [SemilatticeSup α] (c : ClosureOperator α) (x y : α) :
                                  c (c xy) = c (xy)
                                  theorem ClosureOperator.closure_sup_closure_right {α : Type u_1} [SemilatticeSup α] (c : ClosureOperator α) (x y : α) :
                                  c (xc y) = c (xy)
                                  theorem ClosureOperator.closure_sup_closure {α : Type u_1} [SemilatticeSup α] (c : ClosureOperator α) (x y : α) :
                                  c (c xc y) = c (xy)
                                  def ClosureOperator.ofCompletePred {α : Type u_1} [CompleteLattice α] (p : αProp) (hsinf : ∀ (s : Set α), (∀ as, p a)p (sInf s)) :

                                  Define a closure operator from a predicate that's preserved under infima.

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem ClosureOperator.ofCompletePred_apply {α : Type u_1} [CompleteLattice α] (p : αProp) (hsinf : ∀ (s : Set α), (∀ as, p a)p (sInf s)) (a : α) :
                                      (ofCompletePred p hsinf) a = ⨅ (b : { b : α // a b p b }), b
                                      @[simp]
                                      theorem ClosureOperator.ofCompletePred_isClosed {α : Type u_1} [CompleteLattice α] (p : αProp) (hsinf : ∀ (s : Set α), (∀ as, p a)p (sInf s)) (a✝ : α) :
                                      (ofCompletePred p hsinf).IsClosed a✝ = p a✝
                                      theorem ClosureOperator.sInf_isClosed {α : Type u_1} [CompleteLattice α] {c : ClosureOperator α} {S : Set α} (H : xS, c.IsClosed x) :
                                      @[simp]
                                      theorem ClosureOperator.closure_iSup_closure {α : Type u_1} {ι : Sort u_2} [CompleteLattice α] (c : ClosureOperator α) (f : ια) :
                                      c (⨆ (i : ι), c (f i)) = c (⨆ (i : ι), f i)
                                      @[simp]
                                      theorem ClosureOperator.closure_iSup₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} [CompleteLattice α] (c : ClosureOperator α) (f : (i : ι) → κ iα) :
                                      c (⨆ (i : ι), ⨆ (j : κ i), c (f i j)) = c (⨆ (i : ι), ⨆ (j : κ i), f i j)
                                      def OrderIso.equivClosureOperator {α : Type u_4} {β : Type u_5} [Preorder α] [Preorder β] (e : α ≃o β) :

                                      Conjugating ClosureOperators on α and on β by a fixed isomorphism e : α ≃o β gives an equivalence ClosureOperator α ≃ ClosureOperator β.

                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem OrderIso.equivClosureOperator_apply {α : Type u_4} {β : Type u_5} [Preorder α] [Preorder β] (e : α ≃o β) (c : ClosureOperator α) :
                                          @[simp]
                                          theorem OrderIso.equivClosureOperator_symm_apply {α : Type u_4} {β : Type u_5} [Preorder α] [Preorder β] (e : α ≃o β) (c : ClosureOperator β) :

                                          Lower adjoint #

                                          structure LowerAdjoint {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] (u : βα) :
                                          Type (max u_1 u_4)

                                          A lower adjoint of u on the preorder α is a function l such that l and u form a Galois connection. It allows us to define closure operators whose output does not match the input. In practice, u is often (↑) : β → α.

                                          • toFun : αβ

                                            The underlying function

                                          • gc' : GaloisConnection self.toFun u

                                            The underlying function is a lower adjoint.

                                          Instances For

                                            The identity function as a lower adjoint to itself.

                                            Equations
                                              Instances For
                                                @[simp]
                                                theorem LowerAdjoint.id_toFun (α : Type u_1) [Preorder α] (x : α) :
                                                instance LowerAdjoint.instCoeFunForall {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : βα} :
                                                CoeFun (LowerAdjoint u) fun (x : LowerAdjoint u) => αβ
                                                Equations
                                                  theorem LowerAdjoint.gc {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : βα} (l : LowerAdjoint u) :
                                                  theorem LowerAdjoint.ext {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : βα} (l₁ l₂ : LowerAdjoint u) :
                                                  l₁.toFun = l₂.toFunl₁ = l₂
                                                  theorem LowerAdjoint.ext_iff {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : βα} {l₁ l₂ : LowerAdjoint u} :
                                                  l₁ = l₂ l₁.toFun = l₂.toFun
                                                  theorem LowerAdjoint.monotone {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : βα} (l : LowerAdjoint u) :
                                                  theorem LowerAdjoint.le_closure {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : βα} (l : LowerAdjoint u) (x : α) :
                                                  x u (l.toFun x)

                                                  Every element is less than its closure. This property is sometimes referred to as extensivity or inflationarity.

                                                  def LowerAdjoint.closureOperator {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {u : βα} (l : LowerAdjoint u) :

                                                  Every lower adjoint induces a closure operator given by the composition. This is the partial order version of the statement that every adjunction induces a monad.

                                                  Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem LowerAdjoint.closureOperator_isClosed {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {u : βα} (l : LowerAdjoint u) (x : α) :
                                                      l.closureOperator.IsClosed x = ((fun (x : α) => u (l.toFun x)) x = x)
                                                      @[simp]
                                                      theorem LowerAdjoint.closureOperator_apply {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {u : βα} (l : LowerAdjoint u) (x : α) :
                                                      l.closureOperator x = u (l.toFun x)
                                                      theorem LowerAdjoint.idempotent {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {u : βα} (l : LowerAdjoint u) (x : α) :
                                                      u (l.toFun (u (l.toFun x))) = u (l.toFun x)
                                                      theorem LowerAdjoint.le_closure_iff {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {u : βα} (l : LowerAdjoint u) (x y : α) :
                                                      x u (l.toFun y) u (l.toFun x) u (l.toFun y)
                                                      def LowerAdjoint.closed {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : βα} (l : LowerAdjoint u) :
                                                      Set α

                                                      An element x is closed for l : LowerAdjoint u if it is a fixed point: u (l x) = x

                                                      Equations
                                                        Instances For
                                                          theorem LowerAdjoint.mem_closed_iff {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : βα} (l : LowerAdjoint u) (x : α) :
                                                          x l.closed u (l.toFun x) = x
                                                          theorem LowerAdjoint.closure_eq_self_of_mem_closed {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : βα} (l : LowerAdjoint u) {x : α} (h : x l.closed) :
                                                          u (l.toFun x) = x
                                                          theorem LowerAdjoint.mem_closed_iff_closure_le {α : Type u_1} {β : Type u_4} [PartialOrder α] [PartialOrder β] {u : βα} (l : LowerAdjoint u) (x : α) :
                                                          x l.closed u (l.toFun x) x
                                                          @[simp]
                                                          theorem LowerAdjoint.closure_is_closed {α : Type u_1} {β : Type u_4} [PartialOrder α] [PartialOrder β] {u : βα} (l : LowerAdjoint u) (x : α) :
                                                          u (l.toFun x) l.closed
                                                          theorem LowerAdjoint.closed_eq_range_close {α : Type u_1} {β : Type u_4} [PartialOrder α] [PartialOrder β] {u : βα} (l : LowerAdjoint u) :

                                                          The set of closed elements for l is the range of u ∘ l.

                                                          def LowerAdjoint.toClosed {α : Type u_1} {β : Type u_4} [PartialOrder α] [PartialOrder β] {u : βα} (l : LowerAdjoint u) (x : α) :
                                                          l.closed

                                                          Send an x to an element of the set of closed elements (by taking the closure).

                                                          Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem LowerAdjoint.closure_le_closed_iff_le {α : Type u_1} {β : Type u_4} [PartialOrder α] [PartialOrder β] {u : βα} (l : LowerAdjoint u) (x : α) {y : α} (hy : l.closed y) :
                                                              u (l.toFun x) y x y
                                                              theorem LowerAdjoint.closure_top {α : Type u_1} {β : Type u_4} [PartialOrder α] [OrderTop α] [Preorder β] {u : βα} (l : LowerAdjoint u) :
                                                              u (l.toFun ) =
                                                              theorem LowerAdjoint.closure_inf_le {α : Type u_1} {β : Type u_4} [SemilatticeInf α] [Preorder β] {u : βα} (l : LowerAdjoint u) (x y : α) :
                                                              u (l.toFun (xy)) u (l.toFun x)u (l.toFun y)
                                                              theorem LowerAdjoint.closure_sup_closure_le {α : Type u_1} {β : Type u_4} [SemilatticeSup α] [Preorder β] {u : βα} (l : LowerAdjoint u) (x y : α) :
                                                              u (l.toFun x)u (l.toFun y) u (l.toFun (xy))
                                                              theorem LowerAdjoint.closure_sup_closure_left {α : Type u_1} {β : Type u_4} [SemilatticeSup α] [Preorder β] {u : βα} (l : LowerAdjoint u) (x y : α) :
                                                              u (l.toFun (u (l.toFun x)y)) = u (l.toFun (xy))
                                                              theorem LowerAdjoint.closure_sup_closure_right {α : Type u_1} {β : Type u_4} [SemilatticeSup α] [Preorder β] {u : βα} (l : LowerAdjoint u) (x y : α) :
                                                              u (l.toFun (xu (l.toFun y))) = u (l.toFun (xy))
                                                              theorem LowerAdjoint.closure_sup_closure {α : Type u_1} {β : Type u_4} [SemilatticeSup α] [Preorder β] {u : βα} (l : LowerAdjoint u) (x y : α) :
                                                              u (l.toFun (u (l.toFun x)u (l.toFun y))) = u (l.toFun (xy))
                                                              theorem LowerAdjoint.closure_iSup_closure {α : Type u_1} {ι : Sort u_2} {β : Type u_4} [CompleteLattice α] [Preorder β] {u : βα} (l : LowerAdjoint u) (f : ια) :
                                                              u (l.toFun (⨆ (i : ι), u (l.toFun (f i)))) = u (l.toFun (⨆ (i : ι), f i))
                                                              theorem LowerAdjoint.closure_iSup₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {β : Type u_4} [CompleteLattice α] [Preorder β] {u : βα} (l : LowerAdjoint u) (f : (i : ι) → κ iα) :
                                                              u (l.toFun (⨆ (i : ι), ⨆ (j : κ i), u (l.toFun (f i j)))) = u (l.toFun (⨆ (i : ι), ⨆ (j : κ i), f i j))
                                                              theorem LowerAdjoint.subset_closure {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) :
                                                              s (l.toFun s)
                                                              theorem LowerAdjoint.notMem_of_notMem_closure {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) {s : Set β} {P : β} (hP : Pl.toFun s) :
                                                              Ps
                                                              @[deprecated LowerAdjoint.notMem_of_notMem_closure (since := "2025-05-23")]
                                                              theorem LowerAdjoint.not_mem_of_not_mem_closure {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) {s : Set β} {P : β} (hP : Pl.toFun s) :
                                                              Ps

                                                              Alias of LowerAdjoint.notMem_of_notMem_closure.

                                                              theorem LowerAdjoint.le_iff_subset {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) (S : α) :
                                                              l.toFun s S s S
                                                              theorem LowerAdjoint.mem_iff {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (s : Set β) (x : β) :
                                                              x l.toFun s ∀ (S : α), s Sx S
                                                              theorem LowerAdjoint.eq_of_le {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) {s : Set β} {S : α} (h₁ : s S) (h₂ : S l.toFun s) :
                                                              l.toFun s = S
                                                              theorem LowerAdjoint.closure_union_closure_subset {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (x y : α) :
                                                              (l.toFun x) (l.toFun y) (l.toFun (x y))
                                                              @[simp]
                                                              theorem LowerAdjoint.closure_union_closure_left {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (x y : α) :
                                                              l.toFun ((l.toFun x) y) = l.toFun (x y)
                                                              @[simp]
                                                              theorem LowerAdjoint.closure_union_closure_right {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (x y : α) :
                                                              l.toFun (x (l.toFun y)) = l.toFun (x y)
                                                              theorem LowerAdjoint.closure_union_closure {α : Type u_1} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (x y : α) :
                                                              l.toFun ((l.toFun x) (l.toFun y)) = l.toFun (x y)
                                                              @[simp]
                                                              theorem LowerAdjoint.closure_iUnion_closure {α : Type u_1} {ι : Sort u_2} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (f : ια) :
                                                              l.toFun (⋃ (i : ι), (l.toFun (f i))) = l.toFun (⋃ (i : ι), (f i))
                                                              @[simp]
                                                              theorem LowerAdjoint.closure_iUnion₂_closure {α : Type u_1} {ι : Sort u_2} {κ : ιSort u_3} {β : Type u_4} [SetLike α β] (l : LowerAdjoint SetLike.coe) (f : (i : ι) → κ iα) :
                                                              l.toFun (⋃ (i : ι), ⋃ (j : κ i), (l.toFun (f i j))) = l.toFun (⋃ (i : ι), ⋃ (j : κ i), (f i j))

                                                              Translations between GaloisConnection, LowerAdjoint, ClosureOperator #

                                                              def GaloisConnection.lowerAdjoint {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {l : αβ} {u : βα} (gc : GaloisConnection l u) :

                                                              Every Galois connection induces a lower adjoint.

                                                              Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem GaloisConnection.lowerAdjoint_toFun {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {l : αβ} {u : βα} (gc : GaloisConnection l u) (a✝ : α) :
                                                                  gc.lowerAdjoint.toFun a✝ = l a✝
                                                                  def GaloisConnection.closureOperator {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {l : αβ} {u : βα} (gc : GaloisConnection l u) :

                                                                  Every Galois connection induces a closure operator given by the composition. This is the partial order version of the statement that every adjunction induces a monad.

                                                                  Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem GaloisConnection.closureOperator_isClosed {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {l : αβ} {u : βα} (gc : GaloisConnection l u) (x : α) :
                                                                      gc.closureOperator.IsClosed x = (u (l x) = x)
                                                                      @[simp]
                                                                      theorem GaloisConnection.closureOperator_apply {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {l : αβ} {u : βα} (gc : GaloisConnection l u) (x : α) :
                                                                      gc.closureOperator x = u (l x)

                                                                      The set of closed elements has a Galois insertion to the underlying type.

                                                                      Equations
                                                                        Instances For
                                                                          @[simp]

                                                                          The Galois insertion associated to a closure operator can be used to reconstruct the closure operator. Note that the inverse in the opposite direction does not hold in general.