diagonalCoverDiagonalRange

Mathlib.AlgebraicGeometry.Pullbacks

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange

Lean4

/-- The image of `𝒱 i j₁ ×[𝒰 i] 𝒱 i j₂` in `diagonalCover` with `j₁ = j₂` -/
noncomputable def diagonalCoverDiagonalRange : (pullback.diagonalObj f).Opens :=
  ⨆ i : Σ i, (𝒱 i).I₀, ((diagonalCover f 𝒰 𝒱).f ⟨i.1, i.2, i.2⟩).opensRange

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

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

Разделы

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

Аффилиация

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