T1 Alexandrov-discrete topology is discrete

@[simp]

theorem nhdsKer_eq_of_t1Space {X : Type u_1} [TopologicalSpace X] [T1Space X] (s : Set X) : nhdsKer s = s

@[instance 100]

instance instDiscreteTopologyOfAlexandrovDiscreteOfT1Space {X : Type u_1} [TopologicalSpace X] [AlexandrovDiscrete X] [T1Space X] : DiscreteTopology X