English
Let e: α → β with dense range. If the closed set {q ∈ β × β | p q.1 q.2} contains all pairs (e a1, e a2), then p(b1,b2) for all b1,b2.
Русский
Пусть e: α → β имеет плотное образующее. Если замкнутое множество {q ∈ β × β | p q1 q2} содержит все пары вида (e a1, e a2), то p(b1,b2) выполняется для всех b1,b2.
LaTeX
$$$$\operatorname{DenseRange}(e) \Rightarrow \forall b_1,b_2\, p(b_1,b_2).$$$$
Lean4
/-- Two continuous functions to a t2-space that agree on the dense range of a function are equal. -/
theorem equalizer (hfd : DenseRange f) {g h : β → γ} (hg : Continuous g) (hh : Continuous h) (H : g ∘ f = h ∘ f) :
g = h :=
funext fun y => hfd.induction_on y (isClosed_eq hg hh) <| congr_fun H
