X : Type u_3
Y : Type ?u.7897
Z : Type ?u.7900
α✝ : Type ?u.7903
inst✝ : TopologicalSpace X
α : Type u_1
β : Type u_2
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen ((fun x => g (f x)) ⁻¹' (g '' s))
X : Type u_3
Y : Type ?u.7897
Z : Type ?u.7900
α✝ : Type ?u.7903
inst✝ : TopologicalSpace X
α : Type u_1
β : Type u_2
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen (f ⁻¹' s)
rw [← preimage_image_eq s inj, preimage_preimage]
no goals
X : Type u_3
Y : Type ?u.7897
Z : Type ?u.7900
α✝ : Type ?u.7903
inst✝ : TopologicalSpace X
α : Type u_1
β : Type u_2
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen ((fun x => g (f x)) ⁻¹' (g '' s))
exact h (g '' s)