α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
set s := {x | ¬∀ᶠ a in v.filterAt x, 0 < μ a} with hs
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
simp (config := { zeta := false }) only [not_lt, not_eventually, nonpos_iff_eq_zero] at hs
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
⊢ ↑↑μ s = 0
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
⊢ ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a
change μ s = 0
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
⊢ ↑↑μ s = 0
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
⊢ ↑↑μ s = 0
let f : α → Set (Set α) := fun _ => {a | μ a = 0}
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
h : FineSubfamilyOn v f s
⊢ ↑↑μ s = 0
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
⊢ ↑↑μ s = 0
have h : v.FineSubfamilyOn f s := by
  intro x hx ε εpos
  rw [hs] at hx
  simp only [frequently_filterAt_iff, exists_prop, gt_iff_lt, mem_setOf_eq] at hx
  rcases hx ε εpos with ⟨a, a_sets, ax, μa⟩
  exact ⟨a, ⟨a_sets, μa⟩, ax⟩
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
h : FineSubfamilyOn v f s
⊢ ↑↑μ s ≤ 0
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
h : FineSubfamilyOn v f s
⊢ ↑↑μ s = 0
refine' le_antisymm _ bot_le
no goals
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
h : FineSubfamilyOn v f s
⊢ ↑↑μ s ≤ 0
calc
  μ s ≤ ∑' x : h.index, μ (h.covering x) := h.measure_le_tsum
  _ = ∑' x : h.index, 0 := by congr; ext1 x; exact h.covering_mem x.2
  _ = 0 := by simp only [tsum_zero, add_zero]
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
⊢ FineSubfamilyOn v f s
intro x hx ε εpos
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
x : α
hx : x ∈ {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
ε : ℝ
εpos : ε > 0
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
rw [hs] at hx
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
x : α
ε : ℝ
εpos : ε > 0
hx : ∀ (ε : ℝ), 0 < ε → ∃ a, a ∈ setsAt v x ∧ a ⊆ closedBall x ε ∧ ↑↑μ a = 0
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
x : α
hx : x ∈ {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
ε : ℝ
εpos : ε > 0
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
simp only [frequently_filterAt_iff, exists_prop, gt_iff_lt, mem_setOf_eq] at hx
case intro.intro.intro
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
x : α
ε : ℝ
εpos : ε > 0
hx : ∀ (ε : ℝ), 0 < ε → ∃ a, a ∈ setsAt v x ∧ a ⊆ closedBall x ε ∧ ↑↑μ a = 0
a : Set α
a_sets : a ∈ setsAt v x
ax : a ⊆ closedBall x ε
μa : ↑↑μ a = 0
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
x : α
ε : ℝ
εpos : ε > 0
hx : ∀ (ε : ℝ), 0 < ε → ∃ a, a ∈ setsAt v x ∧ a ⊆ closedBall x ε ∧ ↑↑μ a = 0
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
rcases hx ε εpos with ⟨a, a_sets, ax, μa⟩
no goals
case intro.intro.intro
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
x : α
ε : ℝ
εpos : ε > 0
hx : ∀ (ε : ℝ), 0 < ε → ∃ a, a ∈ setsAt v x ∧ a ⊆ closedBall x ε ∧ ↑↑μ a = 0
a : Set α
a_sets : a ∈ setsAt v x
ax : a ⊆ closedBall x ε
μa : ↑↑μ a = 0
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
exact ⟨a, ⟨a_sets, μa⟩, ax⟩
case e_f
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
h : FineSubfamilyOn v f s
⊢ (fun x => ↑↑μ (FineSubfamilyOn.covering h ↑x)) = fun x => 0
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
h : FineSubfamilyOn v f s
⊢ (∑' (x : ↑(FineSubfamilyOn.index h)), ↑↑μ (FineSubfamilyOn.covering h ↑x)) = ∑' (x : ↑(FineSubfamilyOn.index h)), 0
congr
case e_f.h
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
h : FineSubfamilyOn v f s
x : ↑(FineSubfamilyOn.index h)
⊢ ↑↑μ (FineSubfamilyOn.covering h ↑x) = 0
case e_f
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
h : FineSubfamilyOn v f s
⊢ (fun x => ↑↑μ (FineSubfamilyOn.covering h ↑x)) = fun x => 0
ext1 x
no goals
case e_f.h
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
h : FineSubfamilyOn v f s
x : ↑(FineSubfamilyOn.index h)
⊢ ↑↑μ (FineSubfamilyOn.covering h ↑x) = 0
exact h.covering_mem x.2
no goals
α : Type u_1
inst✝² : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.472138
inst✝¹ : NormedAddCommGroup E
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in filterAt v x, 0 < ↑↑μ a}
hs : s = {x | ∃ᶠ (x : Set α) in filterAt v x, ↑↑μ x = 0}
f : α → Set (Set α) := fun x => {a | ↑↑μ a = 0}
h : FineSubfamilyOn v f s
⊢ (∑' (x : ↑(FineSubfamilyOn.index h)), 0) = 0
simp only [tsum_zero, add_zero]