English
If P is stable under post-composition and has restriction property with IsOpenImmersion, then P.HasOfPostcompProperty IsOpenImmersion.
Русский
Если P стабильно после композиции и имеет свойство ограничения совместно с IsOpenImmersion, то P имеет свойство IsOpenImmersion после композиции.
LaTeX
$$$P.HasOfPostcompProperty IsOpenImmersion$$$
Lean4
instance (P : MorphismProperty Scheme) [P.IsStableUnderBaseChange] : P.HasOfPostcompProperty @IsOpenImmersion :=
HasOfPostcompProperty.of_le P (.monomorphisms Scheme) (fun _ _ f _ ↦ inferInstanceAs (Mono f))
