eqToHom_c_app

Mathlib.AlgebraicGeometry.Scheme

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

English

Duplicate entry: same as previous eqToHom_c_app; equality is preserved under substitution on U.

Русский

Дубликат: то же, что и выше; равенство сохраняется при подстановке на U.

LaTeX

$$$(eqToHom e).app U = eqToHom (by \\; subst e; \\; rfl)$$$

Lean4

theorem eqToHom_c_app {X Y : Scheme} (e : X = Y) (U) : (eqToHom e).app U = eqToHom (by subst e; rfl) := by subst e; rfl

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

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

Разделы

Аффилиация

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