@[reducible, inline]

abbrev WeaklyConverseWellFounded {α : Type u_1} (rel : Rel α α) : Prop

Equations

• WeaklyConverseWellFounded rel = ConverseWellFounded rel.IrreflGen

class IsWeaklyConverseWellFounded (α : Type u_1) (rel : Rel α α) : Prop

• wcwf : WeaklyConverseWellFounded rel

theorem isWeaklyConverseWellFounded_iff (α : Type u_1) (rel : Rel α α) : IsWeaklyConverseWellFounded α rel ↔ WeaklyConverseWellFounded rel

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

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

theorem antisymm_of_weaklyConverseWellFounded {α : Type u_1} {rel : α → α → Prop} : WeaklyConverseWellFounded rel → AntiSymmetric rel

instance instIsAntisymmOfIsWeaklyConverseWellFounded {α : Type u_1} {rel : α → α → Prop} [IsWeaklyConverseWellFounded α rel] : IsAntisymm α rel

theorem weaklyConverseWellFounded_of_finite_trans_antisymm {α : Type u_1} {rel : α → α → Prop} (hFin : Finite α) (R_trans : Transitive rel) : AntiSymmetric rel → WeaklyConverseWellFounded rel

instance instIsWeaklyConverseWellFoundedOfFiniteOfIsTransOfIsAntisymm {α : Type u_1} {rel : α → α → Prop} [Finite α] [IsTrans α rel] [IsAntisymm α rel] : IsWeaklyConverseWellFounded α rel