DirSupInacc.of_compl
theorem DirSupInacc.of_compl : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, DirSupInacc sᶜ → DirSupClosed s := by
sorry
The theorem `DirSupInacc.of_compl` states that for any type `α` equipped with a preorder, and for any set `s` of elements of type `α`, if the complement of `s` (`sᶜ`) is inaccessible by directed joins, then `s` is closed under directed joins. In simple terms, if no directed join can reach the outside of `s`, then any directed join that starts within `s` remains within `s`.
More concisely: If the complement of a set in a preordered type is inaccessible by directed joins, then the set is closed under directed joins.
|
Topology.IsScott.topology_eq
theorem Topology.IsScott.topology_eq :
∀ (α : Type u_1) [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsScott α],
inst_1 = Topology.scott α
This theorem states that for any type 'α' that is preordered and is endowed with a topological space and a Scott topology, the topology of that type 'α' is equal to the Scott topology. In other words, if we have a set that carries a pre-order (which is a binary relation indicating that, for certain pairs of elements in the set, one of the elements precedes the other in some ordering sequence) and a topology (which determines the closeness structure of elements), and if this set also carries a Scott topology (which is a specific kind of topology defined as the join of the topology of upper sets and the Scott-Hausdorff topology), then this Scott topology is equivalent to the initially given topology.
More concisely: For any preordered type 'α' with a topology, the Scott topology on 'α' is equal to that topology.
|
dirSupInacc_compl
theorem dirSupInacc_compl : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, DirSupInacc sᶜ ↔ DirSupClosed s := by
sorry
The theorem `dirSupInacc_compl` states that, for any set `s` of a type `α` with a preorder, the set `s` is inaccessible by directed joins if and only if the complement of set `s` is closed under directed joins. In other words, given a set `s` in a preordered type `α`, whenever the least upper bound of a directed set lies outside `s`, it implies that there is some element of the directed set also outside `s`. This is equivalently stated as: if every directed subset of `s` has its least upper bound in `s`, then `s` is closed under directed joins.
More concisely: A set in a preordered type is inaccessible by directed joins if and only if the complement is closed under directed joins.
|
Mathlib.Topology.Order.ScottTopology._auxLemma.1
theorem Mathlib.Topology.Order.ScottTopology._auxLemma.1 :
∀ {α : Type u} {s t : Set α}, (s ∩ t).Nonempty = ¬Disjoint s t
This theorem states that for any type `α` and any two sets `s` and `t` of type `α`, the property that the intersection of `s` and `t` is nonempty is equivalent to the negation of the property that `s` and `t` are disjoint. In other words, the intersection of `s` and `t` contains at least one element if and only if `s` and `t` are not disjoint. This generalizes the idea of disjoint sets in set theory, where two sets are considered disjoint if their intersection is empty.
More concisely: For any type `α` and sets `s` and `t` of type `α`, `s` and `t` have a non-empty intersection if and only if they are not disjoint.
|
DirSupClosed.compl
theorem DirSupClosed.compl : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, DirSupClosed s → DirSupInacc sᶜ := by
sorry
This theorem, named `DirSupClosed.compl`, states that for any type `α` with a preorder and any set `s` of that type, if `s` is closed under directed joins (meaning that if a directed set `d` has a least upper bound `a` and `d` is a subset of `s`, then `a` also belongs to `s`), then the complement of `s` (denoted by `sᶜ`) is inaccessible by directed joins (meaning that if the least upper bound of a directed set `d` lies in the complement of `s`, then `d` has a non-empty intersection with the complement of `s`). Essentially, the theorem asserts the reversal of the direction of `dirSupInacc_compl`.
More concisely: If a set `s` of a preordered type `α` is closed under directed joins, then the complement of `s` is inaccessible by directed joins.
|
DirSupInacc.compl
theorem DirSupInacc.compl : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, DirSupInacc s → DirSupClosed sᶜ := by
sorry
This theorem, known as the **alias of the reverse direction of `dirSupClosed_compl`**, states that for any type `α` equipped with a preorder and any set `s` of this type, if `s` is inaccessible by directed joins, then the complement of `s` is closed under directed joins. Here, a set is said to be inaccessible by directed joins if, given any directed set `d`, when `d` has a least upper bound that resides in `s`, then `d` will have a non-empty intersection with `s`. Similarly, a set is considered closed under directed joins if, whenever a directed set `d` has a least upper bound and is a subset of the set, the least upper bound also resides within the set.
More concisely: If a preorder set `s` is inaccessible by directed joins, then the complement of `s` is closed under directed joins.
|
Mathlib.Topology.Order.ScottTopology._auxLemma.3
theorem Mathlib.Topology.Order.ScottTopology._auxLemma.3 :
∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], Disjoint x yᶜ = (x ≤ y)
This theorem states that for any type `α` equipped with a Boolean algebra structure, and for any elements `x` and `y` of this type, `x` and the complement of `y` are disjoint if and only if `x` is less than or equal to `y`. Here, two elements are considered disjoint if their infimum (greatest lower bound) is the bottom element of the lattice. This is a generalization of the concept of disjoint sets in the subset lattice. Note that the complement of `y` is denoted by `yᶜ` and the bottom element of the lattice is denoted by `⊥`.
More concisely: For any type `α` with a Boolean algebra structure, elements `x` and `y` are disjoint (have infimum equal to the bottom element) if and only if `x ≤ y`.
|
DirSupClosed.of_compl
theorem DirSupClosed.of_compl : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, DirSupClosed sᶜ → DirSupInacc s := by
sorry
This theorem, named `DirSupClosed.of_compl`, states that for any set `s` of a certain type `α` with a preorder relation, if the complement of `s` is closed under directed suprema, then `s` is inaccessible by directed suprema. In other words, if every directed subset `d` whose least upper bound (or supremum) is in the complement of `s` has all of its elements in the complement of `s`, then for any directed subset `d` whose least upper bound is in `s`, `d` has a non-empty intersection with `s`.
More concisely: If the complement of a preordered set `s` is closed under directed suprema, then `s` is closed under directed infima. (This means that every directed subset of `s` has a least upper bound in `s`.)
|
Mathlib.Topology.Order.ScottTopology._auxLemma.2
theorem Mathlib.Topology.Order.ScottTopology._auxLemma.2 : ∀ {a b : Prop}, (¬a → ¬b) = (b → a)
This theorem states that for any two propositions `a` and `b`, the statement "not `a` implies not `b`" is equivalent to "if `b` then `a`". This is a fundamental theorem in logic, reflecting the principle of contraposition, which says that if a statement "if `p` then `q`" is true, then the statement "if not `q` then not `p`" is also true.
More concisely: The negation of proposition `a` implies the negation of proposition `b` is equivalent to `b` implying `a`.
|
Topology.IsScott.closure_singleton
theorem Topology.IsScott.closure_singleton :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [inst_2 : Topology.IsScott α] {a : α},
closure {a} = Set.Iic a
The theorem `Topology.IsScott.closure_singleton` states that for any type `α` that has a preorder and a Scott topology, and for any element `a` of this type, the closure of the singleton set `{a}` in the Scott topology is the right-closed left-infinite interval `(-∞, a]`. In other words, it is the set of all elements that are less than or equal to `a`. This is under the context of domain theory in computer science, where Scott topology plays a crucial role.
More concisely: In the context of a type `α` with a preorder and a Scott topology, the closure of the singleton set `{a}` is equal to the right-closed interval `[-\infty, a]`.
|