Equations
- Functional rel = ∀ ⦃x y z : α⦄, rel x y ∧ rel x z → y = z
Instances For
Equations
- Antisymmetric rel = ∀ ⦃x y : α⦄, rel x y → rel y x → x = y
Instances For
Equations
- Assymetric rel = ∀ ⦃x y : α⦄, rel x y → ¬rel y x
Instances For
@[reducible, inline]
Equations
- ConverseWellFounded rel = WellFounded (flip fun (x x_1 : α) => rel x x_1)
Instances For
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
trans_of_refl_eucl
{α : Type u}
{rel : α → α → Prop}
(hRefl : Reflexive rel)
(hEucl : Euclidean rel)
:
Transitive 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}
(hFinite : Finite α)
(hTrans : Transitive rel)
(hIrrefl : Irreflexive 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
@[simp]
Equations
- Relation.IrreflGen R x y = (x ≠ y ∧ R x y)
Instances For
@[reducible, inline]
Equations
Instances For
theorem
Finite.exists_ne_map_eq_of_infinite_lt
{α : Type u_1}
{β : Sort u_2}
[LinearOrder α]
[Infinite α]
[Finite β]
(f : α → β)
:
theorem
WCWF_of_finite_trans_antisymm
{α : Type u}
{R : α → α → Prop}
(hFin : Finite α)
(R_trans : Transitive R)
:
Antisymmetric R → WCWF R