injective_splitCenterBox — Mathlib

English

The map I.splitCenterBox is injective; distinct center-sets yield distinct subboxes.

Русский

Отображение I.splitCenterBox инъективно; различные множества центров приводят к различным подкоробкам.

LaTeX

$$$$\text{Injective } I.splitCenterBox.$$$$

Lean4

theorem injective_splitCenterBox (I : Box ι) : Injective I.splitCenterBox := fun _ _ H ↦
  by_contra fun Hne ↦ (I.disjoint_splitCenterBox Hne).ne (nonempty_coe _).ne_empty (H ▸ rfl)

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