coequalizer_isOpen_iff — Mathlib

English

Let U be an open subset of the coequalizer of f and g. Then U is open if and only if its preimage under the coequalizer projection π is open in the domain space. This is the same quotient-open criterion expressed for coequalizers.

Русский

Пусть U является открытым подмножеством ко-эквалентного пространства дробления f и g. Тогда U открыто тогда и только тогда, когда его предобраз под проекции π открыто в исходном пространстве.

LaTeX

$$$\\IsOpen(U) \\iff \\IsOpen(\\pi^{-1}(U))$$$

Lean4

theorem coequalizer_isOpen_iff (U : Set ((coequalizer f g :) : Type u)) : IsOpen U ↔ IsOpen (coequalizer.π f g ⁻¹' U) :=
  isOpen_iff_of_isColimit_cofork _ (coequalizerIsCoequalizer f g) _

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