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