trans

Mathlib.AlgebraicGeometry.Cover.Directed

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

Lean4

/-- The transition maps of a directed cover. -/
def trans {i j : 𝒰.I₀} (hij : i ⟶ j) : 𝒰.X i ⟶ 𝒰.X j :=
  LocallyDirected.trans hij

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

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

Разделы

Аффилиация

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