RectangleLastSelected.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A finite subfamily of a selection run has a last member. All the other members were present in its actual previous set.

theorem OAI.LipschitzHilbert.RectangleCoverRun.last_selected_witness line 14
theorem OAI.LipschitzHilbert.RectangleCoverRun.selected_previous_witness line 48
Source documentation
Every strictly longer selected rectangle precedes the specified member and belongs to the previous set at its selection.
```
theorem selected_previous_witness (h : RectangleCoverRun R blocked previous stock selected)
    (r : ι) (hr : r ∈ selected) :
    ∃ p : Finset ι, previous ⊆ p ∧
      (∀ j ∈ selected, (R r).long < (R j).long → j ∈ p) ∧ ¬blocked p r := by
…
```
Mentions: OAI.LipschitzHilbert.RectangleCoverRun