English
If every Bool-valued function that is continuous on s is constant on s, then s is preconnected.
Русский
Если для любого булева-функции, непрерывной на s, выполняется константность на s, то s является предсвязанным пространством.
LaTeX
$$∀ s ⊆ α, (∀ f: α → Bool, ContinuousOn f s → ∀ x,y ∈ s, f(x) = f(y)) → IsPreconnected s$$
Lean4
/-- 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 -/
theorem isPreconnected_of_forall_constant {s : Set α}
(hs : ∀ f : α → Bool, ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y) : IsPreconnected s :=
by
unfold IsPreconnected
by_contra!
rcases this with ⟨u, v, u_op, v_op, hsuv, ⟨x, x_in_s, x_in_u⟩, ⟨y, y_in_s, y_in_v⟩, H⟩
have hy : y ∉ u := fun y_in_u => eq_empty_iff_forall_notMem.mp H y ⟨y_in_s, ⟨y_in_u, y_in_v⟩⟩
have : ContinuousOn u.boolIndicator s :=
by
apply (continuousOn_boolIndicator_iff_isClopen _ _).mpr ⟨_, _⟩
· rw [preimage_subtype_coe_eq_compl hsuv H]
exact (v_op.preimage continuous_subtype_val).isClosed_compl
· exact u_op.preimage continuous_subtype_val
simpa [(u.mem_iff_boolIndicator _).mp x_in_u, (u.notMem_iff_boolIndicator _).mp hy] using hs _ this x x_in_s y y_in_s
