Enveloppes of Semicontinuous functions on Hereditarily Lindelöf spaces

In this file, we show that, if X is a hereditarily Lindelöf space and 𝓕 is any family of upper semicontinuous functions on X, then there is a countable subfamily 𝓕' with the same infimum / lower enveloppe. Most importantly, this applies whenever X has a SecondCountableTopology.

The codomain E of the functions is assumed to be linearly ordered, and to admit a countable order-dense subset. In particular we do not assume that arbitrary infima exist in E, so our result is of the form "if IsGLB 𝓕 s, then there is a countable 𝓕' ⊆ 𝓕 such that IsGLB 𝓕' s".

Of course we also provide the dual statements for lower semicontinuous functions.

Implementation Notes

There is currently no way to state the hypothesis "E admits a countable order-dense subset" which would be inferrable by typeclass inference. Instead, we assume [TopologicalSpace E] [OrderClosedTopology E] [DenselyOrdered E] [SeparableSpace E], and use Dense.exists_between to show that a chosen countable dense subset is order-dense.

This is not completely satisfying because the hypotheses on E should be purely order-theoretic, but in practice E is either Real, NNReal, ENNReal or EReal, all of which are already equipped with the order topology.

References

• N. Bourbaki, Topologie Générale, Chapitre IX, Appendice I (this appendix does not seem to exist in the English translation)

theorem exists_countable_upperSemicontinuous_isGLB {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [HereditarilyLindelofSpace X] [LinearOrder E] [TopologicalSpace E] [OrderClosedTopology E] [DenselyOrdered E] [TopologicalSpace.SeparableSpace E] {s : X → E} {𝓕 : Set (X → E)} (h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f) (h𝓕 : IsGLB 𝓕 s) : ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ IsGLB 𝓕' s

If a function s : X → E can be written as the infimum of a family 𝓕 of upper semicontinuous functions then, assuming that X is hereditarily Lindelöf (for example, second countable), s can in fact be written as the infimum of some countable subfamily 𝓕'.

This is implication a) ⇒ b) in N. Bourbaki, Topologie Générale, Chapitre IX, Appendice I, Proposition 3

See the module docstring for a discussion of the assumptions on E.

theorem exists_countable_lowerSemicontinuous_isLUB {X : Type u_1} {E : Type u_2} [TopologicalSpace X] [HereditarilyLindelofSpace X] [LinearOrder E] [TopologicalSpace E] [OrderClosedTopology E] [DenselyOrdered E] [TopologicalSpace.SeparableSpace E] {s : X → E} {𝓕 : Set (X → E)} (h𝓕_cont : ∀ f ∈ 𝓕, LowerSemicontinuous f) (h𝓕 : IsLUB 𝓕 s) : ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ IsLUB 𝓕' s

If a function s : X → E can be written as the supremum of a family 𝓕 of lower semicontinuous functions then, assuming that X is hereditarily Lindelöf (for example, second countable), s can in fact be written as the supremum of some countable subfamily 𝓕'.

This is implication a) ⇒ b) in N. Bourbaki, Topologie Générale, Chapitre IX, Appendice I, Proposition 3

See the module docstring for a discussion of the assumptions on E.