English
The product G ⨯ H is a coseparator iff {G,H} is a separating set.
Русский
Произведение G ⨯ H является косепаратором тогда и только тогда, когда множество {G,H} разделяющее.
LaTeX
$$$\\mathrm{IsCoseparator}(\\mathrm{prod}\\ G\\ H) \\iff \\mathrm{IsCoseparating}(\\{G,H\\})$$$
Lean4
theorem isCoseparator_prod (G H : C) [HasBinaryProduct G H] :
IsCoseparator (G ⨯ H) ↔ IsCoseparating ({ G, H } : Set C) :=
by
refine ⟨fun h X Y u v huv => ?_, fun h => (isCoseparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => ?_⟩
· refine h.def _ _ fun g => Limits.prod.hom_ext ?_ ?_
· simpa using huv G (by simp) (g ≫ Limits.prod.fst)
· simpa using huv H (by simp) (g ≫ Limits.prod.snd)
· simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ
rcases hZ with (rfl | rfl)
· simpa using huv (prod.lift g 0) =≫ Limits.prod.fst
· simpa using huv (prod.lift 0 g) =≫ Limits.prod.snd
