ballP

formal source

  15structure Kinematics (α : Type) where
  16  step : α → α → Prop
  17
  18def ballP {α : Type} (K : Kinematics α) (x : α) : Nat → α → Prop
  19| 0, y => y = x
  20| Nat.succ n, y => ballP K x n y ∨ ∃ z, ballP K x n z ∧ K.step z y
  21
  22namespace ConeBound
  23
  24variable {α : Type} {d : Nat}
  25variable [DecidableEq α]
  26variable [B : BoundedStep α d]
  27
  28def KB : Kinematics α := { step := B.step }
  29
  30noncomputable def ballFS (x : α) : Nat → Finset α
  31| 0 => {x}
  32| Nat.succ n =>
  33    let prev := ballFS x n
  34    prev ∪ prev.biUnion (fun z => B.neighbors z)
  35
  36theorem mem_ballFS_iff_ballP (x : α) : ∀ n y, y ∈ ballFS (α:=α) x n ↔ ballP (KB (α:=α)) x n y := by
  37  intro n
  38  induction n with
  39  | zero =>
  40    intro y
  41    simp [ballFS, ballP, Finset.mem_singleton]
  42  | succ n ih =>
  43    intro y
  44    dsimp [ballFS, ballP]
  45    constructor
  46    · intro hy
  47      have : y ∈ ballFS (α:=α) x n ∨ y ∈ (ballFS (α:=α) x n).biUnion (fun z => B.neighbors z) :=
  48        Finset.mem_union.mp hy