apply_eq_of_isPreconnected — Mathlib

English

A locally constant function is constant on any preconnected set.

Русский

Локально константная функция константа на любом предсоединенном множестве.

LaTeX

$$IsLocallyConstant f → IsPreconnected s → x ∈ s → y ∈ s → f x = f y$$

Lean4

/-- A locally constant function is constant on any preconnected set. -/
theorem apply_eq_of_isPreconnected {f : X → Y} (hf : IsLocallyConstant f) {s : Set X} (hs : IsPreconnected s) {x y : X}
    (hx : x ∈ s) (hy : y ∈ s) : f x = f y := by
  let U := f ⁻¹' {f y}
  suffices x ∉ Uᶜ from Classical.not_not.1 this
  intro hxV
  specialize hs U Uᶜ (hf {f y}) (hf {f y}ᶜ) _ ⟨y, ⟨hy, rfl⟩⟩ ⟨x, ⟨hx, hxV⟩⟩
  · simp only [union_compl_self, subset_univ]
  · simp only [inter_empty, Set.not_nonempty_empty, inter_compl_self] at hs

Похожие утверждения