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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

• ConverseWellFounded rel = WellFounded (flip fun (x x_1 : α) => rel x x_1)

theorem serial_of_refl {α : Type u} {rel : α → α → Prop} (hRefl : Reflexive rel) : Serial rel

theorem eucl_of_symm_trans {α : Type u} {rel : α → α → Prop} (hSymm : Symmetric rel) (hTrans : Transitive rel) : Euclidean rel

theorem trans_of_symm_eucl {α : Type u} {rel : α → α → Prop} (hSymm : Symmetric rel) (hEucl : Euclidean rel) : Transitive rel

theorem symm_of_refl_eucl {α : Type u} {rel : α → α → Prop} (hRefl : Reflexive rel) (hEucl : Euclidean rel) : Symmetric rel

theorem trans_of_refl_eucl {α : Type u} {rel : α → α → Prop} (hRefl : Reflexive rel) (hEucl : Euclidean rel) : Transitive rel

theorem refl_of_symm_serial_eucl {α : Type u} {rel : α → α → Prop} (hSymm : Symmetric rel) (hSerial : Serial rel) (hEucl : Euclidean rel) : Reflexive 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] [IsIrrefl α rel] : ConverseWellFounded rel

theorem Finite.converseWellFounded_of_trans_irrefl' {α : Type u} {rel : α → α → Prop} (hFinite : Finite α) (hTrans : Transitive rel) (hIrrefl : Irreflexive rel) : ConverseWellFounded rel

theorem extensive_of_reflex_antisymm_eucl {α : Type u} {rel : α → α → Prop} (hRefl : Reflexive rel) (hAntisymm : Antisymmetric rel) (hEucl : Euclidean rel) : Extensive rel

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

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

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

@[simp]

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

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

Equations

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

@[reducible, inline]

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

Equations

• WeaklyConverseWellFounded R = ConverseWellFounded (Relation.IrreflGen R)

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

Alias of WeaklyConverseWellFounded.

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 → Antisymmetric R

theorem WCWF_of_finite_trans_antisymm {α : Type u} {R : α → α → Prop} (hFin : Finite α) (R_trans : Transitive R) : Antisymmetric R → WCWF R