theorem MDP.tsum_succs_univ_iSup_iSup_EC_comm {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {s : State} {α : Act} {c : M.Costs} [DecidableEq State] : ∑' (s' : ↑(M.succs_univ s)), ⨆ (n : ℕ), ⨆ (𝒮 : 𝔖[M]), M.P s α ↑s' * EC c 𝒮 n ↑s' ≤ ⨆ (n : ℕ), ⨆ (𝒮 : 𝔖[M]), ∑' (s' : ↑(M.succs_univ s)), M.P s α ↑s' * EC c 𝒮 n ↑s'

theorem MDP.iSup_iSup_EC_eq_lfp_Φ𝒜 {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {c : M.Costs} [DecidableEq State] : ⨆ (n : ℕ), ⨆ (𝒮 : 𝔖[M]), EC c 𝒮 n = OrderHom.lfp (Φ Optimization.Angelic c)

theorem MDP.iSup_iSup_ECℒ_le_iSup_iSup_EC {State : Type u_1} {Act : Type u_2} {M : MDP State Act} {c : M.Costs} : ⨆ (n : ℕ), ⨆ (ℒ : 𝔏[M]), EC c (↑ℒ) n ≤ ⨆ (n : ℕ), ⨆ (𝒮 : 𝔖[M]), EC c 𝒮 n