comp_app

Mathlib.AlgebraicGeometry.Cover.MorphismProperty

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Cover.comp_app

Lean4

@[simp]
theorem comp_app {X : Scheme.{u}} {𝒰 𝒱 𝒲 : X.Cover (precoverage P)} (f : 𝒰 ⟶ 𝒱) (g : 𝒱 ⟶ 𝒲) (j : 𝒰.I₀) :
    (f ≫ g).app j = f.app j ≫ g.app _ :=
  rfl

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

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

Разделы

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

Аффилиация

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