English
Under the same hypotheses as above, there exists an open set t with s ⊆ t and InjOn f t.
Русский
При тех же условиях существует открытое множество t с s ⊆ t и InjOn f t.
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, IsOpen t ∧ s ⊆ t ∧ 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 an open neighborhood of this set. -/
theorem exists_isOpen_superset {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, IsOpen t ∧ s ⊆ t ∧ InjOn f t :=
let ⟨_t, hst, ht⟩ := inj.exists_mem_nhdsSet sc fc loc
let ⟨u, huo, hsu, hut⟩ := mem_nhdsSet_iff_exists.1 hst
⟨u, huo, hsu, ht.mono hut⟩
