English
If f: α → 𝕜 is defined on a preconnected set S with f^2 = 1 on S and g z ≠ 0 on S, then either f = g on S or f = −g on S.
Русский
Если f: α → 𝕜 определена на предсоединенном множестве S и f^2 = 1 на S, и g(z) ≠ 0 на S, то либо f = g на S, либо f = −g на S.
LaTeX
$$IsPreconnected S → ContinuousOn f S → ContinuousOn g S → EqOn (f^2) (g^2) S → ∀ {x ∈ S}, g x ≠ 0 → EqOn f g S ∨ EqOn f (−g) S$$
Lean4
/-- If `f, g` are functions `α → 𝕜`, both continuous on a preconnected set `S`, with
`f ^ 2 = g ^ 2` on `S`, and `g z ≠ 0` all `z ∈ S`, then either `f = g` or `f = -g` on
`S`. -/
theorem eq_or_eq_neg_of_sq_eq [Field 𝕜] [ContinuousInv₀ 𝕜] [ContinuousMul 𝕜] (hS : IsPreconnected S)
(hf : ContinuousOn f S) (hg : ContinuousOn g S) (hsq : EqOn (f ^ 2) (g ^ 2) S)
(hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0) : EqOn f g S ∨ EqOn f (-g) S :=
by
have hsq : EqOn ((f / g) ^ 2) 1 S := fun x hx => by
simpa [div_eq_one_iff_eq (pow_ne_zero _ (hg_ne hx)), div_pow] using hsq hx
simpa +contextual [EqOn, div_eq_iff (hg_ne _)] using hS.eq_one_or_eq_neg_one_of_sq_eq (hf.div hg fun z => hg_ne) hsq
