[STATEMENT]
lemma going_to_mono: "F \<le> G \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f going_to F within A \<le> f going_to G within B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<le> G; A \<subseteq> B\<rbrakk> \<Longrightarrow> f going_to F within A \<le> f going_to G within B
[PROOF STEP]
unfolding going_to_within_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<le> G; A \<subseteq> B\<rbrakk> \<Longrightarrow> inf (filtercomap f F) (principal A) \<le> inf (filtercomap f G) (principal B)
[PROOF STEP]
by (intro inf_mono filtercomap_mono) simp_all