of_boundaryGE — Mathlib

English

Let e1 and e2 be complementary embeddings. If i2 lies on the right boundary given by e2 (witness h), then ac.Boundary (indexOfBoundaryGE ac h) i2 holds.

Русский

Пусть e1 и e2 — комплементарные вложения. Пусть i2 принадлежит правой границе, задаваемой e2 (существует свид-во h); тогда выполняется ac.Boundary (indexOfBoundaryGE ac h) i2.

LaTeX

$$$ac.Boundary\\, (indexOfBoundaryGE\\, ac\\, h)\\, i_2$$$

Lean4

theorem of_boundaryGE {i₂ : ι₂} (h : e₂.BoundaryGE i₂) : ac.Boundary (indexOfBoundaryGE ac h) i₂ :=
  (exists₂ ac h).choose_spec

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