English
For every x in the set of centers β, the center c(x) lies in the union up to the last step: c(x) ∈ p.iUnionUpTo(p.lastStep).
Русский
Для каждого x из множества центров β центр c(x) принадлежит объединению вплоть до последнего шага: c(x) ∈ p.iUnionUpTo(p.lastStep).
LaTeX
$$$\forall x:\n\; p.c(x) \in p.iUnionUpTo(p.lastStep).$$$
Lean4
/-- Every point is covered by chosen balls, before `p.lastStep`. -/
theorem mem_iUnionUpTo_lastStep (x : β) : p.c x ∈ p.iUnionUpTo p.lastStep :=
by
have A : ∀ z : β, p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep :=
by
have : p.lastStep ∈ {i | ¬∃ b : β, p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b} := csInf_mem p.lastStep_nonempty
simpa only [not_exists, mem_setOf_eq, not_and_or, not_le, not_notMem]
by_contra h
rcases A x with (H | H); · exact h H
have Rpos : 0 < p.R p.lastStep := by apply lt_trans (mul_pos (_root_.zero_lt_one.trans p.one_lt_tau) (p.rpos _)) H
have B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep :=
by
conv_rhs => rw [← one_mul (p.R p.lastStep)]
exact mul_lt_mul (inv_lt_one_of_one_lt₀ p.one_lt_tau) le_rfl Rpos zero_le_one
obtain ⟨y, hy1, hy2⟩ : ∃ y, p.c y ∉ p.iUnionUpTo p.lastStep ∧ p.τ⁻¹ * p.R p.lastStep < p.r y :=
by
have := exists_lt_of_lt_csSup ?_ B
· simpa only [exists_prop, mem_range, exists_exists_and_eq_and, Subtype.exists, Subtype.coe_mk]
rw [← image_univ, image_nonempty]
exact ⟨⟨_, h⟩, mem_univ _⟩
rcases A y with (Hy | Hy)
· exact hy1 Hy
· rw [← div_eq_inv_mul] at hy2
have := (div_le_iff₀' (_root_.zero_lt_one.trans p.one_lt_tau)).1 hy2.le
exact lt_irrefl _ (Hy.trans_le this)
