Geachean

structure Geachean.Taple : Type

Imported declaration from the Incompleteness formalization.

• i : ℕ

  Imported declaration from the Incompleteness formalization.

• j : ℕ

  Imported declaration from the Incompleteness formalization.

• m : ℕ

  Imported declaration from the Incompleteness formalization.

• n : ℕ

  Imported declaration from the Incompleteness formalization.

def Geachean {α : Sort u_1} (t : Geachean.Taple) (R : Rel α α) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• Geachean t R = ∀ {x y z : α}, R.iterate t.i x y ∧ R.iterate t.j x z → ∃ (u : α), R.iterate t.m y u ∧ R.iterate t.n z u

theorem Geachean.serial_def {α : Type u_1} {rel : Rel α α} : Serial rel ↔ Geachean { i := 0, j := 0, m := 1, n := 1 } rel

theorem Geachean.reflexive_def {α : Sort u_1} {rel : Rel α α} : Std.Refl rel ↔ Geachean { i := 0, j := 0, m := 1, n := 0 } rel

theorem Geachean.symmetric_def {α : Type u_1} {rel : Rel α α} : IsSymmetric rel ↔ Geachean { i := 0, j := 1, m := 0, n := 1 } rel

theorem Geachean.transitive_def {α : Sort u_1} {rel : Rel α α} : IsTrans α rel ↔ Geachean { i := 0, j := 2, m := 1, n := 0 } rel

theorem Geachean.euclidean_def {α : Type u_1} {rel : Rel α α} : Euclidean rel ↔ Geachean { i := 1, j := 1, m := 0, n := 1 } rel

theorem Geachean.confluent_def {α : Type u_1} {rel : Rel α α} : Confluent rel ↔ Geachean { i := 1, j := 1, m := 1, n := 1 } rel

theorem Geachean.coreflexive_def {α : Type u_1} {rel : Rel α α} : Coreflexive rel ↔ Geachean { i := 0, j := 1, m := 0, n := 0 } rel

theorem Geachean.functional_def {α : Type u_1} {rel : Rel α α} : Functional rel ↔ Geachean { i := 1, j := 1, m := 0, n := 0 } rel

theorem Geachean.dense_def {α : Type u_1} {rel : Rel α α} : RelDense rel ↔ Geachean { i := 0, j := 1, m := 2, n := 0 } rel

@[simp]

theorem Geachean.satisfies_eq {α : Sort u_1} {t : Taple} : Geachean t fun (x1 x2 : α) => x1 = x2

def MultiGeachean {α : Sort u_1} (G : Set Geachean.Taple) (R : Rel α α) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• MultiGeachean G R = ∀ g ∈ G, Geachean g R