isCoseparating — Mathlib

English

If a set 𝒢 is codetecting in C, then it is coseparating in C.

Русский

Если множество 𝒢 кодетектирует в C, то оно же косепарирует в C.

LaTeX

$$$IsCodetecting(\mathcal{G}) \Rightarrow IsCoseparating(\mathcal{G})$$$

Lean4

theorem isCoseparating [HasCoequalizers C] {𝒢 : Set C} : IsCodetecting 𝒢 → IsCoseparating 𝒢 := by
  simpa only [← isSeparating_op_iff, ← isDetecting_op_iff] using IsDetecting.isSeparating

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