sumElim_right

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#Topology.IsEmbedding.sumElim_right

← MathLib Explorer

English

If Sum.elim f g is an embedding, then g is an embedding.

Русский

Если Sum.elim f g — вложение, то и g — вложение.

LaTeX

$$$\\text{IsEmbedding}(\\mathrm{Sum.elim}\ f\ g) \\Rightarrow \\text{IsEmbedding}(g)$$$

Lean4

/-- If `Sum.elim f g` is an embedding, then so is `g`. -/
theorem sumElim_right (h : IsEmbedding (Sum.elim f g)) : IsEmbedding g :=
  elim_comp_inr f g ▸ h.comp IsEmbedding.inr

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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