Relations: Euclidean Relations

This module proves basic properties about left and right Euclidean relations, which are use in modal logic.

TODO: develop an attribute to dualize theorems to the converse of a relation

References

• Simple Laws about Nonprominent Properties of Binary Relations

theorem Relation.refl_serial {α : Type u_1} (r : α → α → Prop) (h : Std.Refl r) : Serial r

instance Relation.instSerialOfRefl {α : Type u_1} {r : α → α → Prop} [instRefl : Std.Refl r] : Serial r

theorem Relation.RightEuclidean.refl_cod {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] {a b : α} (ab : r a b) : r b b

A RightEuclidean relation is reflexive on its range

theorem Relation.RightEuclidean.refl_cod' {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] {b : α} : b ∈ cod r → r b b

theorem Relation.RightEuclidean.leftEuclidean_swap {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] : LeftEuclidean fun (a b : α) => r b a

The converse of a RightEuclidean relation is LeftEuclidean

instance Relation.RightEuclidean.instSymmOfRefl {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] [Std.Refl r] : Std.Symm r

theorem Relation.RightEuclidean.trichotomous_trans {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] [Std.Trichotomous r] : IsTrans α r

theorem Relation.RightEuclidean.antisymm_rightUnique {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] [Std.Antisymm r] : Relator.RightUnique r

theorem Relation.RightEuclidean.rightUnique_antisymm {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] (h : Relator.RightUnique r) : Std.Antisymm r

theorem Relation.RightEuclidean.rightUnique_trans {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] (h : Relator.RightUnique r) : IsTrans α r

theorem Relation.RightEuclidean.rightTotal_equiv {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] (h : Relator.RightTotal r) : IsEquiv α r

theorem Relation.RightEuclidean.leftTotal_rightUnique_trans {α : Type u_1} {r : α → α → Prop} (h₁ : Relator.LeftTotal r) (h₂ : Relator.RightUnique r) [IsTrans α r] : RightEuclidean r

theorem Relation.RightEuclidean.trichotomous_antisymm_finite {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] [Std.Trichotomous r] [Std.Antisymm r] : Finite α

theorem Relation.RightEuclidean.trichotomous_antisymm_card {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] [Std.Trichotomous r] [Std.Antisymm r] [Fintype α] : Fintype.card α ≤ 2

theorem Relation.RightEuclidean.cod_subset_dom {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] : cod r ⊆ dom r

instance Relation.RightEuclidean.instElemCodValMemSet {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] : RightEuclidean fun (a b : ↑(cod r)) => r ↑a ↑b

instance Relation.RightEuclidean.instElemDomValMemSet {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] : RightEuclidean fun (a b : ↑(dom r)) => r ↑a ↑b

theorem Relation.RightEuclidean.rightTotal_cod {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] : Relator.RightTotal fun (a b : ↑(cod r)) => r ↑a ↑b

theorem Relation.RightEuclidean.equiv_cod {α : Type u_1} {r : α → α → Prop} [RightEuclidean r] : IsEquiv ↑(cod r) fun (a b : ↑(cod r)) => r ↑a ↑b

theorem Relation.LeftEuclidean.refl_dom {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] {a b : α} (ab : r a b) : r a a

A LeftEuclidean relation is reflexive on its domain

theorem Relation.LeftEuclidean.refl_dom' {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] {a : α} : a ∈ dom r → r a a

theorem Relation.LeftEuclidean.rightEuclidean_swap {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] : RightEuclidean fun (a b : α) => r b a

The converse of a LeftEuclidean relation is RightEuclidean

instance Relation.LeftEuclidean.instSymmOfRefl {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] [Std.Refl r] : Std.Symm r

theorem Relation.LeftEuclidean.trichotomous_trans {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] [Std.Trichotomous r] : IsTrans α r

theorem Relation.LeftEuclidean.antisymm_leftUnique {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] [Std.Antisymm r] : Relator.LeftUnique r

theorem Relation.LeftEuclidean.leftUnique_antisymm {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] (h : Relator.LeftUnique r) : Std.Antisymm r

theorem Relation.LeftEuclidean.leftUnique_trans {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] (h : Relator.LeftUnique r) : IsTrans α r

theorem Relation.LeftEuclidean.leftTotal_equiv {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] (h : Relator.LeftTotal r) : IsEquiv α r

theorem Relation.LeftEuclidean.rightTotal_leftUnique_trans {α : Type u_1} {r : α → α → Prop} (h₁ : Relator.RightTotal r) (h₂ : Relator.LeftUnique r) [IsTrans α r] : LeftEuclidean r

theorem Relation.LeftEuclidean.trichotomous_antisymm_finite {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] [Std.Trichotomous r] [Std.Antisymm r] : Finite α

theorem Relation.LeftEuclidean.trichotomous_antisymm_card {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] [Std.Trichotomous r] [Std.Antisymm r] [Fintype α] : Fintype.card α ≤ 2

theorem Relation.LeftEuclidean.dom_subset_cod {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] : dom r ⊆ cod r

instance Relation.LeftEuclidean.instElemCodValMemSet {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] : LeftEuclidean fun (a b : ↑(cod r)) => r ↑a ↑b

instance Relation.LeftEuclidean.instElemDomValMemSet {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] : LeftEuclidean fun (a b : ↑(dom r)) => r ↑a ↑b

theorem Relation.LeftEuclidean.leftTotal_dom {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] : Relator.LeftTotal fun (a b : ↑(dom r)) => r ↑a ↑b

theorem Relation.LeftEuclidean.equiv_dom {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] : IsEquiv ↑(dom r) fun (a b : ↑(dom r)) => r ↑a ↑b

theorem Relation.symm_leftEuclidean_iff_rightEuclidean {α : Type u_1} {r : α → α → Prop} [Std.Symm r] : LeftEuclidean r ↔ RightEuclidean r

For a symmetric relation, LeftEuclidean and RightEuclidean are equivalent.

theorem Relation.symm_leftEuclidean_iff_trans {α : Type u_1} {r : α → α → Prop} [Std.Symm r] : LeftEuclidean r ↔ IsTrans α r

For a symmetric relation, LeftEuclidean and transitivity are equivalent.

theorem Relation.symm_rightEuclidean_iff_trans {α : Type u_1} {r : α → α → Prop} [Std.Symm r] : RightEuclidean r ↔ IsTrans α r

For a symmetric relation, RightEuclidean and transitivity are equivalent.

theorem Relation.leftEuclidean_rightEuclidean_dom_cod_eq {α : Type u_1} {r : α → α → Prop} [LeftEuclidean r] [RightEuclidean r] : dom r = cod r

theorem Relation.dom_cod_leftEuclidean {α : Type u_1} {r : α → α → Prop} (eq : dom r = cod r) [equiv_dom : IsEquiv ↑(dom r) fun (a b : ↑(dom r)) => r ↑a ↑b] : LeftEuclidean r

theorem Relation.dom_cod_rightEuclidean {α : Type u_1} {r : α → α → Prop} (eq : dom r = cod r) [equiv_dom : IsEquiv ↑(dom r) fun (a b : ↑(dom r)) => r ↑a ↑b] : RightEuclidean r

theorem Relation.leftEuclidean_rightEuclidean_iff_dom_cod {α : Type u_1} {r : α → α → Prop} : LeftEuclidean r ∧ RightEuclidean r ↔ dom r = cod r ∧ IsEquiv ↑(dom r) fun (a b : ↑(dom r)) => r ↑a ↑b

A relation is both left and right Euclidean if and only if the relation is an equivalence on coinciding domain and codomain.