indexOfBoundaryGE

Mathlib.Algebra.Homology.Embedding.AreComplementary

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

Lean4

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

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

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

Разделы

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

Аффилиация

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