IsLocallyInjective — Mathlib

English

A function f is locally injective if every point has a neighborhood on which f is injective.

Русский

Функция f локально инъективна, если для каждой точки найдется окрестность, на которой f инъективна.

LaTeX

$$def IsLocallyInjective (f : X → Y) : Prop := ∀ x : X, ∃ U, IsOpen U ∧ x ∈ U ∧ U.InjOn f$$

Lean4

/-- A function from a topological space `X` is locally injective if every point of `X`
  has a neighborhood on which `f` is injective. -/
def IsLocallyInjective (f : X → Y) : Prop :=
  ∀ x : X, ∃ U, IsOpen U ∧ x ∈ U ∧ U.InjOn f

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