homOfLE — Mathlib

English

A corollary about images under open immersions and restrictions.

Русский

Следствие о образах при открытых вложениях и ограничениях.

LaTeX

$$$ \\text{corollary: image inclusions commute under restriction}$$$

Lean4

/-- If `U ≤ V`, then `U` is also a subscheme of `V`. -/
protected noncomputable def homOfLE (X : Scheme.{u}) {U V : X.Opens} (e : U ≤ V) : (U : Scheme.{u}) ⟶ V :=
  IsOpenImmersion.lift V.ι U.ι (by simpa using e)

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