Lists of involutions

This file provides an elementary invariance result for predicates transported along lists of involutions.

Main results

• TauCeti.predicate_foldl_iff_of_involutive: a predicate preserved by involutive steps is invariant along a list of steps.

theorem TauCeti.predicate_foldl_iff_of_involutive {I : Type u_1} {J : Type u_2} (p : I → Prop) (reflect : J → I → I) (hinvolutive : ∀ (j : J), Function.Involutive (reflect j)) (hreflect : ∀ (a : I) (j : J), p a → p (reflect j a)) (l : List J) (a : I) : p (List.foldl (fun (b : I) (j : J) => reflect j b) a l) ↔ p a

A predicate preserved by a family of involutions is invariant under every list of those involutions.