Theorems · Theorem · general topology

Set.EqOn.of_subset_closure

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {s t : Set X}
  {f g : X → Y}, Set.EqOn f g s → ContinuousOn f t → ContinuousOn g t → s ⊆ t → t ⊆ closure s → Set.EqOn f g t

If f x = g x for all x ∈ s and f, g are continuous on t, s ⊆ t ⊆ closure s, then f x = g x for all x ∈ t. See also Set.EqOn.closure.

Defined in

Mathlib.Topology.Separation.Hausdorff

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceT2Space