BinaryRelations

def IsSymmetric {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• IsSymmetric rel = ∀ ⦃x y : α⦄, rel x y → rel y x

def Euclidean {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• Euclidean rel = ∀ ⦃x y z : α⦄, rel x y → rel x z → rel z y

def Serial {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• Serial rel = ∀ (x : α), ∃ (y : α), rel x y

def Confluent {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• Confluent rel = ∀ ⦃x y z : α⦄, rel x y ∧ rel x z → ∃ (w : α), rel y w ∧ rel z w

def RelDense {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• RelDense rel = ∀ ⦃x y : α⦄, rel x y → ∃ (z : α), rel x z ∧ rel z y

def Connected {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• Connected rel = ∀ ⦃x y z : α⦄, rel x y ∧ rel x z → rel y z ∨ rel z y

def Functional {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• Functional rel = ∀ ⦃x y z : α⦄, rel x y ∧ rel x z → y = z

def RightConvergent {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• RightConvergent rel = ∀ ⦃x y z : α⦄, rel x y ∧ rel x z → rel y z ∨ rel z y ∨ y = z

def Coreflexive {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• Coreflexive rel = ∀ ⦃x y : α⦄, rel x y → x = y

def Equality {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• Equality rel = ∀ ⦃x y : α⦄, rel x y ↔ x = y

def Isolated {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• Isolated rel = ∀ ⦃x y : α⦄, ¬rel x y

def Assymetric {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• Assymetric rel = ∀ ⦃x y : α⦄, rel x y → ¬rel y x

def Universal {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• Universal rel = ∀ ⦃x y : α⦄, rel x y

@[reducible, inline]

abbrev ConverseWellFounded {α : Type u} (rel : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• ConverseWellFounded rel = WellFounded (flip fun (x1 x2 : α) => rel x1 x2)

theorem serial_of_refl {α : Type u} {rel : α → α → Prop} (hRefl : ∀ (x : α), rel x x) : Serial rel

theorem eucl_of_symm_trans {α : Type u} {rel : α → α → Prop} (hSymm : IsSymmetric rel) (hTrans : ∀ ⦃x y z : α⦄, rel x y → rel y z → rel x z) : Euclidean rel

theorem trans_of_symm_eucl {α : Type u} {rel : α → α → Prop} (hSymm : IsSymmetric rel) (hEucl : Euclidean rel) ⦃x y z : α⦄ : rel x y → rel y z → rel x z

theorem symm_of_refl_eucl {α : Type u} {rel : α → α → Prop} (hRefl : ∀ (x : α), rel x x) (hEucl : Euclidean rel) : IsSymmetric rel

theorem trans_of_refl_eucl {α : Type u} {rel : α → α → Prop} (hRefl : ∀ (x : α), rel x x) (hEucl : Euclidean rel) ⦃x y z : α⦄ : rel x y → rel y z → rel x z

theorem refl_of_symm_serial_eucl {α : Type u} {rel : α → α → Prop} (hSymm : IsSymmetric rel) (hSerial : Serial rel) (hEucl : Euclidean rel) (x : α) : rel x x

theorem corefl_of_refl_assym_eucl {α : Type u} {rel : α → α → Prop} (hRefl : ∀ (x : α), rel x x) (hAntisymm : ∀ ⦃x y : α⦄, rel x y → rel y x → x = y) (hEucl : Euclidean rel) : Coreflexive rel

theorem equality_of_refl_corefl {α : Type u} {rel : α → α → Prop} (hRefl : ∀ (x : α), rel x x) (hCorefl : Coreflexive rel) : Equality rel

theorem equality_of_refl_assym_eucl {α : Type u} {rel : α → α → Prop} (hRefl : ∀ (x : α), rel x x) (hAntisymm : ∀ ⦃x y : α⦄, rel x y → rel y x → x = y) (hEucl : Euclidean rel) : Equality rel

theorem refl_of_equality {α : Type u} {rel : α → α → Prop} (h : Equality rel) (x : α) : rel x x

theorem corefl_of_equality {α : Type u} {rel : α → α → Prop} (h : Equality rel) : Coreflexive rel

theorem irreflexive_of_assymetric {α : Type u} {rel : α → α → Prop} (hAssym : Assymetric rel) (x : α) : ¬rel x x

theorem refl_of_universal {α : Type u} {rel : α → α → Prop} (h : Universal rel) (x : α) : rel x x

theorem eucl_of_universal {α : Type u} {rel : α → α → Prop} (h : Universal rel) : Euclidean rel

theorem confluent_of_refl_connected {α : Type u} {rel : α → α → Prop} (hRefl : ∀ (x : α), rel x x) (hConfl : Connected rel) : Confluent rel

theorem ConverseWellFounded.iff_has_max {α : Type u} {r : α → α → Prop} : ConverseWellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r m x

theorem Finite.converseWellFounded_of_trans_irrefl {α : Type u} {rel : α → α → Prop} [Finite α] [IsTrans α rel] [Std.Irrefl rel] : ConverseWellFounded rel

theorem Finite.converseWellFounded_of_trans_irrefl' {α : Type u} {rel : α → α → Prop} (hFinite : Finite α) (hTrans : ∀ ⦃x y z : α⦄, rel x y → rel y z → rel x z) (hIrrefl : ∀ (x : α), ¬rel x x) : ConverseWellFounded rel

@[simp]

theorem WellFounded.trivial_wellfounded {α : Type u} : WellFounded fun (x x_1 : α) => False

def Relation.IrreflGen {α : Type u} (R : α → α → Prop) (x y : α) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• Relation.IrreflGen R x y = (x ≠ y ∧ R x y)

@[reducible, inline]

abbrev WeaklyConverseWellFounded {α : Type u} (R : α → α → Prop) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• WeaklyConverseWellFounded R = ConverseWellFounded (Relation.IrreflGen R)

def WCWF {α : Type u} (R : α → α → Prop) : Prop

Alias of WeaklyConverseWellFounded.

---

Imported declaration from the Incompleteness formalization.

Equations

• @WCWF = @WeaklyConverseWellFounded

theorem dependent_choice {α : Type u} {R : α → α → Prop} (h : ∃ (s : Set α), s.Nonempty ∧ ∀ a ∈ s, ∃ b ∈ s, R a b) : ∃ (f : ℕ → α), ∀ (x : ℕ), R (f x) (f (x + 1))

theorem Finite.exists_ne_map_eq_of_infinite_lt {α : Type u_1} {β : Sort u_2} [LinearOrder α] [Infinite α] [Finite β] (f : α → β) : ∃ (x : α) (y : α), x < y ∧ f x = f y

theorem antisymm_of_WCWF {α : Type u} {R : α → α → Prop} : WCWF R → ∀ ⦃x y : α⦄, R x y → R y x → x = y

theorem WCWF_of_finite_trans_antisymm {α : Type u} {R : α → α → Prop} (hFin : Finite α) (R_trans : ∀ ⦃x y z : α⦄, R x y → R y z → R x z) : (∀ ⦃x y : α⦄, R x y → R y x → x = y) → WCWF R