copy — Mathlib

English

Copy ensures equality of HasAffineProperty under equalities of the underlying morphism-property data.

Русский

Копирование сохраняет равенство HasAffineProperty при равенствах надлежащих данных свойства морфизмов.

LaTeX

$$$\forall P P' Q Q'\; (P = P') (Q = Q') \Rightarrow \mathrm{HasAffineProperty} P' Q'.$$$

Lean4

theorem copy {P P'} {Q Q'} [HasAffineProperty P Q] (e : P = P') (e' : Q = Q') : HasAffineProperty P' Q'
    where
  isLocal_affineProperty := e' ▸ isLocal_affineProperty P
  eq_targetAffineLocally' := e' ▸ e.symm ▸ eq_targetAffineLocally P

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