Totality of a reflexive transitive closure as the absence of a closed proper subset

Read r : α → α → Prop as the edge relation of a directed graph. Saying that Relation.ReflTransGen r relates every pair of points is the "any two points are joined by a chain" form of connectedness; saying that every nonempty proper subset of α has an edge leaving it is the "no disconnecting cut" form. Relation.forall_reflTransGen_iff is the translation between the two, for an arbitrary relation on an arbitrary type.

Main results

• Relation.forall_reflTransGen_iff: totality of Relation.ReflTransGen r is exactly the absence of a nonempty proper subset with no outgoing edge.

theorem Relation.forall_reflTransGen_iff {α : Type u_1} (r : α → α → Prop) : (∀ (i j : α), ReflTransGen r i j) ↔ ∀ (s : Set α), s.Nonempty → s ≠ Set.univ → ∃ (i : α), i ∈ s ∧ ∃ (j : α), ¬j ∈ s ∧ r i j

Totality of a reflexive transitive closure is the absence of a disconnecting cut. Every pair of points is joined by an r-chain exactly when every nonempty proper subset s carries an edge from a point of s to a point outside s.