idRestrGroupoid_mem

Mathlib.Geometry.Manifold.ChartedSpace

URI: https://scilib.ai/kg/mathlib#idRestrGroupoid_mem

English

The trivial restriction-closed groupoid idRestrGroupoid is closed under restriction.

Русский

Тривиальный ограниченно-закрытый группоид idRestrGroupoid замкнут по ограничению.

LaTeX

$$$ClosedUnderRestriction\\ idRestrGroupoid$$$

Lean4

theorem idRestrGroupoid_mem {s : Set H} (hs : IsOpen s) : ofSet s hs ∈ @idRestrGroupoid H _ :=
  ⟨s, hs, refl _⟩

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

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

Разделы

Аффилиация

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