locality

Mathlib.Geometry.Manifold.ChartedSpace

URI: https://scilib.ai/kg/mathlib#StructureGroupoid.locality

← MathLib Explorer

English

If for every e ∈ G the local charts restrict to open restrictions, then e lies in G.

Русский

Если для каждого элемента e ∈ G локальные ограничения ограничиваются, то e ∈ G.

LaTeX

$$G.locality' e h$$

Lean4

theorem locality (G : StructureGroupoid H) {e : OpenPartialHomeomorph H H}
    (h : ∀ x ∈ e.source, ∃ s, IsOpen s ∧ x ∈ s ∧ e.restr s ∈ G) : e ∈ G :=
  G.locality' e h

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

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

Разделы

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

Аффилиация

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