T587 is redundant

[prabau]

Removing (T587) Lindelof => meta-Lindelof as a direct consequence of

• (T654) Lindelof => para-Lindelof
• (T655) para-Lindelof => meta-Lindelof

[felixpernegger]

Lots of theorems are redundant, I made a list of them one time (and could easily reconstruct it if needed). Like 100 iirc.

I think it would make more sense to remove them more systematically (or at least in batches) rather than picking them out 1 by 1 like this

[Moniker1998]

@prabau what about the policy in which we agreed that we won't be removing theorems

[prabau]

(adding @StevenClontz to the conversation)

@Moniker1998 Regarding the prohibition on removing theorems, it was indeed the policy at some point. But that was relaxed after later discussions in Zulip.

I can't find the exact place, but see for example these Zulip threads:
#pi-base > improving theorems in pi-base
and
#pi-base > Lean linkage
(in particular the message from Jul 2, 11:17pm and msgs before and after).

Maybe Steven can give more details.

---

I am not advocating to remove all redundancies. On the contrary, there are good reasons to keep some of them and it would be helpful to even add more redundancies for some situations. I think it should be handled on a case by case basis.

I suggested to remove T587 as derivable from T654 and T655 for the following reasons. All three involved theorems are very simple (trivially verifiable). The Lindelof (P18) property can be considered a rather basic property, but para-Lindelof (P105) and meta-Lindelof (P83) are more "exotic". So expanding the chain P18 -> P83 to P18 -> P105 -> P83 will not expand derivations for results (trait derivations) involving "basic properties" (and results involving more "exotic properties" would have their derivation increased by only 1 step, if at all, so would not widely affect much of anything.)
And removing the redundant theorem seems to make things clearer in this case.

Looking forward to read your opinion.

[felixpernegger]

I agree that some redundant theorems ought to be kept (like urysohns metrization theorem that was added a while ago etc), but the vast majority is quite useless. I agree this is a good theorem to remove in that sense, but I still think it would be more productive to have a broader plan to remove stuff.

[prabau]

@StevenClontz Can you comment on this PR, #1835 (comment) in particular?