α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
i j : Ordinal
hij : i ≤ j
⊢ iUnionUpTo p i ≤ iUnionUpTo p j
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
⊢ Monotone (iUnionUpTo p)
intro i j hij
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
i j : Ordinal
hij : i ≤ j
⊢ (⋃ (j : { j // j < i }),
      ball (BallPackage.c p.toBallPackage (index p ↑j)) (BallPackage.r p.toBallPackage (index p ↑j))) ≤
    ⋃ (j_1 : { j_1 // j_1 < j }),
      ball (BallPackage.c p.toBallPackage (index p ↑j_1)) (BallPackage.r p.toBallPackage (index p ↑j_1))
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
i j : Ordinal
hij : i ≤ j
⊢ iUnionUpTo p i ≤ iUnionUpTo p j
simp only [iUnionUpTo]
no goals
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
i j : Ordinal
hij : i ≤ j
⊢ (⋃ (j : { j // j < i }),
      ball (BallPackage.c p.toBallPackage (index p ↑j)) (BallPackage.r p.toBallPackage (index p ↑j))) ≤
    ⋃ (j_1 : { j_1 // j_1 < j }),
      ball (BallPackage.c p.toBallPackage (index p ↑j_1)) (BallPackage.r p.toBallPackage (index p ↑j_1))
exact iUnion_mono' fun r => ⟨⟨r, r.2.trans_le hij⟩, Subset.rfl⟩