appLE_map' — Mathlib

English

A congruence lemma: changing f.appLE by an equality i between opens yields the same equality on the composed maps via appLE.

Русский

Лемма о согласованности: изменение f.appLE в силу равенства между открытиями приводит к той же равенности на составных отображениях через appLE.

LaTeX

$$$f.appLE U V e = f_1.appLE U V e' \Rightarrow \cdots$$$

Lean4

@[reassoc]
theorem appLE_map' (e : V ≤ f ⁻¹ᵁ U) (i : V = V') :
    f.appLE U V' (i ▸ e) ≫ X.presheaf.map (eqToHom i).op = f.appLE U V e :=
  appLE_map _ _ _

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