of_isOpenImmersion — Mathlib

English

If Q contains identities, then for any open immersion f, the property P holds for f.

Русский

Если Q содержит тождественные гомоморфизмы, то для любого открытого погружения f свойство P выполняется для f.

LaTeX

$$$(\text{RingHom.ContainsIdentities } Q) \Rightarrow [\text{IsOpenImmersion } f] \Rightarrow P(f).$$$

Lean4

theorem of_isOpenImmersion (hP : RingHom.ContainsIdentities Q) [IsOpenImmersion f] : P f :=
  haveI : P.ContainsIdentities := containsIdentities hP
  IsZariskiLocalAtSource.of_isOpenImmersion f

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