indexOfBoundaryLE

Mathlib.Algebra.Homology.Embedding.AreComplementary

URI: https://scilib.ai/kg/mathlib#ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryLE

Lean4

/-- If `ac : AreComplementary e₁ e₂` (with `e₁ : ComplexShape.Embedding c₁ c` and
`e₂ : ComplexShape.Embedding c₂ c`), and `i₁` belongs to `e₁.BoundaryLE`,
then this is the (unique) index `i₂` of `c₂` such that `ac.Boundary i₁ i₂`. -/
noncomputable def indexOfBoundaryLE {i₁ : ι₁} (h : e₁.BoundaryLE i₁) : ι₂ :=
  (exists₁ ac h).choose

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

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

Разделы

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

Аффилиация

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