English
If f, g are continuous on a preconnected set S with f^2 = g^2 on S and g z ≠ 0 on S, then as soon as f y = g y holds at one point y ∈ S, it holds for all points of S; i.e., f ≡ g on S.
Русский
Если f, g непрерывны на предсоединенном множестве S, и f^2 = g^2 на S, и g не равна нулю на S, то при наличии хотя бы одного y ∈ S с f(y) = g(y) имеем f ≡ g на S.
LaTeX
$$IsPreconnected S → ContinuousOn f S → ContinuousOn g S → EqOn (f^2) (g^2) S → ∀ {y} (hy : y ∈ S), f y = g y → 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 as soon as `f = g` holds at
one point of `S` it holds for all points. -/
theorem eq_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) {y : α} (hy : y ∈ S)
(hy' : f y = g y) : EqOn f g S := fun x hx =>
by
rcases hS.eq_or_eq_neg_of_sq_eq hf hg @hsq @hg_ne with (h | h)
· exact h hx
·
rw [h _, Pi.neg_apply, neg_eq_iff_add_eq_zero, ← two_mul, mul_eq_zero,
(iff_of_eq (iff_false _)).2 (hg_ne _)] at hy' ⊢ <;>
assumption
