isSeparator_sigma_of_isSeparator — Mathlib

English

If a component f b is a separator, then the coproduct ∐ f is a separator.

Русский

Если компонент f b является разделителем, то coproduct ∐ f является разделителем.

LaTeX

$$$\\mathrm{IsSeparator}(f b) \\Rightarrow \\mathrm{IsSeparator}(\\Bigsqcup_i f(i))$$$

Lean4

theorem isSeparator_sigma_of_isSeparator {β : Type w} (f : β → C) [HasCoproduct f] (b : β) (hb : IsSeparator (f b)) :
    IsSeparator (∐ f) :=
  (isSeparator_sigma _).2 <| IsSeparating.mono hb <| by simp

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