English
If S is preconnected and f: S → 𝕜 is continuous with f^2 ≡ 1 on S, then either f ≡ 1 on S or f ≡ −1 on S.
Русский
Если S является предсоединенным, и f: S → 𝕜 непрерывна с f^2 ≡ 1 на S, то либо f ≡ 1 на S, либо f ≡ −1 на S.
LaTeX
$$IsPreconnected S → ContinuousOn f S → EqOn (f^2) 1 S → EqOn f 1 S ∨ EqOn f (−1) S$$
Lean4
/-- If `f` is a function `α → 𝕜` which is continuous on a preconnected set `S`, and
`f ^ 2 = 1` on `S`, then either `f = 1` on `S`, or `f = -1` on `S`. -/
theorem eq_one_or_eq_neg_one_of_sq_eq [Ring 𝕜] [NoZeroDivisors 𝕜] (hS : IsPreconnected S) (hf : ContinuousOn f S)
(hsq : EqOn (f ^ 2) 1 S) : EqOn f 1 S ∨ EqOn f (-1) S :=
by
have : DiscreteTopology ({1, -1} : Set 𝕜) := Finite.instDiscreteTopology
have hmaps : MapsTo f S {1, -1} := by simpa only [EqOn, Pi.one_apply, Pi.pow_apply, sq_eq_one_iff] using hsq
simpa using hS.eqOn_const_of_mapsTo hf hmaps
