feat: tweak the definition of semicontinuity to behave better in nonlinear orders

[ADedecker]

Summary of the changes:

• change definitions to make lowerSemicontinuous_iff_isClosed_preimage true without assuming LinearOrder, so that semicontinuity corresponds to continuity for lower/upper order topology on the codomain. See discussion on Zulip
• add new iff lemmas for unfolding the definition
• add iff lemmas with the old definition in the linearly ordered case
• some basic lemmas need to be changed in an easy way
• minimize assumptions for continuity => semicontinuity
• prove the semicontinuity criterion for indicators using "preimage of Ici/Iic" instead of a direct proof, because the proof is more natural (especially because we have no filter_upwards for Frequently)
• in the rest of the file (which is about linear orders anyway), we don't touch the statements and just rewrite to the old definition. Some of these could be generalized, but we keep that for a later PR.

---