ι_jointly_surjective

Mathlib.Topology.Category.CompHausLike.Limits

URI: https://scilib.ai/kg/mathlib#CompHausLike.finiteCoproduct.ι_jointly_surjective

Lean4

theorem ι_jointly_surjective (R : finiteCoproduct X) : ∃ (a : α) (r : X a), R = finiteCoproduct.ι X a r :=
  ⟨R.fst, R.snd, rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru