Theorems · Theorem · general topology

ContinuousOn.surjOn_of_tendsto

∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {f : α → δ} {s : Set α} [s.OrdConnected],
  s.Nonempty →
    ContinuousOn f s →
      Filter.Tendsto (fun x => f ↑x) Filter.atBot Filter.atBot →
        Filter.Tendsto (fun x => f ↑x) Filter.atTop Filter.atTop → Set.SurjOn f s Set.univ

If a function f : α → β is continuous on a nonempty interval s, its restriction to s tends to Filter.atBot : Filter β along Filter.atBot : Filter ↥s and tends to Filter.atTop : Filter β along Filter.atTop : Filter ↥s, then the restriction of f to s is surjective. We formulate the conclusion as Function.surjOn f s Set.univ.

Defined in

Mathlib.Topology.Order.IntermediateValue

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceConditionallyCompleteLinearOrderOrderTopologyDenselyOrderedLinearOrderTopologicalSpaceOrderClosedTopologySet.OrdConnected