of_boundaryLE — Mathlib

English

Let e1 and e2 be complementary embeddings of complex shapes. If i1 lies on the left boundary of e1 (witness h), then the boundary relation at i1 with the indexOfBoundaryLE ac h holds in the ambient complex.

Русский

Пусть e1 и e2 — комплементарные вложения комплексных форм. Пусть i1 принадлежит левой границе e1 (существует свидетельство h); тогда отношение границы для i1 и индекса indexOfBoundaryLE ac h выполняется во внедрённом комплексе.

LaTeX

$$$ac.Boundary\\, i_1\\, (indexOfBoundaryLE\\, ac\\, h)$$$

Lean4

theorem of_boundaryLE {i₁ : ι₁} (h : e₁.BoundaryLE i₁) : ac.Boundary i₁ (indexOfBoundaryLE ac h) :=
  (exists₁ ac h).choose_spec

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