Reduce derived proofs

[jamesdabbs]

The proof that a 2-point discrete space is T2.5 uses an assumption that the space is Finite, but the proof that a countably infinite discrete space is T2.5 finds a simpler, more natural proof using just the Discrete assumption.

It's almost certainly computationally infeasible to generate the "most natural" proof (if that's even well-defined), but we can look at some reasonable heuristics and simplification strategies. One straightforward one to implement would be –

• prefer "less complex" proofs
  • record proofs exactly as we do today
  • at display time, search for alternate proofs, removing assumptions

[StevenClontz]

So I had some trouble parsing this graph: https://graph.topology.pages.dev/spaces/S000002/properties/P000044 One thing that'd help a lot is color-coding whether properties are true or false.

Another thing that'd help: for compound theorems, I think we really need a directed hypergraph: https://en.wikipedia.org/wiki/Hypergraph#/media/File:Directed_hypergraph_example.svg So for P and Q then R, we should show an arrow starting from P and Q and pointing to R.

[StevenClontz]

The other thing that would have helped me: presenting T309 as the equivalent Cardinality<c + not Strongly Connected => not Connected because nested contrapositives are hard.