instIsClosedImmersionιOfIsSeparated

English

Another form of the composition criterion: IsSeparated (f ≫ g) iff IsSeparated f when g is separated.

Русский

Еще одна форма критерия композиции: IsSeparated (f ≫ g) эквивалентно IsSeparated f, когда g разделим.

LaTeX

$$IsSeparated(f \circ g) \Leftrightarrow IsSeparated(f)$$

Lean4

instance (f g : X ⟶ Y) [Y.IsSeparated] : IsClosedImmersion (Limits.equalizer.ι f g) :=
  MorphismProperty.of_isPullback (isPullback_equalizer_prod f g).flip inferInstance

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