  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
  49      cases this with
  50      | inl hy_prev => exact Or.inl ((ih _).mp hy_prev)
  51      | inr hy_union =>
  52        rcases Finset.mem_biUnion.mp hy_union with ⟨z, hz, hyz⟩
  53        refine Or.inr ⟨z, (ih z).mp hz, ?_⟩
  54        dsimp [KB]
  55        rw [B.step_iff_mem]
  56        exact hyz
  57    · intro hy
  58      cases hy with

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.