lim_eq — Mathlib

English

There exists a t such that t ∈ 𝓝ˢ s and InjOn f t.

Русский

Существует подмножество 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, \ t\in 𝓝ˢ s ∧ InjOn f t$$$

Lean4

theorem lim_eq {x : X} [NeBot f] (h : f ≤ 𝓝 x) : @lim _ _ ⟨x⟩ f = x :=
  tendsto_nhds_unique (le_nhds_lim ⟨x, h⟩) h

Похожие утверждения