eqId_iff_len_le

Mathlib.AlgebraicTopology.SimplicialObject.Split

URI: https://scilib.ai/kg/mathlib#SimplicialObject.Splitting.IndexSet.eqId_iff_len_le

← MathLib Explorer

English

EqId ⇔ Δ.unop.len ≤ A.1.unop.len.

Русский

EqId ⇔ Δ.unop.len ≤ A.1.unop.len.

LaTeX

$$$A.\\mathrm{EqId} \\Leftrightarrow (\\Delta.\\mathrm{unop}).\\mathrm{len} \\le A.1.\\mathrm{unop}.\\mathrm{len}$$$

Lean4

theorem eqId_iff_len_le : A.EqId ↔ Δ.unop.len ≤ A.1.unop.len :=
  by
  rw [eqId_iff_len_eq]
  constructor
  · intro h
    rw [h]
  · exact le_antisymm (len_le_of_epi A.e)

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

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

Разделы

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

Аффилиация

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