English
If a subalgebra s ⊆ C(α,𝕜) separates points, then it separates points strongly: for any v and x,y there is f ∈ s with f(x)=v(x) and f(y)=v(y).
Русский
Если подпалгебра s ⊆ C(α,𝕜) разделяет точки, то она разделяет точки сильнее: для любого v и x,y существует f ∈ s такое, что f(x)=v(x) и f(y)=v(y).
LaTeX
$$$\\text{SeparationStrongly}(s) := \\forall v, x,y, \\exists f\\in s: f(x)=v(x) \\land f(y)=v(y).$$$
Lean4
/-- 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`.
-/
theorem strongly {s : Subalgebra 𝕜 C(α, 𝕜)} (h : s.SeparatesPoints) : (s : Set C(α, 𝕜)).SeparatesPointsStrongly :=
fun v x y => by
by_cases n : x = y
· subst n
exact ⟨_, (v x • (1 : s) : s).prop, mul_one _, mul_one _⟩
obtain ⟨_, ⟨f, hf, rfl⟩, hxy⟩ := h n
replace hxy : f x - f y ≠ 0 := sub_ne_zero_of_ne hxy
let a := v x
let b := v y
let f' : s := ((b - a) * (f x - f y)⁻¹) • (algebraMap _ s (f x) - (⟨f, hf⟩ : s)) + algebraMap _ s a
refine ⟨f', f'.prop, ?_, ?_⟩
· simp [a, b, f']
· simp [a, b, f', inv_mul_cancel_right₀ hxy]
