X : Type u_1
Y : Type u_2
Z : Type ?u.6330
α : Type ?u.6333
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this : TopologicalSpace Y := ⊥
⊢ Set.Finite (range f)
X : Type u_1
Y : Type u_2
Z : Type ?u.6330
α : Type ?u.6333
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
⊢ Set.Finite (range f)
letI : TopologicalSpace Y := ⊥
X : Type u_1
Y : Type u_2
Z : Type ?u.6330
α : Type ?u.6333
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this✝ : TopologicalSpace Y := ⊥
this : DiscreteTopology Y
⊢ Set.Finite (range f)
X : Type u_1
Y : Type u_2
Z : Type ?u.6330
α : Type ?u.6333
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this : TopologicalSpace Y := ⊥
⊢ Set.Finite (range f)
haveI := discreteTopology_bot Y
no goals
X : Type u_1
Y : Type u_2
Z : Type ?u.6330
α : Type ?u.6333
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this✝ : TopologicalSpace Y := ⊥
this : DiscreteTopology Y
⊢ Set.Finite (range f)
exact (isCompact_range hf.continuous).finite_of_discrete