Boundary

Mathlib.Algebra.Homology.Embedding.AreComplementary

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

Lean4

/-- If `e₁` and `e₂` are complementary embeddings into a complex shape `c`,
indices `i₁` and `i₂` are at the boundary if `c.Rel (e₁.f i₁) (e₂.f i₂)`. -/
@[nolint unusedArguments]
def Boundary (_ : AreComplementary e₁ e₂) (i₁ : ι₁) (i₂ : ι₂) : Prop :=
  c.Rel (e₁.f i₁) (e₂.f i₂)

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

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

Разделы

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

Аффилиация

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