English
Let f be injective on a compact set s, continuous at every point of s, and injective on a neighborhood of each point of s. Then there exists a neighborhood t of s on which f is injective.
Русский
Пусть f инъективна на компактном множестве s, непрерывна на каждой точке s, и инъективна на окрестности каждой точки s. Тогда существует окрестность t множества s, на которой f инъективна.
LaTeX
$$$\forall X,Y\,[TopologicalSpace X]\,[TopologicalSpace Y]\,[T2Space Y],\forall f:X\to Y,\forall s\subseteq X\ (inj : InjOn f\ s)\, (sc : IsCompact s)\, (fc:\forall x\in s, ContinuousAt f\ x)\, (loc:\forall x\in s,\exists u\in 𝓝 x, InjOn f\ u)\Rightarrow \exists t\in 𝓝ˢ s, InjOn f\ t$$$
Lean4
/-- If a function `f` is
- injective on a compact set `s`;
- continuous at every point of this set;
- injective on a neighborhood of each point of this set,
then it is injective on a neighborhood of this set. -/
theorem exists_mem_nhdsSet {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} {s : Set X}
(inj : InjOn f s) (sc : IsCompact s) (fc : ∀ x ∈ s, ContinuousAt f x) (loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u) :
∃ t ∈ 𝓝ˢ s, InjOn f t :=
by
have : ∀ x ∈ s ×ˢ s, ∀ᶠ y in 𝓝 x, f y.1 = f y.2 → y.1 = y.2 := fun (x, y) ⟨hx, hy⟩ ↦
by
rcases eq_or_ne x y with rfl | hne
· rcases loc x hx with ⟨u, hu, hf⟩
exact Filter.mem_of_superset (prod_mem_nhds hu hu) <| forall_prod_set.2 hf
· suffices ∀ᶠ z in 𝓝 (x, y), f z.1 ≠ f z.2 from this.mono fun _ hne h ↦ absurd h hne
refine (fc x hx).prodMap' (fc y hy) <| isClosed_diagonal.isOpen_compl.mem_nhds ?_
exact inj.ne hx hy hne
rw [← eventually_nhdsSet_iff_forall, sc.nhdsSet_prod_eq sc] at this
exact eventually_prod_self_iff.1 this
