Theorems · Theorem · general topology

Dense.lowerBounds_image

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

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

Defined in

Mathlib.Topology.Order.IsLUB

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpacePreorderClosedIciTopologyTopologicalSpace