𝕜 : Type ?u.592530
G : Type u_1
H✝ : Type ?u.592536
inst✝¹² : MeasurableSpace G
inst✝¹¹ : MeasurableSpace H✝
inst✝¹⁰ : Group G
inst✝⁹ : TopologicalSpace G
μ : Measure G
inst✝⁸ : IsHaarMeasure μ
inst✝⁷ : BorelSpace G
inst✝⁶ : TopologicalGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : T2Space H
inst✝ : TopologicalGroup H
f : G →* H
hf : Continuous ↑f
h_surj : Surjective ↑f
h_prop : Tendsto (↑f) (cocompact G) (cocompact H)
K : Set H
hK : IsCompact K
⊢ ↑↑(map (↑f) μ) K < ⊤
𝕜 : Type ?u.592530
G : Type u_1
H✝ : Type ?u.592536
inst✝¹² : MeasurableSpace G
inst✝¹¹ : MeasurableSpace H✝
inst✝¹⁰ : Group G
inst✝⁹ : TopologicalSpace G
μ : Measure G
inst✝⁸ : IsHaarMeasure μ
inst✝⁷ : BorelSpace G
inst✝⁶ : TopologicalGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : T2Space H
inst✝ : TopologicalGroup H
f : G →* H
hf : Continuous ↑f
h_surj : Surjective ↑f
h_prop : Tendsto (↑f) (cocompact G) (cocompact H)
⊢ ∀ ⦃K : Set H⦄, IsCompact K → ↑↑(map (↑f) μ) K < ⊤
intro K hK
𝕜 : Type ?u.592530
G : Type u_1
H✝ : Type ?u.592536
inst✝¹² : MeasurableSpace G
inst✝¹¹ : MeasurableSpace H✝
inst✝¹⁰ : Group G
inst✝⁹ : TopologicalSpace G
μ : Measure G
inst✝⁸ : IsHaarMeasure μ
inst✝⁷ : BorelSpace G
inst✝⁶ : TopologicalGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : T2Space H
inst✝ : TopologicalGroup H
f : G →* H
hf : Continuous ↑f
h_surj : Surjective ↑f
h_prop : Tendsto (↑f) (cocompact G) (cocompact H)
K : Set H
hK : IsCompact K
⊢ ↑↑μ (↑f ⁻¹' K) < ⊤
𝕜 : Type ?u.592530
G : Type u_1
H✝ : Type ?u.592536
inst✝¹² : MeasurableSpace G
inst✝¹¹ : MeasurableSpace H✝
inst✝¹⁰ : Group G
inst✝⁹ : TopologicalSpace G
μ : Measure G
inst✝⁸ : IsHaarMeasure μ
inst✝⁷ : BorelSpace G
inst✝⁶ : TopologicalGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : T2Space H
inst✝ : TopologicalGroup H
f : G →* H
hf : Continuous ↑f
h_surj : Surjective ↑f
h_prop : Tendsto (↑f) (cocompact G) (cocompact H)
K : Set H
hK : IsCompact K
⊢ ↑↑(map (↑f) μ) K < ⊤
rw [map_apply hf.measurable hK.measurableSet]
no goals
𝕜 : Type ?u.592530
G : Type u_1
H✝ : Type ?u.592536
inst✝¹² : MeasurableSpace G
inst✝¹¹ : MeasurableSpace H✝
inst✝¹⁰ : Group G
inst✝⁹ : TopologicalSpace G
μ : Measure G
inst✝⁸ : IsHaarMeasure μ
inst✝⁷ : BorelSpace G
inst✝⁶ : TopologicalGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
inst✝¹ : T2Space H
inst✝ : TopologicalGroup H
f : G →* H
hf : Continuous ↑f
h_surj : Surjective ↑f
h_prop : Tendsto (↑f) (cocompact G) (cocompact H)
K : Set H
hK : IsCompact K
⊢ ↑↑μ (↑f ⁻¹' K) < ⊤
exact IsCompact.measure_lt_top ((⟨⟨f, hf⟩, h_prop⟩ : CocompactMap G H).isCompact_preimage hK)