Transporting reflexive–transitive closure along maps

Mathlib's Relation.ReflTransGen.lift carries paths forward along any map. The converse needs an injective map whose range contains every vertex reachable from the image of the source: then paths between images pull back to paths in the domain. Bijections satisfy this automatically.

Main results

• Relation.reflTransGen_onFun_iff: closure of a pulled-back relation along an injective map whose range contains every reachable vertex.
• Relation.reflTransGen_equiv_iff: closure is invariant under a bijection carrying one edge relation to the other.

theorem Relation.reflTransGen_onFun_iff {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) {r : β → β → Prop} {a b : α} (hrange : ∀ (y : β), ReflTransGen r (f a) y → ∃ (x : α), f x = y) : ReflTransGen (fun (x y : α) => r (f x) (f y)) a b ↔ ReflTransGen r (f a) (f b)

Closure of r pulled back along an injective map f is closure of r between images, provided every vertex reachable from f a lies in the range of f.

theorem Relation.reflTransGen_equiv_iff {α : Type u_1} {β : Type u_2} (e : α ≃ β) {r : α → α → Prop} {s : β → β → Prop} (h : ∀ (a b : α), r a b ↔ s (e a) (e b)) (a b : α) : ReflTransGen r a b ↔ ReflTransGen s (e a) (e b)

Reachability is invariant under a bijection that carries one edge relation to the other.