Documentation

Foundation.FirstOrder.Arith.Representation

theorem Part.unit_dom_iff (x : Part Unit) :
x.Dom () x
theorem Mathlib.Vector.cons_get {α : Type u_1} {k : } (a : α) (v : Mathlib.Vector α k) :
(a ::ᵥ v).get = a :> v.get
theorem Nat.Partrec.projection {f : →. } (hf : Nat.Partrec f) (unif : ∀ {m n₁ n₂ a₁ a₂ : }, a₁ f (Nat.pair m n₁)a₂ f (Nat.pair m n₂)a₁ = a₂) :
∃ (g : →. ), Nat.Partrec g ∀ (a m : ), a g m ∃ (z : ), a f (Nat.pair m z)
theorem Partrec.projection {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {f : αβ →. γ} (hf : Partrec₂ f) (unif : ∀ {a : α} {b₁ b₂ : β} {c₁ c₂ : γ}, c₁ f a b₁c₂ f a b₂c₁ = c₂) :
∃ (g : α →. γ), Partrec g ∀ (c : γ) (a : α), c g a ∃ (b : β), c f a b
@[simp]
theorem RePred.const {α : Type u_1} [Primcodable α] (p : Prop) :
RePred fun (x : α) => p
theorem RePred.iff {α : Type u_1} [Primcodable α] {p : αProp} :
RePred p ∃ (f : α →. Unit), Partrec f p = fun (x : α) => (f x).Dom
theorem RePred.iff' {α : Type u_1} [Primcodable α] {p : αProp} :
RePred p ∃ (f : α →. Unit), Partrec f ∀ (x : α), p x (f x).Dom
theorem RePred.and {α : Type u_1} [Primcodable α] {p : αProp} {q : αProp} (hp : RePred p) (hq : RePred q) :
RePred fun (x : α) => p x q x
theorem RePred.or {α : Type u_1} [Primcodable α] {p : αProp} {q : αProp} (hp : RePred p) (hq : RePred q) :
RePred fun (x : α) => p x q x
theorem RePred.projection {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : α × βProp} (hp : RePred p) :
RePred fun (x : α) => ∃ (y : β), p (x, y)
theorem RePred.comp {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : αβ} (hf : Computable f) {p : βProp} (hp : RePred p) :
RePred fun (x : α) => p (f x)
@[simp]
theorem LO.FirstOrder.Arith.natCast_nat (n : ) :
n = n
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For