α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
⊢ ∀ {K L : Set G}, IsCompact K → IsCompact L → Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
intro K L hK hL
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite ((↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K)ᶜ)ᶜ)
⊢ Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
α : Type u
β : Type v
G : Type w
H : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
have H : Set.Finite _ := hS ((hL.prod hK).image continuous_div').compl_mem_cocompact
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K))
⊢ Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite ((↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K)ᶜ)ᶜ)
⊢ Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
rw [preimage_compl, compl_compl] at H
case h.e'_2
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K))
⊢ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} = ↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K)
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K))
⊢ Set.Finite {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}
convert H
case h.e'_2.h
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K))
x : { x // x ∈ S }
⊢ x ∈ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} ↔ x ∈ ↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K)
case h.e'_2
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K))
⊢ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} = ↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K)
ext x
case h.e'_2.h
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K))
x : { x // x ∈ S }
⊢ x • K ∩ L ≠ ∅ ↔ ∃ a b, (a, b) ∈ L ×ˢ K ∧ a / b = ↑x
case h.e'_2.h
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K))
x : { x // x ∈ S }
⊢ x ∈ {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} ↔ x ∈ ↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K)
simp only [image_smul, mem_setOf_eq, coeSubtype, mem_preimage, mem_image, Prod.exists]
no goals
case h.e'_2.h
α : Type u
β : Type v
G : Type w
H✝ : Type x
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : TopologicalGroup G
S✝ : Subgroup G
inst✝¹ : Normal S✝
inst✝ : IsClosed ↑S✝
S : Subgroup G
hS : Tendsto (↑(Subgroup.subtype S)) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
H : Set.Finite (↑(Subgroup.subtype S) ⁻¹' ((fun p => p.fst / p.snd) '' L ×ˢ K))
x : { x // x ∈ S }
⊢ x • K ∩ L ≠ ∅ ↔ ∃ a b, (a, b) ∈ L ×ˢ K ∧ a / b = ↑x
exact Set.smul_inter_ne_empty_iff'