structure Geachean.Taple : Type

• i : ℕ
• j : ℕ
• m : ℕ
• n : ℕ

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

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 {α : Type u_1} {rel : Rel α α} : Reflexive rel ↔ Geachean { i := 0, j := 0, m := 1, n := 0 } rel

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

theorem Geachean.transitive_def {α : Type u_1} {rel : Rel α α} : Transitive 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 α α} : Dense rel ↔ Geachean { i := 0, j := 1, m := 2, n := 0 } rel

@[simp]

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

class IsGeachean (g : Geachean.Taple) (α : Type u_1) (R : Rel α α) : Prop

• geachean {x y z : α} : R.iterate g.i x y ∧ R.iterate g.j x z → ∃ (u : α), R.iterate g.m y u ∧ R.iterate g.n z u

instance instIsTransOfIsGeacheanMkOfNatNat {α : Type u_1} {R : Rel α α} [IsGeachean { i := 0, j := 2, m := 1, n := 0 } α R] : IsTrans α R

instance instIsGeacheanMkOfNatNatOfIsTrans {α : Type u_1} {R : Rel α α} [IsTrans α R] : IsGeachean { i := 0, j := 2, m := 1, n := 0 } α R

instance instIsReflOfIsGeacheanMkOfNatNat {α : Type u_1} {R : Rel α α} [IsGeachean { i := 0, j := 0, m := 1, n := 0 } α R] : IsRefl α R

instance instIsGeacheanMkOfNatNatOfIsRefl {α : Type u_1} {R : Rel α α} [IsRefl α R] : IsGeachean { i := 0, j := 0, m := 1, n := 0 } α R

instance instIsSymmOfIsGeacheanMkOfNatNat {α : Type u_1} {R : Rel α α} [IsGeachean { i := 0, j := 1, m := 0, n := 1 } α R] : IsSymm α R

instance instIsGeacheanMkOfNatNatOfIsSymm {α : Type u_1} {R : Rel α α} [IsSymm α R] : IsGeachean { i := 0, j := 1, m := 0, n := 1 } α R

instance instIsSerialOfIsGeacheanMkOfNatNat {α : Type u_1} {R : Rel α α} [IsGeachean { i := 0, j := 0, m := 1, n := 1 } α R] : IsSerial α R

instance instIsGeacheanMkOfNatNatOfIsSerial {α : Type u_1} {R : Rel α α} [IsSerial α R] : IsGeachean { i := 0, j := 0, m := 1, n := 1 } α R

instance instIsEuclideanOfIsGeacheanMkOfNatNat {α : Type u_1} {R : Rel α α} [IsGeachean { i := 1, j := 1, m := 0, n := 1 } α R] : IsEuclidean α R

instance instIsGeacheanMkOfNatNatOfIsEuclidean {α : Type u_1} {R : Rel α α} [IsEuclidean α R] : IsGeachean { i := 1, j := 1, m := 0, n := 1 } α R

instance instIsConfluentOfIsGeacheanMkOfNatNat {α : Type u_1} {R : Rel α α} [IsGeachean { i := 1, j := 1, m := 1, n := 1 } α R] : IsConfluent α R

instance instIsGeacheanMkOfNatNatOfIsConfluent {α : Type u_1} {R : Rel α α} [IsConfluent α R] : IsGeachean { i := 1, j := 1, m := 1, n := 1 } α R

instance instIsCoreflexiveOfIsGeacheanMkOfNatNat {α : Type u_1} {R : Rel α α} [IsGeachean { i := 0, j := 1, m := 0, n := 0 } α R] : IsCoreflexive α R

instance instIsGeacheanMkOfNatNatOfIsCoreflexive {α : Type u_1} {R : Rel α α} [IsCoreflexive α R] : IsGeachean { i := 0, j := 1, m := 0, n := 0 } α R

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

Equations

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