Theorems · Theorem · general topology

exists_countable_upperSemicontinuous_isGLB

∀ {X : Type u_1} {E : Type u_2} [inst : TopologicalSpace X] [HereditarilyLindelofSpace X] [inst_2 : LinearOrder E]
  [inst_3 : TopologicalSpace E] [OrderClosedTopology E] [DenselyOrdered E] [TopologicalSpace.SeparableSpace E]
  {s : X → E} {𝓕 : Set (X → E)}, (∀ f ∈ 𝓕, UpperSemicontinuous f) → 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][bourbaki1974] See the module docstring for a discussion of the assumptions on E.

Defined in

Mathlib.Topology.Semicontinuity.Lindelof

Cited by

1 results in Mathlib

Foundations

Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceHereditarilyLindelofSpaceLinearOrderTopologicalSpaceOrderClosedTopologyDenselyOrderedTopologicalSpace.SeparableSpace