Theorems · Theorem · field theory

IsPreconnected.eq_or_eq_neg_of_sq_eq

∀ {α : Type u_2} {𝕜 : Type u_3} {f g : α → 𝕜} {S : Set α} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace 𝕜]
  [T1Space 𝕜] [inst_3 : Field 𝕜] [ContinuousInv₀ 𝕜] [ContinuousMul 𝕜],
  IsPreconnected S →
    ContinuousOn f S →
      ContinuousOn g S → Set.EqOn (f ^ 2) (g ^ 2) S → (∀ {x : α}, x ∈ S → g x ≠ 0) → Set.EqOn f g S ∨ Set.EqOn f (-g) S

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.

Defined in

Mathlib.Topology.Algebra.Field

Cited by

1 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceT1SpaceFieldContinuousInv₀ContinuousMul