Theorems · Theorem · general topology

Dense.upperBounds_image

∀ {γ : Type u_2} {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] {f : γ → α}
  [inst_3 : TopologicalSpace γ] {S : Set γ}, Dense S → Continuous f → upperBounds (f '' S) = upperBounds (Set.range f)

The upper bounds of the image of a continuous function on a dense set are equal to the upper bounds of the range of the universe.

Defined in

Mathlib.Topology.Order.IsLUB

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreorderClosedIicTopologyTopologicalSpace