Theorems · Theorem · general topology

IsPreconnected.eqOn_const_of_mapsTo

∀ {α : Type u} [inst : TopologicalSpace α] {S : Set α},
  IsPreconnected S →
    ∀ {β : Type u_3} [inst_1 : TopologicalSpace β] {T : Set β},
      IsDiscrete T →
        ∀ {f : α → β}, ContinuousOn f S → Set.MapsTo f S T → T.Nonempty → ∃ y ∈ T, Set.EqOn f (Function.const α y) S

A version of IsPreconnected.constant_of_mapsTo that assumes that the codomain is nonempty and proves that f is equal to const α y on S for some y ∈ T.

Defined in

Mathlib.Topology.Connected.TotallyDisconnected

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace