Theory Pointwise

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