Relations: Properties on set restrictions

References

• Simple Laws about Nonprominent Properties of Binary Relations

@[simp]

theorem Set.refl_iff_reflOn {α : Type u_1} (r : α → α → Prop) (s : Set α) : (Std.Refl fun (a b : ↑s) => r ↑a ↑b) ↔ s.ReflOn r

@[simp]

theorem Set.symm_iff_symmOn {α : Type u_1} (r : α → α → Prop) (s : Set α) : (Std.Symm fun (a b : ↑s) => r ↑a ↑b) ↔ s.SymmOn r

theorem Set.ReflOn.of_dom {α✝ : Type u_1} {a b : α✝} {r : α✝ → α✝ → Prop} : (Relation.dom r).ReflOn r → r a b → r a a

theorem Set.ReflOn.of_cod {α✝ : Type u_1} {a b : α✝} {r : α✝ → α✝ → Prop} : (Relation.cod r).ReflOn r → r a b → r b b

theorem Set.SymmOn.of_dom {α✝ : Type u_1} {a b c : α✝} {r : α✝ → α✝ → Prop} : (Relation.dom r).SymmOn r → r a b → r b c → r b a

theorem Set.SymmOn.of_cod {α✝ : Type u_1} {a b c : α✝} {r : α✝ → α✝ → Prop} : (Relation.cod r).SymmOn r → r a b → r c a → r b a