[STATEMENT]
lemma countable_bipartite_web_reduce_weight:
  assumes "weight \<Gamma> x \<ge> w"
  shows "countable_bipartite_web (reduce_weight \<Gamma> x w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable_bipartite_web (reduce_weight \<Gamma> x w)
[PROOF STEP]
using bipartite_V A_vertex bipartite_E disjoint assms
[PROOF STATE]
proof (prove)
using this:
\<^bold>V \<subseteq> A \<Gamma> \<union> B \<Gamma>
A \<Gamma> \<subseteq> \<^bold>V
edge \<Gamma> ?x ?y \<Longrightarrow> ?x \<in> A \<Gamma> \<and> ?y \<in> B \<Gamma>
A \<Gamma> \<inter> B \<Gamma> = {}
ennreal w \<le> weight \<Gamma> x

goal (1 subgoal):
 1. countable_bipartite_web (reduce_weight \<Gamma> x w)
[PROOF STEP]
by unfold_locales (auto 4 3 simp add: weight_outside )