Theorems · Theorem · field theory

IsPreconnected.eq_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) → ∀ {y : α}, y ∈ S → f y = g y → 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 as soon as f = g holds at one point of S it holds for all points.

Defined in

Mathlib.Topology.Algebra.Field

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceT1SpaceFieldContinuousInv₀ContinuousMul