section_spec

Mathlib.Geometry.Manifold.Sheaf.Basic

URI: https://scilib.ai/kg/mathlib#StructureGroupoid.LocalInvariantProp.section_spec

← MathLib Explorer

English

For a local invariantProp hG, a section f of the lifted sheaf satisfies LiftProp P.

Русский

Для локального invariantProp hG секция f обладает свойством LiftProp P.

LaTeX

$$StructureGroupoid.LocalInvariantProp.section_spec hG U f : ChartedSpace.LiftProp P f$$

Lean4

theorem section_spec (hG : LocalInvariantProp G G' P) (U : (Opens (TopCat.of M))ᵒᵖ) (f : (hG.sheaf M M').val.obj U) :
    ChartedSpace.LiftProp P f :=
  f.2

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

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

Разделы

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

Аффилиация

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