Equations
- GeachConfluent 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
Instances For
theorem
GeachConfluent.serial_def
{α : Type u_1}
{R : Rel α α}
:
Serial R ↔ GeachConfluent { i := 0, j := 0, m := 1, n := 1 } R
theorem
GeachConfluent.reflexive_def
{α : Type u_1}
{R : Rel α α}
:
Reflexive R ↔ GeachConfluent { i := 0, j := 0, m := 1, n := 0 } R
theorem
GeachConfluent.symmetric_def
{α : Type u_1}
{R : Rel α α}
:
Symmetric R ↔ GeachConfluent { i := 0, j := 1, m := 0, n := 1 } R
theorem
GeachConfluent.transitive_def
{α : Type u_1}
{R : Rel α α}
:
Transitive R ↔ GeachConfluent { i := 0, j := 2, m := 1, n := 0 } R
theorem
GeachConfluent.euclidean_def
{α : Type u_1}
{R : Rel α α}
:
Euclidean R ↔ GeachConfluent { i := 1, j := 1, m := 0, n := 1 } R
theorem
GeachConfluent.confluent_def
{α : Type u_1}
{R : Rel α α}
:
Confluent R ↔ GeachConfluent { i := 1, j := 1, m := 1, n := 1 } R
theorem
GeachConfluent.extensive_def
{α : Type u_1}
{R : Rel α α}
:
Extensive R ↔ GeachConfluent { i := 0, j := 1, m := 0, n := 0 } R
theorem
GeachConfluent.functional_def
{α : Type u_1}
{R : Rel α α}
:
Functional R ↔ GeachConfluent { i := 1, j := 1, m := 0, n := 0 } R
theorem
GeachConfluent.dense_def
{α : Type u_1}
{R : Rel α α}
:
Dense R ↔ GeachConfluent { i := 0, j := 1, m := 2, n := 0 } R
@[simp]
theorem
GeachConfluent.satisfies_eq
{α : Type u_1}
{t : GeachTaple}
:
GeachConfluent t fun (x x_1 : α) => x = x_1
Equations
- MultiGeachConfluent [] R = True
- MultiGeachConfluent [t] R = GeachConfluent t R
- MultiGeachConfluent (t :: ts_2) R = (GeachConfluent t R ∧ MultiGeachConfluent ts_2 R)
Instances For
@[simp]
@[simp]
theorem
MultiGeachConfluent.iff_singleton
{t : GeachTaple}
:
∀ {α : Type u_1} {R : Rel α α}, MultiGeachConfluent [t] R ↔ GeachConfluent t R
theorem
MultiGeachConfluent.iff_cons
{ts : List GeachTaple}
{t : GeachTaple}
:
∀ {α : Type u_1} {R : Rel α α},
ts ≠ [] → (MultiGeachConfluent (t :: ts) R ↔ GeachConfluent t R ∧ MultiGeachConfluent ts R)
@[simp]
theorem
MultiGeachConfluent.satisfies_eq
{α : Type u_1}
{ts : List GeachTaple}
:
MultiGeachConfluent ts fun (x x_1 : α) => x = x_1
@[reducible, inline]
abbrev
LO.Axioms.Geach
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
(t : GeachTaple)
(p : F)
:
F
Instances For
@[reducible, inline]
abbrev
LO.Axioms.Geach.set
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
(t : GeachTaple)
:
Set F
Equations
- 𝗴𝗲(t) = {x : F | ∃ (p : F), LO.Axioms.Geach t p = x}
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Axioms.Geach.T_def
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
theorem
LO.Axioms.Geach.B_def
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
theorem
LO.Axioms.Geach.D_def
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
theorem
LO.Axioms.Geach.Four_def
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
theorem
LO.Axioms.Geach.Five_def
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
theorem
LO.Axioms.Geach.Dot2_def
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
theorem
LO.Axioms.Geach.C4_def
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
theorem
LO.Axioms.Geach.CD_def
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
theorem
LO.Axioms.Geach.Tc_def
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
class
LO.Axioms.IsGeach
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
(Ax : Set F)
:
- taple : GeachTaple
- char : Ax = 𝗴𝗲(LO.Axioms.IsGeach.taple Ax)
Instances
theorem
LO.Axioms.IsGeach.char
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
{Ax : Set F}
[self : LO.Axioms.IsGeach Ax]
:
Ax = 𝗴𝗲(LO.Axioms.IsGeach.taple Ax)
instance
LO.Axioms.instIsGeachSet
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
Equations
- LO.Axioms.instIsGeachSet = { taple := { i := 0, j := 0, m := 1, n := 0 }, char := ⋯ }
instance
LO.Axioms.instIsGeachSet_1
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
Equations
- LO.Axioms.instIsGeachSet_1 = { taple := { i := 0, j := 1, m := 0, n := 1 }, char := ⋯ }
instance
LO.Axioms.instIsGeachSet_2
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
Equations
- LO.Axioms.instIsGeachSet_2 = { taple := { i := 0, j := 0, m := 1, n := 1 }, char := ⋯ }
instance
LO.Axioms.instIsGeachSet_3
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
Equations
- LO.Axioms.instIsGeachSet_3 = { taple := { i := 0, j := 2, m := 1, n := 0 }, char := ⋯ }
instance
LO.Axioms.instIsGeachSet_4
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
Equations
- LO.Axioms.instIsGeachSet_4 = { taple := { i := 1, j := 1, m := 0, n := 1 }, char := ⋯ }
instance
LO.Axioms.instIsGeachSet_5
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
Equations
- LO.Axioms.instIsGeachSet_5 = { taple := { i := 1, j := 1, m := 1, n := 1 }, char := ⋯ }
instance
LO.Axioms.instIsGeachSet_6
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
Equations
- LO.Axioms.instIsGeachSet_6 = { taple := { i := 0, j := 1, m := 2, n := 0 }, char := ⋯ }
instance
LO.Axioms.instIsGeachSet_7
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
Equations
- LO.Axioms.instIsGeachSet_7 = { taple := { i := 1, j := 1, m := 0, n := 0 }, char := ⋯ }
instance
LO.Axioms.instIsGeachSet_8
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
Equations
- LO.Axioms.instIsGeachSet_8 = { taple := { i := 0, j := 1, m := 0, n := 0 }, char := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.Axioms.MultiGeach.def_nil
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
:
@[simp]
theorem
LO.Axioms.MultiGeach.iff_cons
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
{x : GeachTaple}
{l : List GeachTaple}
:
theorem
LO.Axioms.MultiGeach.mem
{F : Type u_1}
[LO.LogicalConnective F]
[LO.BasicModalLogicalConnective F]
{x : GeachTaple}
{l : List GeachTaple}
(h : x ∈ l)
:
@[reducible, inline]
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances
@[simp]
theorem
LO.Modal.Hilbert.IsGeach.char
{α : Type u_1}
{L : LO.Modal.Hilbert α}
{ts : List GeachTaple}
[self : L.IsGeach ts]
:
theorem
LO.Modal.IsGeach.ax
{α : Type u_1}
{ts : List GeachTaple}
{Λ : LO.Modal.Hilbert α}
[geach : Λ.IsGeach ts]
:
Equations
- LO.Modal.IsGeach.instIsGeachKNilGeachTaple = { char := ⋯ }
instance
LO.Modal.IsGeach.instIsGeachKDConsGeachTapleMkOfNatNatNil
{α : Type u_1}
:
𝐊𝐃.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }]
Equations
- LO.Modal.IsGeach.instIsGeachKDConsGeachTapleMkOfNatNatNil = { char := ⋯ }
instance
LO.Modal.IsGeach.instIsGeachKTConsGeachTapleMkOfNatNatNil
{α : Type u_1}
:
𝐊𝐓.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }]
Equations
- LO.Modal.IsGeach.instIsGeachKTConsGeachTapleMkOfNatNatNil = { char := ⋯ }
instance
LO.Modal.IsGeach.instIsGeachKTBConsGeachTapleMkOfNatNatNil
{α : Type u_1}
:
𝐊𝐓𝐁.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }]
Equations
- LO.Modal.IsGeach.instIsGeachKTBConsGeachTapleMkOfNatNatNil = { char := ⋯ }
instance
LO.Modal.IsGeach.instIsGeachK4ConsGeachTapleMkOfNatNatNil
{α : Type u_1}
:
𝐊𝟒.IsGeach [{ i := 0, j := 2, m := 1, n := 0 }]
Equations
- LO.Modal.IsGeach.instIsGeachK4ConsGeachTapleMkOfNatNatNil = { char := ⋯ }
instance
LO.Modal.IsGeach.instIsGeachS4ConsGeachTapleMkOfNatNatNil
{α : Type u_1}
:
𝐒𝟒.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }]
Equations
- LO.Modal.IsGeach.instIsGeachS4ConsGeachTapleMkOfNatNatNil = { char := ⋯ }
instance
LO.Modal.IsGeach.instIsGeachS4Dot2ConsGeachTapleMkOfNatNatNil
{α : Type u_1}
:
𝐒𝟒.𝟐.IsGeach
[{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 1, j := 1, m := 1, n := 1 }]
Equations
- LO.Modal.IsGeach.instIsGeachS4Dot2ConsGeachTapleMkOfNatNatNil = { char := ⋯ }
instance
LO.Modal.IsGeach.instIsGeachS5ConsGeachTapleMkOfNatNatNil
{α : Type u_1}
:
𝐒𝟓.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }]
Equations
- LO.Modal.IsGeach.instIsGeachS5ConsGeachTapleMkOfNatNatNil = { char := ⋯ }
instance
LO.Modal.IsGeach.instIsGeachKT4BConsGeachTapleMkOfNatNatNil
{α : Type u_1}
:
𝐊𝐓𝟒𝐁.IsGeach
[{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }]
Equations
- LO.Modal.IsGeach.instIsGeachKT4BConsGeachTapleMkOfNatNatNil = { char := ⋯ }
instance
LO.Modal.IsGeach.instIsGeachTrivConsGeachTapleMkOfNatNatNil
{α : Type u_1}
:
𝐓𝐫𝐢𝐯.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 0 }]
Equations
- LO.Modal.IsGeach.instIsGeachTrivConsGeachTapleMkOfNatNatNil = { char := ⋯ }