Theorems · Theorem · general topology

Subalgebra.SeparatesPoints.strongly

∀ {α : Type u_1} [inst : TopologicalSpace α] {𝕜 : Type u_5} [inst_1 : TopologicalSpace 𝕜] [inst_2 : Field 𝕜]
  [inst_3 : IsTopologicalRing 𝕜] {s : Subalgebra 𝕜 C(α, 𝕜)}, s.SeparatesPoints → (↑s).SeparatesPointsStrongly

Working in continuous functions into a topological field, a subalgebra of functions that separates points also separates points strongly. By the hypothesis, we can find a function f so f x ≠ f y. By an affine transformation in the field we can arrange so that f x = a and f x = b.

Defined in

Mathlib.Topology.ContinuousMap.Algebra

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceFieldIsTopologicalRing