α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
⊢ ∃ g, Disjoint K (g • L)
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
⊢ ∃ g, Disjoint K (g • L)
have A : ¬K * L⁻¹ = univ := (hK.mul hL.inv).ne_univ
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
⊢ ∃ g, Disjoint K (g • L)
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
⊢ ∃ g, Disjoint K (g • L)
obtain ⟨g, hg⟩ : ∃ g, g ∉ K * L⁻¹ := by
  contrapose! A
  exact eq_univ_iff_forall.2 A
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
⊢ Disjoint K (g • L)
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
⊢ ∃ g, Disjoint K (g • L)
refine' ⟨g, _⟩
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
a : G
ha : a ∈ K
h'a : a ∈ g • L
⊢ g ∈ K * L⁻¹
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
⊢ Disjoint K (g • L)
refine disjoint_left.2 fun a ha h'a => hg ?_
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
b : G
bL : b ∈ L
ha : (fun x => g • x) b ∈ K
⊢ g ∈ K * L⁻¹
case intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
a : G
ha : a ∈ K
h'a : a ∈ g • L
⊢ g ∈ K * L⁻¹
rcases h'a with ⟨b, bL, rfl⟩
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
b : G
bL : b ∈ L
ha : (fun x => g • x) b ∈ K
⊢ (fun x x_1 => x * x_1) (g * b) b⁻¹ = g
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
b : G
bL : b ∈ L
ha : (fun x => g • x) b ∈ K
⊢ g ∈ K * L⁻¹
refine' ⟨g * b, b⁻¹, ha, by simpa only [Set.mem_inv, inv_inv] using bL, _⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
b : G
bL : b ∈ L
ha : (fun x => g • x) b ∈ K
⊢ (fun x x_1 => x * x_1) (g * b) b⁻¹ = g
simp only [smul_eq_mul, mul_inv_cancel_right]
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ∀ (g : G), g ∈ K * L⁻¹
⊢ K * L⁻¹ = univ
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
⊢ ∃ g, ¬g ∈ K * L⁻¹
contrapose! A
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ∀ (g : G), g ∈ K * L⁻¹
⊢ K * L⁻¹ = univ
exact eq_univ_iff_forall.2 A
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : NoncompactSpace G
K L : Set G
hK : IsCompact K
hL : IsCompact L
A : ¬K * L⁻¹ = univ
g : G
hg : ¬g ∈ K * L⁻¹
b : G
bL : b ∈ L
ha : (fun x => g • x) b ∈ K
⊢ b⁻¹ ∈ L⁻¹
simpa only [Set.mem_inv, inv_inv] using bL