isCoseparator_pi_of_isCoseparator

English

If f: β → C and b ∈ β with f(b) a coseparator, then the Pi-object πObj f is a coseparator.

Русский

Если f: β → C и b ∈ β таков, что f(b) является косепаратором, тогда Pi-объект πObj f является косепаратором.

LaTeX

$$$\\mathrm{IsCoseparator}(f(b)) \\Rightarrow \\mathrm{IsCoseparator}(\\pi\\!\\!Obj f)$$$

Lean4

theorem isCoseparator_pi_of_isCoseparator {β : Type w} (f : β → C) [HasProduct f] (b : β) (hb : IsCoseparator (f b)) :
    IsCoseparator (∏ᶜ f) :=
  (isCoseparator_pi _).2 <| IsCoseparating.mono hb <| by simp

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