ClosureOperator.closure_sup_closure_left
theorem ClosureOperator.closure_sup_closure_left :
∀ {α : Type u_1} [inst : SemilatticeSup α] (c : ClosureOperator α) (x y : α), c (c x ⊔ y) = c (x ⊔ y)
This theorem states that for any type `α` with a sup-semilattice structure and any closure operator `c` on `α`, the closure of the sup of the closure of `x` and `y` is equal to the closure of the sup of `x` and `y`. In mathematical notation, this can be expressed as `c(c(x) ⊔ y) = c(x ⊔ y)`. This is about the idempotent nature of the closure operator and the compatibility with the `sup` operation in the semilattice.
In a more mathematical context, `α` can be any set equipped with a binary operation `sup` (also known as join) that is associative, commutative, and idempotent. A closure operator on `α` is a function `c: α -> α` that is extensive (`x ≤ c(x)`), increasing (`x ≤ y` then `c(x) ≤ c(y)`) and idempotent (`c(c(x)) = c(x)`).
More concisely: For any sup-semilattice `α` and closure operator `c` on `α`, `c(x ⊔ y) = c(x) ⊔ y = c(x ⊔ c(y))`, where `⊔` denotes the sup operation.
|
ClosureOperator.isClosed_closure
theorem ClosureOperator.isClosed_closure :
∀ {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) (x : α), c.IsClosed (c x)
This theorem states that for any type `α` that has a partial order, and for any closure operator `c` on this type, the closure of any element `x` of type `α` under the operator `c` is a closed element, according to the closure operator `c`. In other words, for any partial order and any closure operator defined on it, applying the closure operator to an element results in a closed element.
More concisely: For any type `α` with a partial order and any closure operator `c` on `α`, `c(x)` is a closed element under `c` for all `x` in `α`.
|
ClosureOperator.setOf_isClosed_eq_range_closure
theorem ClosureOperator.setOf_isClosed_eq_range_closure :
∀ {α : Type u_1} [inst : PartialOrder α] {c : ClosureOperator α}, {x | c.IsClosed x} = Set.range ⇑c
The theorem `ClosureOperator.setOf_isClosed_eq_range_closure` states that, for any type `α` with a partial order and any closure operator `c` on this type, the set of all elements for which `c.IsClosed` holds is exactly equivalent to the range of the function represented by the closure operator `c`. Here, the term "range" refers to the set of all possible outputs of a function, and a "closure operator" refers to a function that encapsulates the 'closure' properties of a mathematical structure, such as closure under addition in a group. In this case, `c.IsClosed` is a property that an element of the type `α` may have under the closure operator `c`.
More concisely: For any type `α` with a partial order and a closure operator `c`, the elements with property `IsClosed` under `c` are exactly the range of `c`.
|
ClosureOperator.le_closure'
theorem ClosureOperator.le_closure' :
∀ {α : Type u_1} [inst : Preorder α] (self : ClosureOperator α) (x : α), x ≤ self.toFun x
This theorem states that for any given type `α` equipped with a preorder, and for any closure operator defined on `α`, an element `x` of `α` is always less than or equal to its closure under the closure operator. In mathematical terms, for any `x` in `α`, we have `x ≤ closure(x)`, where `closure` denotes the closure operation.
More concisely: For any preordered type `α` and closure operator on `α`, for all `x` in `α`, we have `x ≤ closure x`.
|
LowerAdjoint.closed_eq_range_close
theorem LowerAdjoint.closed_eq_range_close :
∀ {α : Type u_1} {β : Type u_4} [inst : PartialOrder α] [inst_1 : PartialOrder β] {u : β → α} (l : LowerAdjoint u),
l.closed = Set.range (u ∘ l.toFun)
This theorem states that for any types `α` and `β` with `PartialOrder` structures, and for any function `u` from `β` to `α`, if `l` is a lower adjoint of `u`, then the set of closed elements for `l` is the range of `u` composed with `l`. In other words, every element in the set of closed elements for `l` corresponds to an element in the range of the composition of `u` and `l`. This links the concepts of adjointness and closure in ordered sets.
More concisely: For any functions `u: β → α` between partially ordered types, if `l` is a lower adjoint of `u`, then the set of closed elements for `l` equals the range of `u ∘ l`.
|
ClosureOperator.IsClosed.closure_eq
theorem ClosureOperator.IsClosed.closure_eq :
∀ {α : Type u_1} [inst : PartialOrder α] {c : ClosureOperator α} {x : α}, c.IsClosed x → c x = x
This theorem states that for any type `α`, under a partial order, given a closure operator `c` and an element `x` of type `α`, if `x` is a closed element under the closure operator `c`, then applying the closure operator `c` to `x` will not change `x`. In mathematical terms, if a set contains its closure under a closure operator, the closure of that set is equal to the set itself.
More concisely: If `α` is a type with a partial order and `c` is a closure operator on `α` such that `x` is a closed element under `c`, then `c(x) = x`.
|
ClosureOperator.le_closure_iff
theorem ClosureOperator.le_closure_iff :
∀ {α : Type u_1} [inst : PartialOrder α] {c : ClosureOperator α} {x y : α}, x ≤ c y ↔ c x ≤ c y
This theorem states that for any type `α` that has a `PartialOrder` structure, and for any `ClosureOperator` on `α`, and any elements `x` and `y` of type `α`, `x` is less than or equal to the closure of `y` if and only if the closure of `x` is less than or equal to the closure of `y`. In other words, this theorem illustrates an important property of closure operators in the context of partially ordered sets: it establishes the relationship between the order of the elements and their closures.
More concisely: For any type `α` with a `PartialOrder` structure and any `ClosureOperator` on `α`, the closure of `x` is less than or equal to the closure of `y` if and only if `x` is less than or equal to `y`.
|
closureOperator_gi_self
theorem closureOperator_gi_self :
∀ {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α), ⋯.closureOperator = c
This theorem states that for any given closure operator `c` on a partially ordered set `α`, the Galois insertion associated with `c` can be used to reconstruct that closure operator. However, it is important to note that the inverse operation, i.e., reconstructing the Galois insertion from the closure operator, doesn't generally hold true. This theorem is applicable to all types `α` with a given partial order.
More concisely: Given a closure operator `c` on a partially ordered set `α`, the Galois insertion `g` associated with `c` can be reconstructed as `g X = {x : α | ∃ y ∈ X, c y ⊆ {x}}`.
|
ClosureOperator.monotone
theorem ClosureOperator.monotone : ∀ {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α), Monotone ⇑c := by
sorry
The theorem `ClosureOperator.monotone` states that for any type `α` that has an instance of a partial order, any closure operator `c` on `α` is monotone. In other words, given any two elements `a` and `b` in `α` such that `a` is less than or equal to `b`, the application of the closure operator `c` preserves this order, i.e., `c(a)` is less than or equal to `c(b)`.
More concisely: For any type equipped with a partial order and any closure operator, the closure of a lesser element is less than or equal to the closure of a greater element.
|
ClosureOperator.idempotent'
theorem ClosureOperator.idempotent' :
∀ {α : Type u_1} [inst : Preorder α] (self : ClosureOperator α) (x : α), self.toFun (self.toFun x) = self.toFun x
This theorem, "ClosureOperator.idempotent'", states that for any given type `α` equipped with a `Preorder` instance and an instance of the `ClosureOperator` for `α`, applying the function associated with the closure operator twice to any element `x` of type `α` will yield the same result as applying it once. In more mathematical terms, closure operators are idempotent, meaning their application is invariant under repetition.
More concisely: For any type `α` with a `Preorder` and a `ClosureOperator`, the closure operator is idempotent, i.e., `ClosureOperator.apply (ClosureOperator.apply x) = ClosureOperator.apply x` for all `x` of type `α`.
|
LowerAdjoint.gc'
theorem LowerAdjoint.gc' :
∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {u : β → α} (self : LowerAdjoint u),
GaloisConnection self.toFun u
This theorem states that for any types `α` and `β` that have a preorder relation, and a function `u` from `β` to `α`, if there exists a lower adjoint `self` of the function `u`, then a Galois connection exists between the underlying function of the lower adjoint `self` and the function `u`. A Galois connection is a pair of functions `l` and `u` that satisfy the property `l a ≤ b ↔ a ≤ u b` for all `a` in `α` and `b` in `β`, and in the case of this theorem, the function `l` is the underlying function of the lower adjoint `self`.
More concisely: If `α` and `β` have a preorder relation and `u` is a function from `β` to `α` with a lower adjoint `self`, then `self` and `u` form a Galois connection.
|
ClosureOperator.IsClosed.closure_le_iff
theorem ClosureOperator.IsClosed.closure_le_iff :
∀ {α : Type u_1} [inst : PartialOrder α] {c : ClosureOperator α} {x y : α}, c.IsClosed y → (c x ≤ y ↔ x ≤ y) := by
sorry
This theorem states that for any type `α` equipped with a partial order, and for any closure operator `c` on `α`, if `y` is a closed element with respect to `c`, then `c x` is less than or equal to `y` if and only if `x` is less than or equal to `y`. This essentially means that the closure operation doesn't alter the order relation for any `x` when compared with a closed element `y`.
More concisely: For any type `α` with a partial order and closure operator `c`, if `y` is a closed element and `x` is less than or equal to `y`, then `c x` is less than or equal to `y`. Conversely, if `c x` is less than or equal to `y`, then `x` is less than or equal to `y`.
|
ClosureOperator.closure_min
theorem ClosureOperator.closure_min :
∀ {α : Type u_1} [inst : PartialOrder α] {c : ClosureOperator α} {x y : α}, x ≤ y → c.IsClosed y → c x ≤ y := by
sorry
This theorem states that for any type `α` endowed with a partial order and a `ClosureOperator c`, if `x` and `y` are elements of type `α` such that `x` is less than or equal to `y` and `y` is a closed element under the operator `c`, then the closure of `x` under operator `c` is less than or equal to `y`. In other words, if `x` is not greater than `y` and `y` is a "stable" point for the closure operation, then the closure of `x` won't exceed `y`.
More concisely: For any type `α` with a partial order and a closure operator `c`, if `x ≤ y` and `y` is closed under `c`, then `clo(x) ≤ y`, where `clo(x)` represents the closure of `x` under `c`.
|
LowerAdjoint.gc
theorem LowerAdjoint.gc :
∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u),
GaloisConnection l.toFun u
This theorem states that for any two types `α` and `β` that are preorders, and a function `u` from `β` to `α`, if `l` is a lower adjoint of `u`, then `l` and `u` form a Galois connection. In other words, for any elements `a` from `α` and `b` from `β`, `l a` is less than or equal to `b` if and only if `a` is less than or equal to `u b`. This theorem is a specific case of the Galois connection concept from order theory and category theory.
More concisely: For any preorders `α` and `β` and a function `u` from `β` to `α`, if `l` is a lower adjoint of `u`, then `l` and `u` form a Galois connection, i.e., for all `a ∈ α` and `b ∈ β`, `l a ≤ b` if and only if `a ≤ u b`.
|
ClosureOperator.idempotent
theorem ClosureOperator.idempotent :
∀ {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) (x : α), c (c x) = c x
This theorem states that for any type `α` that has a partial order, and for any closure operator `c` defined on that type, applying `c` twice to any element `x` of type `α` is the same as applying `c` once. In other words, the closure operator `c` is idempotent: for every `x` in `α`, `c(c(x))` equals `c(x)`. This is a property common to many mathematical operators, such as the closure of a set in topology.
More concisely: For any partial order type `α` and closure operator `c` on `α`, `c(c(x)) = c(x)` for all `x` in `α`.
|
LowerAdjoint.le_closure
theorem LowerAdjoint.le_closure :
∀ {α : Type u_1} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α),
x ≤ u (l.toFun x)
The theorem `LowerAdjoint.le_closure` states that for any given types `α` and `β` with preorders, and a function `u` mapping `β` to `α`, if `l` is a lower adjoint of `u`, then any element `x` from `α` is less than or equal to the result of applying `u` to the result of applying `l.toFun` to `x`. This is a property sometimes referred to as extensivity or inflationarity.
More concisely: For any types with preorders `α` and `β`, and a lower adjoint `l` of a function `u` from `β` to `α`, `x ≤ u (l.toFun x)` holds for all `x` in `α`.
|
ClosureOperator.closure_top
theorem ClosureOperator.closure_top :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] (c : ClosureOperator α), c ⊤ = ⊤
This theorem states that for any given closure operator `c` defined on a partially ordered set `α` that also has a top element, the result of applying the closure operator `c` to the top element is always the top element itself. The partial order and the top element are given as preconditions in the theorem, and `c` is the closure operator being considered. The theorem is essentially saying that the closure of the top element under any closure operator in this context is still the top element.
More concisely: For any closure operator `c` on a partially ordered set `α` with a top element, the closure of the top element under `c` equals the top element.
|
ClosureOperator.le_closure
theorem ClosureOperator.le_closure :
∀ {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α) (x : α), x ≤ c x
This theorem states that for any type `α` under a partial order, and for any closure operator `c` on `α`, every element `x` of `α` is less than or equal to its closure (`c x`). This property is sometimes referred to as extensivity or inflationarity. In mathematical notation, this can be written as `∀x ∈ α, x ≤ c(x)`.
More concisely: For any type `α` under a partial order and closure operator `c` on `α`, every element `x` satisfies `x ≤ c(x)`.
|
ClosureOperator.closure_sup_closure_right
theorem ClosureOperator.closure_sup_closure_right :
∀ {α : Type u_1} [inst : SemilatticeSup α] (c : ClosureOperator α) (x y : α), c (x ⊔ c y) = c (x ⊔ y)
This theorem states that for any given type `α` equipped with a semilattice (a structure with an associative, commutative, and idempotent binary operation "sup"), and for any closure operator `c` on this type, the result of applying `c` to the supremum of `x` and the closure of `y` (denoted `c (x ⊔ c y)`) is the same as the result of applying `c` to the supremum of `x` and `y` (denoted `c (x ⊔ y)`). In effect, this means that the closure of `y` under the operator `c` can be "pulled out" of the supremum operation without changing the overall result of the computation.
More concisely: For any semilattice `α` and closure operator `c` on `α`, the application of `c` to the supremum of `x` and `c y` is equal to the application of `c` to the supremum of `x` and `y`. In other words, `c (x ⊔ y) = c (x ⊔ c y)`.
|
ClosureOperator.eq_ofPred_closed
theorem ClosureOperator.eq_ofPred_closed :
∀ {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α),
c = ClosureOperator.ofPred (⇑c) c.IsClosed ⋯ ⋯ ⋯
This theorem states that for any given closure operator `c` on a partially ordered type `α`, `c` is equivalent to the closure operator constructed from the function underlying `c` and the predicate `c.IsClosed`. This is realized using the `ClosureOperator.ofPred` constructor, demonstrating the redundancy of these two different ways to construct a closure operator, thereby ensuring consistency and interchangeability in the context where both methods are used.
More concisely: For any closure operator `c` on a partially ordered type `α`, `c` is equivalent to the closure operator constructed from `c.fn` and `c.IsClosed` using `ClosureOperator.ofPred`.
|