α : Type u_3
G : Type u_1
ι : Type u_2
inst✝² : Group G
𝔖 : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
this : HasBasis (comap (fun p => p.snd / p.fst) (𝓝 1)) p fun i => (fun p => p.snd / p.fst) ⁻¹' b i
⊢ HasBasis (𝓝 1) p fun i => {f | ∀ (x : α), f x ∈ b i}
α : Type u_3
G : Type u_1
ι : Type u_2
inst✝² : Group G
𝔖 : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
⊢ HasBasis (𝓝 1) p fun i => {f | ∀ (x : α), f x ∈ b i}
have := h.comap fun p : G × G => p.2 / p.1
α : Type u_3
G : Type u_1
ι : Type u_2
inst✝² : Group G
𝔖 : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
this : HasBasis (uniformity G) p fun i => (fun p => p.snd / p.fst) ⁻¹' b i
⊢ HasBasis (𝓝 1) p fun i => {f | ∀ (x : α), f x ∈ b i}
α : Type u_3
G : Type u_1
ι : Type u_2
inst✝² : Group G
𝔖 : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
this : HasBasis (comap (fun p => p.snd / p.fst) (𝓝 1)) p fun i => (fun p => p.snd / p.fst) ⁻¹' b i
⊢ HasBasis (𝓝 1) p fun i => {f | ∀ (x : α), f x ∈ b i}
rw [← uniformity_eq_comap_nhds_one] at this
case h.e'_5.h.h.e'_2.h.a
α : Type u_3
G : Type u_1
ι : Type u_2
inst✝² : Group G
𝔖 : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
this : HasBasis (uniformity G) p fun i => (fun p => p.snd / p.fst) ⁻¹' b i
x✝¹ : ι
x✝ : α →ᵤ G
⊢ (∀ (x : α), x✝ x ∈ b x✝¹) ↔ (1, x✝) ∈ UniformFun.gen α G ((fun p => p.snd / p.fst) ⁻¹' b x✝¹)
α : Type u_3
G : Type u_1
ι : Type u_2
inst✝² : Group G
𝔖 : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
this : HasBasis (uniformity G) p fun i => (fun p => p.snd / p.fst) ⁻¹' b i
⊢ HasBasis (𝓝 1) p fun i => {f | ∀ (x : α), f x ∈ b i}
convert UniformFun.hasBasis_nhds_of_basis α _ (1 : α →ᵤ G) this
no goals
case h.e'_5.h.h.e'_2.h.a
α : Type u_3
G : Type u_1
ι : Type u_2
inst✝² : Group G
𝔖 : Set (Set α)
inst✝¹ : UniformSpace G
inst✝ : UniformGroup G
p : ι → Prop
b : ι → Set G
h : HasBasis (𝓝 1) p b
this : HasBasis (uniformity G) p fun i => (fun p => p.snd / p.fst) ⁻¹' b i
x✝¹ : ι
x✝ : α →ᵤ G
⊢ (∀ (x : α), x✝ x ∈ b x✝¹) ↔ (1, x✝) ∈ UniformFun.gen α G ((fun p => p.snd / p.fst) ⁻¹' b x✝¹)
simp [UniformFun.gen]