isLocallyInjective

Mathlib.Topology.IsLocalHomeomorph

URI: https://scilib.ai/kg/mathlib#IsLocalHomeomorph.isLocallyInjective

← MathLib Explorer

English

A local homeomorphism is locally injective.

Русский

Локальная гомеоморфия локально инъективна.

LaTeX

$$$\operatorname{IsLocalHomeomorph}(f) \Rightarrow \operatorname{IsLocallyInjective}(f)$$$

Lean4

theorem isLocallyInjective (hf : IsLocalHomeomorph f) : IsLocallyInjective f := fun x ↦ by obtain ⟨f, hx, rfl⟩ := hf x;
  exact ⟨f.source, f.open_source, hx, f.injOn⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru