[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
hU : IsOpen U
⊢ ↑↑μ U = 0 ↔ U = ∅
[PROOFSTEP]
simpa only [not_lt, nonpos_iff_eq_zero, not_nonempty_iff_eq_empty] using not_congr (hU.measure_pos_iff μ)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
hU : IsOpen U
h : U = ∅
⊢ ↑↑μ U = 0
[PROOFSTEP]
simp [h]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
hU : IsOpen U
⊢ U =ᶠ[ae μ] ∅ ↔ U = ∅
[PROOFSTEP]
rw [ae_eq_empty, hU.measure_zero_iff_eq_empty]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
hF : IsClosed F
⊢ F =ᶠ[ae μ] univ ↔ F = univ
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun h ↦ by rw [h]⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
hF : IsClosed F
h : F = univ
⊢ F =ᶠ[ae μ] univ
[PROOFSTEP]
rw [h]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
hF : IsClosed F
h : F =ᶠ[ae μ] univ
⊢ F = univ
[PROOFSTEP]
rwa [ae_eq_univ, hF.isOpen_compl.measure_eq_zero_iff μ, compl_empty_iff] at h
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
m : MeasurableSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T2Space Y
μ ν : Measure X
inst✝² : IsOpenPosMeasure μ
s U F : Set X
x : X
inst✝¹ : OpensMeasurableSpace X
inst✝ : IsFiniteMeasure μ
hF : IsClosed F
⊢ ↑↑μ F = ↑↑μ univ ↔ F = univ
[PROOFSTEP]
rw [← ae_eq_univ_iff_measure_eq hF.measurableSet.nullMeasurableSet, hF.ae_eq_univ_iff_eq]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
m : MeasurableSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T2Space Y
μ ν : Measure X
inst✝² : IsOpenPosMeasure μ
s U F : Set X
x : X
inst✝¹ : OpensMeasurableSpace X
inst✝ : IsProbabilityMeasure μ
hF : IsClosed F
⊢ ↑↑μ F = 1 ↔ F = univ
[PROOFSTEP]
rw [← measure_univ (μ := μ), hF.measure_eq_univ_iff_eq]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
h : f =ᶠ[ae (restrict μ U)] g
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
⊢ EqOn f g U
[PROOFSTEP]
replace h := ae_imp_of_ae_restrict h
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ∀ᵐ (x : X) ∂μ, x ∈ U → f x = g x
⊢ EqOn f g U
[PROOFSTEP]
simp only [EventuallyEq, ae_iff, not_imp] at h
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ↑↑μ {a | a ∈ U ∧ ¬f a = g a} = 0
⊢ EqOn f g U
[PROOFSTEP]
have : IsOpen (U ∩ {a | f a ≠ g a}) :=
  by
  refine' isOpen_iff_mem_nhds.mpr fun a ha => inter_mem (hU.mem_nhds ha.1) _
  rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩
  exact
    (hf.continuousAt (hU.mem_nhds ha)).prod_mk_nhds (hg.continuousAt (hU.mem_nhds ha))
      (isClosed_diagonal.isOpen_compl.mem_nhds ha')
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ↑↑μ {a | a ∈ U ∧ ¬f a = g a} = 0
⊢ IsOpen (U ∩ {a | f a ≠ g a})
[PROOFSTEP]
refine' isOpen_iff_mem_nhds.mpr fun a ha => inter_mem (hU.mem_nhds ha.1) _
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ↑↑μ {a | a ∈ U ∧ ¬f a = g a} = 0
a : X
ha : a ∈ U ∩ {a | f a ≠ g a}
⊢ {a | f a ≠ g a} ∈ 𝓝 a
[PROOFSTEP]
rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩
[GOAL]
case intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ↑↑μ {a | a ∈ U ∧ ¬f a = g a} = 0
a : X
ha : a ∈ U
ha' : (f a, g a) ∈ (diagonal Y)ᶜ
⊢ {a | f a ≠ g a} ∈ 𝓝 a
[PROOFSTEP]
exact
  (hf.continuousAt (hU.mem_nhds ha)).prod_mk_nhds (hg.continuousAt (hU.mem_nhds ha))
    (isClosed_diagonal.isOpen_compl.mem_nhds ha')
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ↑↑μ {a | a ∈ U ∧ ¬f a = g a} = 0
this : IsOpen (U ∩ {a | f a ≠ g a})
⊢ EqOn f g U
[PROOFSTEP]
replace := (this.eq_empty_of_measure_zero h).le
[GOAL]
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
μ ν : Measure X
inst✝ : IsOpenPosMeasure μ
s U F : Set X
x : X
f g : X → Y
hU : IsOpen U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ↑↑μ {a | a ∈ U ∧ ¬f a = g a} = 0
this : U ∩ {a | f a ≠ g a} ≤ ∅
⊢ EqOn f g U
[PROOFSTEP]
exact fun x hx => Classical.not_not.1 fun h => this ⟨hx, h⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁷ : TopologicalSpace X
m : MeasurableSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : T2Space Y
μ ν : Measure X
inst✝⁴ : IsOpenPosMeasure μ
s U F : Set X
x : X
inst✝³ : OpensMeasurableSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
inst✝¹ : MeasurableSpace Z
inst✝ : BorelSpace Z
f : X → Z
hf : Continuous f
hf_surj : Surjective f
⊢ IsOpenPosMeasure (map f μ)
[PROOFSTEP]
refine' ⟨fun U hUo hUne => _⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁷ : TopologicalSpace X
m : MeasurableSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : T2Space Y
μ ν : Measure X
inst✝⁴ : IsOpenPosMeasure μ
s U✝ F : Set X
x : X
inst✝³ : OpensMeasurableSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
inst✝¹ : MeasurableSpace Z
inst✝ : BorelSpace Z
f : X → Z
hf : Continuous f
hf_surj : Surjective f
U : Set Z
hUo : IsOpen U
hUne : Set.Nonempty U
⊢ ↑↑(map f μ) U ≠ 0
[PROOFSTEP]
rw [Measure.map_apply hf.measurable hUo.measurableSet]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁷ : TopologicalSpace X
m : MeasurableSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : T2Space Y
μ ν : Measure X
inst✝⁴ : IsOpenPosMeasure μ
s U✝ F : Set X
x : X
inst✝³ : OpensMeasurableSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
inst✝¹ : MeasurableSpace Z
inst✝ : BorelSpace Z
f : X → Z
hf : Continuous f
hf_surj : Surjective f
U : Set Z
hUo : IsOpen U
hUne : Set.Nonempty U
⊢ ↑↑μ (f ⁻¹' U) ≠ 0
[PROOFSTEP]
exact (hUo.preimage hf).measure_ne_zero μ (hf_surj.nonempty_preimage.mpr hUne)
[GOAL]
X✝ : Type u_1
inst✝⁴ : PseudoMetricSpace X✝
m✝ : MeasurableSpace X✝
μ✝ : Measure X✝
inst✝³ : IsOpenPosMeasure μ✝
X : Type u_2
inst✝² : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst✝¹ : IsOpenPosMeasure μ
inst✝ : NoAtoms μ
x : X
r : ℝ
⊢ 0 < ↑↑μ (closedBall x r) ↔ 0 < r
[PROOFSTEP]
refine' ⟨fun h ↦ _, measure_closedBall_pos μ x⟩
[GOAL]
X✝ : Type u_1
inst✝⁴ : PseudoMetricSpace X✝
m✝ : MeasurableSpace X✝
μ✝ : Measure X✝
inst✝³ : IsOpenPosMeasure μ✝
X : Type u_2
inst✝² : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst✝¹ : IsOpenPosMeasure μ
inst✝ : NoAtoms μ
x : X
r : ℝ
h : 0 < ↑↑μ (closedBall x r)
⊢ 0 < r
[PROOFSTEP]
contrapose! h
[GOAL]
X✝ : Type u_1
inst✝⁴ : PseudoMetricSpace X✝
m✝ : MeasurableSpace X✝
μ✝ : Measure X✝
inst✝³ : IsOpenPosMeasure μ✝
X : Type u_2
inst✝² : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst✝¹ : IsOpenPosMeasure μ
inst✝ : NoAtoms μ
x : X
r : ℝ
h : r ≤ 0
⊢ ↑↑μ (closedBall x r) ≤ 0
[PROOFSTEP]
rw [(subsingleton_closedBall x h).measure_zero μ]


[GOAL]
α : Type u_1
β : Type ?u.2132
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ ↑↑count s = ∑' (i : ↑s), 1
[PROOFSTEP]
simp only [count, sum_apply, hs, dirac_apply', ← tsum_subtype s (1 : α → ℝ≥0∞), Pi.one_apply]
[GOAL]
α : Type u_1
β : Type ?u.3143
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
⊢ ↑↑count ∅ = 0
[PROOFSTEP]
rw [count_apply MeasurableSet.empty, tsum_empty]
[GOAL]
α : Type u_1
β : Type ?u.3931
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
s : Finset α
s_mble : MeasurableSet ↑s
⊢ ∑ i in s, 1 = ↑(Finset.card s)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type ?u.7325
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ s : Set α
s_fin : Set.Finite s
s_mble : MeasurableSet s
⊢ ↑↑count s = ↑(Finset.card (Finite.toFinset s_fin))
[PROOFSTEP]
simp [← @count_apply_finset' _ _ s_fin.toFinset (by simpa only [Finite.coe_toFinset] using s_mble)]
[GOAL]
α : Type u_1
β : Type ?u.7325
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ s : Set α
s_fin : Set.Finite s
s_mble : MeasurableSet s
⊢ MeasurableSet ↑(Finite.toFinset s_fin)
[PROOFSTEP]
simpa only [Finite.coe_toFinset] using s_mble
[GOAL]
α : Type u_1
β : Type ?u.8457
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : Set.Finite s
⊢ ↑↑count s = ↑(Finset.card (Finite.toFinset hs))
[PROOFSTEP]
rw [← count_apply_finset, Finite.coe_toFinset]
[GOAL]
α : Type u_1
β : Type ?u.8764
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : Set.Infinite s
⊢ ↑↑count s = ⊤
[PROOFSTEP]
refine' top_unique (le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n => _)
[GOAL]
α : Type u_1
β : Type ?u.8764
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : Set.Infinite s
n : ℕ
⊢ ↑n ≤ ↑↑count s
[PROOFSTEP]
rcases hs.exists_subset_card_eq n with ⟨t, ht, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type ?u.8764
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : Set.Infinite s
t : Finset α
ht : ↑t ⊆ s
⊢ ↑(Finset.card t) ≤ ↑↑count s
[PROOFSTEP]
calc
  (t.card : ℝ≥0∞) = ∑ i in t, 1 := by simp
  _ = ∑' i : (t : Set α), 1 := (t.tsum_subtype 1).symm
  _ ≤ count (t : Set α) := le_count_apply
  _ ≤ count s := measure_mono ht
[GOAL]
α : Type u_1
β : Type ?u.8764
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : Set.Infinite s
t : Finset α
ht : ↑t ⊆ s
⊢ ↑(Finset.card t) = ∑ i in t, 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type ?u.12614
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
by_cases hs : s.Finite
[GOAL]
case pos
α : Type u_1
β : Type ?u.12614
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hs : Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
simp [Set.Infinite, hs, count_apply_finite' hs s_mble]
[GOAL]
case neg
α : Type u_1
β : Type ?u.12614
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hs : ¬Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
change s.Infinite at hs
[GOAL]
case neg
α : Type u_1
β : Type ?u.12614
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hs : Set.Infinite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
simp [hs, count_apply_infinite]
[GOAL]
α : Type u_1
β : Type ?u.13909
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
by_cases hs : s.Finite
[GOAL]
case pos
α : Type u_1
β : Type ?u.13909
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hs : Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
exact count_apply_eq_top' hs.measurableSet
[GOAL]
case neg
α : Type u_1
β : Type ?u.13909
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hs : ¬Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
change s.Infinite at hs
[GOAL]
case neg
α : Type u_1
β : Type ?u.13909
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hs : Set.Infinite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
simp [hs, count_apply_infinite]
[GOAL]
α : Type u_1
β : Type ?u.16312
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
⊢ s = ∅
[PROOFSTEP]
have hs : s.Finite := by
  rw [← count_apply_lt_top' s_mble, hsc]
  exact WithTop.zero_lt_top
[GOAL]
α : Type u_1
β : Type ?u.16312
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
⊢ Set.Finite s
[PROOFSTEP]
rw [← count_apply_lt_top' s_mble, hsc]
[GOAL]
α : Type u_1
β : Type ?u.16312
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
⊢ 0 < ⊤
[PROOFSTEP]
exact WithTop.zero_lt_top
[GOAL]
α : Type u_1
β : Type ?u.16312
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
hs : Set.Finite s
⊢ s = ∅
[PROOFSTEP]
simpa [count_apply_finite' hs s_mble] using hsc
[GOAL]
α : Type u_1
β : Type ?u.17964
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
⊢ s = ∅
[PROOFSTEP]
have hs : s.Finite := by
  rw [← count_apply_lt_top, hsc]
  exact WithTop.zero_lt_top
[GOAL]
α : Type u_1
β : Type ?u.17964
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
⊢ Set.Finite s
[PROOFSTEP]
rw [← count_apply_lt_top, hsc]
[GOAL]
α : Type u_1
β : Type ?u.17964
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
⊢ 0 < ⊤
[PROOFSTEP]
exact WithTop.zero_lt_top
[GOAL]
α : Type u_1
β : Type ?u.17964
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
hs : Set.Finite s
⊢ s = ∅
[PROOFSTEP]
simpa [count_apply_finite _ hs] using hsc
[GOAL]
α : Type u_1
β : Type ?u.20387
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs' : Set.Nonempty s
s_mble : MeasurableSet s
⊢ ↑↑count s ≠ 0
[PROOFSTEP]
rw [Ne.def, count_eq_zero_iff' s_mble]
[GOAL]
α : Type u_1
β : Type ?u.20387
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs' : Set.Nonempty s
s_mble : MeasurableSet s
⊢ ¬s = ∅
[PROOFSTEP]
exact hs'.ne_empty
[GOAL]
α : Type u_1
β : Type ?u.20618
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hs' : Set.Nonempty s
⊢ ↑↑count s ≠ 0
[PROOFSTEP]
rw [Ne.def, count_eq_zero_iff]
[GOAL]
α : Type u_1
β : Type ?u.20618
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hs' : Set.Nonempty s
⊢ ¬s = ∅
[PROOFSTEP]
exact hs'.ne_empty
[GOAL]
α : Type u_1
β : Type ?u.20894
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
ha : MeasurableSet {a}
⊢ ↑↑count {a} = 1
[PROOFSTEP]
rw [count_apply_finite' (Set.finite_singleton a) ha, Set.Finite.toFinset]
[GOAL]
α : Type u_1
β : Type ?u.20894
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
ha : MeasurableSet {a}
⊢ ↑(Finset.card (toFinset {a})) = 1
[PROOFSTEP]
simp [@toFinset_card _ _ (Set.finite_singleton a).fintype, @Fintype.card_unique _ _ (Set.finite_singleton a).fintype]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
⊢ ↑↑count (f '' s) = ↑↑count s
[PROOFSTEP]
by_cases hs : s.Finite
[GOAL]
case pos
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
[PROOFSTEP]
lift s to Finset β using hs
[GOAL]
case pos.intro
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ ↑↑count (f '' ↑s) = ↑↑count ↑s
[PROOFSTEP]
rw [← Finset.coe_image, count_apply_finset' _, count_apply_finset' s_mble, s.card_image_of_injective hf]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ MeasurableSet ↑(Finset.image f s)
[PROOFSTEP]
simpa only [Finset.coe_image] using fs_mble
[GOAL]
case neg
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
[PROOFSTEP]
rw [count_apply_infinite hs]
[GOAL]
case neg
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ⊤
[PROOFSTEP]
rw [← finite_image_iff <| hf.injOn _] at hs
[GOAL]
case neg
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬Set.Finite (f '' s)
⊢ ↑↑count (f '' s) = ⊤
[PROOFSTEP]
rw [count_apply_infinite hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
⊢ ↑↑count (f '' s) = ↑↑count s
[PROOFSTEP]
by_cases hs : s.Finite
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
[PROOFSTEP]
exact count_injective_image' hf hs.measurableSet (Finite.image f hs).measurableSet
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
[PROOFSTEP]
rw [count_apply_infinite hs]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ⊤
[PROOFSTEP]
rw [← finite_image_iff <| hf.injOn _] at hs
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬Set.Finite (f '' s)
⊢ ↑↑count (f '' s) = ⊤
[PROOFSTEP]
rw [count_apply_infinite hs]
[GOAL]
α : Type ?u.24262
β : Type ?u.24265
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
inst✝¹ : Finite α
inst✝ : MeasurableSpace α
⊢ ↑↑count univ < ⊤
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type ?u.24262
β : Type ?u.24265
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
inst✝¹ : Finite α
inst✝ : MeasurableSpace α
val✝ : Fintype α
⊢ ↑↑count univ < ⊤
[PROOFSTEP]
simpa [Measure.count_apply, tsum_fintype] using (ENNReal.nat_ne_top _).lt_top