Theorems · Theorem · general topology

isPreconnected_of_forall_constant

∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
  (∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y) → IsPreconnected s

If every map to Bool (a discrete two-element space), that is continuous on a set s, is constant on s, then s is preconnected

Defined in

Mathlib.Topology.Connected.Clopen

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpace