section ‹Basic lemmas about functions› theory FunctionLemmas imports Main "HOL-Library.FuncSet" begin text ‹These are used in simplification. Note that the difference from Pi-mem is that the statement about the function comes first, so Isabelle can more easily figure out what $S$ is.› lemma PiE_mem2: "f ∈ S→⇩E T ⟹ x ∈ S ⟹ f x ∈ T" unfolding PiE_def by auto lemma Pi_mem2: "f ∈ S→ T ⟹ x ∈ S ⟹ f x ∈ T" unfolding Pi_def by auto end