splitCenterBoxEmb — Mathlib

English

The center-splitting operation can be packaged as an embedding, pairing the center-splitting map with its injectivity.

Русский

Операцию разбиения по центру можно оформить как вложение, сочетая отображение разбиения по центру с его инъективностью.

LaTeX

$$$$\text{SplitCenterBoxEmb}(I) : Set ι \hookrightarrow Box ι \quad\text{is an embedding}.$$$$

Lean4

/-- `BoxIntegral.Box.splitCenterBox` bundled as a `Function.Embedding`. -/
@[simps]
def splitCenterBoxEmb (I : Box ι) : Set ι ↪ Box ι :=
  ⟨splitCenterBox I, injective_splitCenterBox I⟩

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