instIsMultiplicativeScheme — Mathlib

English

The class of universally open morphisms is closed under composition and contains identity morphisms.

Русский

Класс морфизмов, являющихся универсально открытыми, замкнут по композиции и содержит тождественные морфизмы.

LaTeX

$$$\forall X,Y,Z \;\forall f:X\to Y, \forall g:Y\to Z, (\mathsf{UniversallyOpen}(f) \land \mathsf{UniversallyOpen}(g)) \Rightarrow \mathsf{UniversallyOpen}(g\circ f) \\ \wedge \\ \forall X:\; \mathsf{UniversallyOpen}(\mathrm{id}_X).$$$

Lean4

instance : MorphismProperty.IsMultiplicative @UniversallyOpen where id_mem _ := inferInstance

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