Relations: preservation of properties

@[simp]

theorem Relation.preserves_reflGen_iff {α✝ : Type u_1} {r : α✝ → α✝ → Prop} {P : α✝ → Prop} : Preserves (ReflGen r) P ↔ Preserves r P

A predicate preserved by a relation is also preserved by its reflexive closure.

@[simp]

theorem Relation.preserves_transGen_iff {α✝ : Sort u_1} {r : α✝ → α✝ → Prop} {P : α✝ → Prop} : Preserves (TransGen r) P ↔ Preserves r P

A predicate preserved by a relation is also preserved by its transitive closure.

@[simp]

theorem Relation.preserves_reflTransGen_iff {α✝ : Type u_1} {r : α✝ → α✝ → Prop} {P : α✝ → Prop} : Preserves (ReflTransGen r) P ↔ Preserves r P

A predicate is preserved by a relation iff it is preserves by its reflexive and transitive closure.