DiscreteTopology bot

Stream: mathlib4

[Yury G. Kudryashov]

In Lean 3, we have docs#discrete_topology_bot. While porting this file, the naive approach

instance : @DiscreteTopology α ⊥ where
  eq_bot := rfl

failed because it tried to find [TopologicalSpace α] for DiscreteTopology.mk. While I can define this instance using @DiscreteTopology.mk, I took this as a hint that this instance can be less useful in Lean 4 than it was in Lean 3 and deleted it (backported in #18312 together with other changes). Am I right? Or it makes sense to have it?

[Yury G. Kudryashov]

@Gabriel Ebner @Mario Carneiro :up:

[Gabriel Ebner]

It seems useful, but as a def.

[Gabriel Ebner]

But removing it also seems fine if it's never used.

[Mario Carneiro]

it strikes me more as an endpoint theorem such that removing it would be weird even if it's not used

[Mario Carneiro]

is it actually not found when you search for that instance directly?

[Mario Carneiro]

it's not too surprising that the instance definition itself requires some extra @, but if you have a @DiscreteTopology α ⊥ instance search I think we want this instance to solve it

[Gabriel Ebner]

I do not want to declare this as an instance, since it does not work well with (discrimination tree) indexing. Lean will try to apply it for any DiscreteTopology goal.

[Yury G. Kudryashov]

As a lemma, it's just ⟨rfl⟩.

[Yury G. Kudryashov]

But I can restore it.

[Mario Carneiro]

Yury G. Kudryashov said:

As a lemma, it's just ⟨rfl⟩.

It's ⟨rfl⟩ and an annoying type signature to write