cover

Mathlib.AlgebraicGeometry.Morphisms.LocalClosure

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.sourceLocalClosure.cover

Lean4

/-- A choice of open cover on which `P` is satisfied if `f` satisfies the source local closure
of `P`. -/
noncomputable def cover {f : X ⟶ Y} (hf : sourceLocalClosure W P f) : Scheme.Cover.{u} (Scheme.precoverage W) X :=
  hf.choose

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

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

Разделы

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

Аффилиация

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