resLE_congr — Mathlib

English

If U = U' and V = V' via equalities e1, e2, then any property P applied to f.resLE U V e is equivalent to P applied to the corresponding restricted resLE on U',V' adjusting by the equalities.

Русский

Если U = U' и V = V' через равенства e1, e2, то свойство P, применённое к f.resLE U V e, эквивалентно P для соответствующего ограниченного f.resLE на U',V', с учётом равенств.

LaTeX

$$$e_1:U=U'\,\; e_2:V=V'\;\;\Rightarrow\;\ P(f.resLE U V e) \leftrightarrow P(f.resLE U' V' (e_1\,\rsh\, e_2\,\to\, e))$$$

Lean4

theorem resLE_congr (e₁ : U = U') (e₂ : V = V') (P : MorphismProperty Scheme.{u}) :
    P (f.resLE U V e) ↔ P (f.resLE U' V' (e₁ ▸ e₂ ▸ e)) := by subst e₁; subst e₂; rfl

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