theorem AlgebraicGeometry.isSeparated_of_isImmersion {Z X : Scheme} (f : Z ⟶ X) [IsImmersion f] [X.IsSeparated] : Z.IsSeparated

If X is a separated scheme and f : Z ⟶ X is an immersion (in particular locally closed), then Z is also separated (Lem 17, Lec 7).

theorem AlgebraicGeometry.isSeparated_comp_of_isImmersion {Z X S : Scheme} (f : Z ⟶ X) (g : X ⟶ S) [IsImmersion f] [IsSeparated g] : IsSeparated (CategoryTheory.CategoryStruct.comp f g)

The composition of an immersion with a separated morphism is separated.