OneOneReducible.disjoin_right
theorem OneOneReducible.disjoin_right :
∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α → Prop} {q : β → Prop},
q ≤₁ Sum.elim p q
The theorem `OneOneReducible.disjoin_right` states that for any two types `α` and `β`, which are both primcodable, and any properties `p` on type `α` and `q` on type `β`, the property `q` is one-one reducible to the function `Sum.elim p q`. In other words, there is an injective function that maps elements of `β` satisfying `q` to the sum type `α ⊕ β` in such a way that `q` holds if and only if `Sum.elim p q` holds.
More concisely: For any primcodable types `α` and `β` and properties `p` on `α` and `q` on `β`, `q` is one-to-one reducible to the function `Sum.elim p q`, meaning there exists an injection from the set of elements satisfying `q` to the sum type `α ⊕ β` such that `q(x) <--> Sum.elim p q(fx)`, where `fx` is the image of `x` under the function associated with property `p`.
|
ManyOneEquiv.le_congr_left
theorem ManyOneEquiv.le_congr_left :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop}, ManyOneEquiv p q → (p ≤₀ r ↔ q ≤₀ r)
The theorem `ManyOneEquiv.le_congr_left` states that for any three types `α`, `β`, and `γ` that can be encoded as primitive recursive functions (i.e., they have `Primcodable` instance), and any properties `p` over `α`, `q` over `β`, and `r` over `γ`, if `p` and `q` are many-one equivalent (meaning each one of them can be many-one reduced to the other), then `p` is many-one reducible to `r` if and only if `q` is many-one reducible to `r`. In essence, if two properties are many-one equivalent, then any many-one reduction to another property can be substituted between them.
More concisely: If properties `p` over `α` and `q` over `β` are many-one equivalent, then they have the same many-one reducibility to property `r` over `γ`.
|
OneOneReducible.to_many_one
theorem OneOneReducible.to_many_one :
∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α → Prop} {q : β → Prop},
p ≤₁ q → p ≤₀ q
This theorem states that for any types `α` and `β` and predicates `p` and `q` on `α` and `β` respectively, if `p` is one-one reducible to `q` (denoted by `p ≤₁ q`), then `p` is many-one reducible to `q` (denoted by `p ≤₀ q`). Here, both `α` and `β` are required to be primcodable, which means there exists an effective procedure to encode and decode values of these types. One-one reducibility and many-one reducibility are concepts from the theory of computability, which deal with the transformations between different decision problems or sets.
More concisely: If `α` and `β` are primcodable types and `p` is one-one reducible to `q` (`p ≤₁ q`), then `p` is many-one reducible to `q` (`p ≤₀ q`).
|
ManyOneEquiv.le_congr_right
theorem ManyOneEquiv.le_congr_right :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop}, ManyOneEquiv q r → (p ≤₀ q ↔ p ≤₀ r)
The theorem `ManyOneEquiv.le_congr_right` states that for all types `α`, `β`, and `γ`, which have the `Primcodable` property, and for all propositions `p` that maps from type `α` to `Prop`, `q` from `β` to `Prop`, and `r` from `γ` to `Prop`, if `q` and `r` are many-one equivalent (meaning that each one is many-one reducible to the other), then `p` is many-one reducible to `q` if and only if `p` is many-one reducible to `r`. In simple terms, if `q` and `r` are interchangeable via many-one reduction, then `p`'s reducibility to `q` is equivalent to its reducibility to `r`.
More concisely: For types `α`, `β`, `γ` with `Primcodable` property and propositions `p : α → Prop`, `q : β → Prop`, `r : γ → Prop`, if `q` and `r` are many-one equivalent, then `p` is many-one reducible to `q` if and only if it is many-one reducible to `r`.
|
OneOneReducible.trans
theorem OneOneReducible.trans :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop}, p ≤₁ q → q ≤₁ r → p ≤₁ r
The theorem `OneOneReducible.trans` states that for any three types `α`, `β`, and `γ` that are Primcodable, and any three properties `p` of `α`, `q` of `β`, and `r` of `γ`, if `p` is one-one reducible to `q`, and `q` is one-one reducible to `r`, then `p` is one-one reducible to `r`. Here, "one-one reducible" means there exists some function that maps every instance of the first property to a unique instance of the second, preserving the structure in the process. This theorem is essentially a transitivity property for one-one reducibility between properties on different types.
More concisely: If `p` is one-one reducible to `q` and `q` is one-one reducible to `r`, then `p` is one-one reducible to `r`. (One-one reducibility is a transitive relation between properties on different types.)
|
ManyOneDegree.add_le
theorem ManyOneDegree.add_le : ∀ {d₁ d₂ d₃ : ManyOneDegree}, d₁ + d₂ ≤ d₃ ↔ d₁ ≤ d₃ ∧ d₂ ≤ d₃
This theorem states that for any three many-one degrees `d₁`, `d₂`, and `d₃`, the many-one degree of the sum `d₁ + d₂` is less than or equal to `d₃` if and only if both `d₁` and `d₂` are individually less than or equal to `d₃`. Here, the sum and inequalities are in the context of many-one degrees, which are equivalence classes of sets connected by a many-one equivalence relation.
More concisely: For any many-one degrees d₁, d₂, and d₃, d₁ + d₂ ≤ d₃ if and only if d₁ ≤ d₃ and d₂ ≤ d₃. (In the context of many-one degrees, "+", and "<=" denote the sum and inequality relations, respectively.)
|
disjoin_manyOneReducible
theorem disjoin_manyOneReducible :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop}, p ≤₀ r → q ≤₀ r → Sum.elim p q ≤₀ r
The theorem `disjoin_manyOneReducible` states that for any types `α`, `β`, and `γ` where `α`, `β`, and `γ` are primcodable, and any predicates `p` on `α`, `q` on `β`, and `r` on `γ`, if `p` is many-one reducible to `r` and `q` is many-one reducible to `r`, then the function `Sum.elim p q`, which defines a function on the disjoint union of `α` and `β` (i.e., `α ⊕ β`) by giving separate definitions on `α` and `β`, is also many-one reducible to `r`. Here, "many-one reducible" is denoted by `≤₀`.
More concisely: If `p` is many-one reducible to `r` and `q` is many-one reducible to `r`, then the function `Sum.elim p q` on the disjoint union of `α` and `β` is many-one reducible to `r`.
|
ManyOneReducible.trans
theorem ManyOneReducible.trans :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable γ] {p : α → Prop} {q : β → Prop} {r : γ → Prop}, p ≤₀ q → q ≤₀ r → p ≤₀ r
This theorem, `ManyOneReducible.trans`, states that for any three types α, β, and γ, each of which has a `Primcodable` instance, and for any three propositions `p : α → Prop`, `q : β → Prop`, and `r : γ → Prop`, if `p` is many-one reducible to `q` (`p ≤₀ q`), and `q` is many-one reducible to `r` (`q ≤₀ r`), then `p` is many-one reducible to `r` (`p ≤₀ r`). This is the transitivity property for the many-one reducibility relation in the context of computability theory.
More concisely: If `α`, `β`, and `γ` have `Primcodable` instances, and `p ≤₀ q` and `q ≤₀ r` are many-one reducibilities between propositions, then `p ≤₀ r`.
|
manyOneEquiv_refl
theorem manyOneEquiv_refl : ∀ {α : Type u_1} [inst : Primcodable α] (p : α → Prop), ManyOneEquiv p p
The theorem `manyOneEquiv_refl` states that for any type `α` that is primcodable and any property `p` of `α`, `p` is many-one equivalent to itself. In other words, a property `p` is many-one reducible to itself and vice versa. This is a reflection property in the context of many-one equivalence, indicating that any property is many-one equivalent to itself.
More concisely: For any primcodable type `α` and property `p` of `α`, the property `p` is many-one equivalent to itself.
|
OneOneReducible.disjoin_left
theorem OneOneReducible.disjoin_left :
∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : α → Prop} {q : β → Prop},
p ≤₁ Sum.elim p q
The theorem `OneOneReducible.disjoin_left` states that for any types `α` and `β` that have instances of `Primcodable` (i.e., they can be encoded as natural numbers), and for any properties `p` of type `α` and `q` of type `β`, the property `p` is one-one reducible to the function `Sum.elim p q`, which is defined on the sum type of `α` and `β`. The function `Sum.elim p q` applies the property `p` to elements of `α` and the property `q` to elements of `β`. Here, `≤₁` denotes one-one reducibility, meaning that there is an injective (one-to-one) function that transforms instances of `p` into instances of `Sum.elim p q`.
More concisely: For types `α` and `β` with `Primcodable` instances, and properties `p` of type `α` and `q` of type `β`, `p` is one-one reducible to the function `Sum.elim p q` that applies `p` to elements of `α` and `q` to elements of `β`.
|