α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ (s ∈ ⨅ (ε : ℝ) (_ : ε ∈ Ioi 0), 𝓟 {a | a ∈ setsAt v x ∧ a ⊆ closedBall x ε}) ↔
    ∃ ε, 0 < ε ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ s ∈ filterAt v x ↔ ∃ ε, ε > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
simp only [filterAt, exists_prop, gt_iff_lt]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ (∃ i, i ∈ Ioi 0 ∧ s ∈ 𝓟 {a | a ∈ setsAt v x ∧ a ⊆ closedBall x i}) ↔
    ∃ ε, 0 < ε ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s

case h
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ DirectedOn ((fun ε => 𝓟 {a | a ∈ setsAt v x ∧ a ⊆ closedBall x ε}) ⁻¹'o fun x x_1 => x ≥ x_1) (Ioi 0)

case ne
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ Set.Nonempty (Ioi 0)
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ (s ∈ ⨅ (ε : ℝ) (_ : ε ∈ Ioi 0), 𝓟 {a | a ∈ setsAt v x ∧ a ⊆ closedBall x ε}) ↔
    ∃ ε, 0 < ε ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
rw [mem_biInf_of_directed]
no goals
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ (∃ i, i ∈ Ioi 0 ∧ s ∈ 𝓟 {a | a ∈ setsAt v x ∧ a ⊆ closedBall x i}) ↔
    ∃ ε, 0 < ε ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
simp only [subset_def, and_imp, exists_prop, mem_sep_iff, mem_Ioi, mem_principal]
case h
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ ∀ (x_1 : ℝ),
    0 < x_1 →
      ∀ (y : ℝ),
        0 < y →
          ∃ z,
            0 < z ∧
              {a | a ∈ setsAt v x ∧ a ⊆ closedBall x z} ⊆ {a | a ∈ setsAt v x ∧ a ⊆ closedBall x x_1} ∧
                {a | a ∈ setsAt v x ∧ a ⊆ closedBall x z} ⊆ {a | a ∈ setsAt v x ∧ a ⊆ closedBall x y}
case h
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ DirectedOn ((fun ε => 𝓟 {a | a ∈ setsAt v x ∧ a ⊆ closedBall x ε}) ⁻¹'o fun x x_1 => x ≥ x_1) (Ioi 0)
simp only [DirectedOn, exists_prop, ge_iff_le, le_principal_iff, mem_Ioi, Order.Preimage,
  mem_principal]
case h
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x✝ : α
s : Set (Set α)
x : ℝ
hx : 0 < x
y : ℝ
hy : 0 < y
⊢ ∃ z,
    0 < z ∧
      {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ z} ⊆ {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ x} ∧
        {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ z} ⊆ {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ y}
case h
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ ∀ (x_1 : ℝ),
    0 < x_1 →
      ∀ (y : ℝ),
        0 < y →
          ∃ z,
            0 < z ∧
              {a | a ∈ setsAt v x ∧ a ⊆ closedBall x z} ⊆ {a | a ∈ setsAt v x ∧ a ⊆ closedBall x x_1} ∧
                {a | a ∈ setsAt v x ∧ a ⊆ closedBall x z} ⊆ {a | a ∈ setsAt v x ∧ a ⊆ closedBall x y}
intro x hx y hy
no goals
case h
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x✝ : α
s : Set (Set α)
x : ℝ
hx : 0 < x
y : ℝ
hy : 0 < y
⊢ ∃ z,
    0 < z ∧
      {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ z} ⊆ {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ x} ∧
        {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ z} ⊆ {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ y}
refine' ⟨min x y, lt_min hx hy,
  fun a ha => ⟨ha.1, ha.2.trans (closedBall_subset_closedBall (min_le_left _ _))⟩,
  fun a ha => ⟨ha.1, ha.2.trans (closedBall_subset_closedBall (min_le_right _ _))⟩⟩
no goals
case ne
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ Set.Nonempty (Ioi 0)
exact ⟨(1 : ℝ), mem_Ioi.2 zero_lt_one⟩