Theorems · Theorem · general topology

Dense.ciSup

∀ {γ : Type u_2} {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLattice α]
  [ClosedIicTopology α] {f : γ → α} [inst_3 : TopologicalSpace γ] {S : Set γ},
  Dense S → Continuous f → BddAbove (Set.range f) → ⨆ s, f ↑s = ⨆ i, f i

The supremum of a bounded above, continuous function on a dense set is equal to the supremum on the universe.

Defined in

Mathlib.Topology.Order.IsLUB

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceConditionallyCompleteLatticeClosedIicTopologyTopologicalSpace