structure NetworkFlow.FlowNetwork (V : Type u_2) [Fintype V] [DecidableEq V] : Type u_2

• cap : V → V → ℝ
• s : V
• t : V
• s_ne_t : self.s ≠ self.t
• cap_nonneg (u v : V) : 0 ≤ self.cap u v

structure NetworkFlow.STFlow {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) : Type u_1

• f : V → V → ℝ
• flow_nonneg (u v : V) : 0 ≤ self.f u v
• flow_cap (u v : V) : self.f u v ≤ N.cap u v
• conservation (v : V) : v ≠ N.s → v ≠ N.t → ∑ u : V, self.f u v = ∑ u : V, self.f v u

noncomputable def NetworkFlow.flowValue {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) : ℝ

structure NetworkFlow.STCut {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) : Type u_1

• S : Finset V
• s_mem : N.s ∈ self.S
• t_not_mem : N.t ∉ self.S

noncomputable def NetworkFlow.cutCapacity {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (C : STCut N) : ℝ

theorem NetworkFlow.flow_le_cut {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (C : STCut N) : flowValue N fl ≤ cutCapacity N C