α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
h : IsPreconnected s
hs : Set.Nontrivial s
hf : Set.Finite s
⊢ Subsingleton ↑s
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
h : IsPreconnected s
hs : Set.Nontrivial s
⊢ Set.Infinite s
refine' mt (fun hf => (subsingleton_coe s).mp _) (not_subsingleton_iff.mpr hs)
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
h : IsPreconnected s
hs : Set.Nontrivial s
hf : Set.Finite s
this : DiscreteTopology ↑s
⊢ Subsingleton ↑s
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
h : IsPreconnected s
hs : Set.Nontrivial s
hf : Set.Finite s
⊢ Subsingleton ↑s
haveI := @discrete_of_t1_of_finite s _ _ hf.to_subtype
no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
h : IsPreconnected s
hs : Set.Nontrivial s
hf : Set.Finite s
this : DiscreteTopology ↑s
⊢ Subsingleton ↑s
exact @PreconnectedSpace.trivial_of_discrete _ _ (Subtype.preconnectedSpace h) _