eq_targetAffineLocally

Mathlib.AlgebraicGeometry.Morphisms.Basic

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally

English

If HasAffineProperty P Q holds, then P equals targetAffineLocally Q.

Русский

Если выполняется HasAffineProperty P Q, то P равно targetAffineLocally Q.

LaTeX

$$$\mathrm{eq\_targetAffineLocally}:\; P = \mathrm{targetAffineLocally}(Q)$ under HasAffineProperty.$$

Lean4

theorem eq_targetAffineLocally : P = targetAffineLocally Q :=
  eq_targetAffineLocally'

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

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

Разделы

Аффилиация

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