isSection

Mathlib.Topology.Sheaves.LocalPredicate

URI: https://scilib.ai/kg/mathlib#TopCat.isSection

Lean4

/-- The local predicate of being a partial section of a function. -/
def isSection {T} (p : T → X) : LocalPredicate fun _ : X ↦ T
    where
  pred f := p ∘ f = (↑)
  res _ _ h := funext fun _ ↦ congr_fun h _
  locality _
    w :=
    funext fun x ↦
      have ⟨_, hV, _, h⟩ := w x;
      congr_fun h ⟨x, hV⟩

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

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

Разделы

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

Аффилиация

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