α : Type u_3
β : Type u_4
γ : Type ?u.83924
ι : Sort ?u.83927
ι' : Sort ?u.83930
π : α → Type u_1
π' : β → Type u_2
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
⊢ HasBasis (comap (Sigma.map f g) (map (Sigma.mk (f a)) l)) (fun s => s ∈ l) fun i => Sigma.mk a '' (g a ⁻¹' id i)
α : Type u_3
β : Type u_4
γ : Type ?u.83924
ι : Sort ?u.83927
ι' : Sort ?u.83930
π : α → Type u_1
π' : β → Type u_2
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
⊢ map (Sigma.mk a) (comap (g a) l) = comap (Sigma.map f g) (map (Sigma.mk (f a)) l)
refine' (((basis_sets _).comap _).map _).eq_of_same_basis _
case h.e'_5.h
α : Type u_3
β : Type u_4
γ : Type ?u.83924
ι : Sort ?u.83927
ι' : Sort ?u.83930
π : α → Type u_1
π' : β → Type u_2
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
x✝ : Set (π' (f a))
⊢ Sigma.mk a '' (g a ⁻¹' id x✝) = Sigma.map f g ⁻¹' (Sigma.mk (f a) '' id x✝)
α : Type u_3
β : Type u_4
γ : Type ?u.83924
ι : Sort ?u.83927
ι' : Sort ?u.83930
π : α → Type u_1
π' : β → Type u_2
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
⊢ HasBasis (comap (Sigma.map f g) (map (Sigma.mk (f a)) l)) (fun s => s ∈ l) fun i => Sigma.mk a '' (g a ⁻¹' id i)
convert ((basis_sets l).map (Sigma.mk (f a))).comap (Sigma.map f g)
no goals
case h.e'_5.h
α : Type u_3
β : Type u_4
γ : Type ?u.83924
ι : Sort ?u.83927
ι' : Sort ?u.83930
π : α → Type u_1
π' : β → Type u_2
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
x✝ : Set (π' (f a))
⊢ Sigma.mk a '' (g a ⁻¹' id x✝) = Sigma.map f g ⁻¹' (Sigma.mk (f a) '' id x✝)
apply image_sigmaMk_preimage_sigmaMap hf