Theory Max_Flow_Min_Cut_Countable

(* Author: Andreas Lochbihler, ETH Zurich & Digital Asset *)

theory Max_Flow_Min_Cut_Countable imports
  MFMC_Bounded
  MFMC_Unbounded
begin

section ‹The Max-Flow Min-Cut theorem›

theorem max_flow_min_cut_countable:
  fixes Δ (structure)
  assumes countable_E [simp]: "countable E"
  and source_neq_sink [simp]: "source Δ  sink Δ"
  and capacity_outside: "e. e  E  capacity Δ e = 0"
  and capacity_finite [simp]: "e. capacity Δ e  "
  shows "f S. flow Δ f  cut Δ S  orthogonal Δ f S"
proof -
  interpret countable_network Δ using assms by(unfold_locales) auto
  show ?thesis by(rule max_flow_min_cut)
qed

hide_const (open) A B weight

end