isoRestrict_hom_ofRestrict — Mathlib

English

If hf is an open embedding f: X → Y, then Y restricted along hf is an open immersion.

Русский

Если hf — открытое вложение f: X → Y, то ограничение Y по hf является открытым вложением.

LaTeX

$$$\text{IsOpenImmersion}(Y|_{hf}).$$$

Lean4

@[reassoc (attr := simp)]
theorem isoRestrict_hom_ofRestrict : (isoRestrict f).hom ≫ Y.ofRestrict _ = f :=
  PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict f

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