instance MDP.Path.instMembership {State : Type u_1} {Act : Type u_2} {M : MDP State Act} : Membership State M.Path

Equations

• MDP.Path.instMembership = { mem := fun (π : M.Path) (s : State) => ∃ (i : Fin ‖π‖), π[i] = s }

@[simp]

theorem MDP.Path.mem_states_iff_mem {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : State} : s ∈ π.states ↔ s ∈ π

theorem MDP.Path.mem_iff_getElem {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) {s : State} : s ∈ π ↔ ∃ (i : Fin ‖π‖), π[i] = s

@[simp]

theorem MDP.Path.getElem_mem {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (i : Fin ‖π‖) : π[i] ∈ π

@[simp]

theorem MDP.Path.getElem_nat_mem {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (i : ℕ) (hi : i < ‖π‖) : π[i] ∈ π

@[simp]

theorem MDP.Path.last_mem {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) : π.last ∈ π

instance MDP.Path.instDecidableForallForallMemEqOfDecidableEq {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) [DecidableEq State] (s : State) : Decidable (∀ s' ∈ π, s' = s)

Equations

• π.instDecidableForallForallMemEqOfDecidableEq s = if h : (π.states.all fun (x : State) => decide (x = s)) = true then isTrue ⋯ else isFalse ⋯

instance MDP.Path.instDecidableMemOfDecidableEq {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) [DecidableEq State] (s : State) : Decidable (s ∈ π)

Equations

• π.instDecidableMemOfDecidableEq s = if h : s ∈ π.states then isTrue ⋯ else isFalse ⋯

@[simp]

theorem MDP.Path.mem_extend {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (π : M.Path) (s : ↑(M.succs_univ π.last)) (s' : State) : s' ∈ π.extend s ↔ s' ∈ π ∨ ↑s = s'

@[simp]

theorem MDP.Path.mem_singleton {State : Type u_1} {Act : Type u_2} {M : MDP State Act} (s s' : State) : s ∈ {s'} ↔ s = s'