Semicontinuity definition for non-linear orders

Stream: maths

[Anatole Dedecker]

I was going to add the theorem that semicontinuity is equivalent to continuity for some order topology (docs#Topology.upper or docs#Topology.lower), but I realized I can't prove this equivalence without linearity of the order, because semicontinuity is defined in terms of open intervals, while lower/upper topologies are defined by complements of closed intervals, which is not the same (e.g compare docs#Topology.IsLower.continuous_iff_Ici with docs#upperSemicontinuous_iff_isOpen_preimage).

Since @Christopher Hoskin introduced the lower/upper topologies with lattices in mind (or at least this is the feeling I get when reading the references of the file), I'm ready to believe that the choice of using closed intervals instead of open ones is mathematically meaningful, which makes sense to me because strict order is not a particularly useful relation in the non-linear context. My question is, should we change the definition of semicontinuity to reflect this?

As an example, the definition of docs#LowerSemicontinuousAt, would become:

def LowerSemicontinuousAt (f : α → β) (x : α) :=
  ∀ y, (∃ᶠ x' in 𝓝 x, f x' ≤ y) → f x ≤ y

[Sébastien Gouëzel]

I am pretty sure that the definition of semicontinuity we have currently was only defined with linear orders in mind. So if another definition is equivalent to the one we have in the linear case, and better behaved in the nonlinear case, go ahead!

[Christopher Hoskin]

@Anatole Dedecker if you equip β with the Scott topology, then I think the lower semi-continuous functions on α should be those that are Scott continuous? At least this is the case when β is the real numbers (Gierz et al, II.2.3).

[Christopher Hoskin]

In a linear order β, the Scott open sets are β and the complements of the lower closures of singletons (Gierz et al, II.1.5) which is why Scott continuity and lower semi-continuity coincide for the reals.

[Christopher Hoskin]

Ignore me, I think the characterisation I was thinking of only makes sense when both spaces have an order structure.

[Christopher Hoskin]

I opened some PRs stimulated by this discussion:

• https://github.com/leanprover-community/mathlib4/pull/12175
• https://github.com/leanprover-community/mathlib4/pull/12221
• https://github.com/leanprover-community/mathlib4/pull/12234