sumElim_left

Mathlib.Topology.Constructions.SumProd

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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