theory Pointwise imports Main begin text {* Lifting a relation to a function. *} definition pointwise where "pointwise P m m' = (∀ x. P (m x) (m' x))" lemma pointwiseI[intro]: "(⋀ x. P (m x) (m' x)) ⟹ pointwise P m m'" unfolding pointwise_def by blast end