mem_splitCenter — Mathlib

English

A box J lies in the center split of I if and only if there exists a center-split box s with J = I.splitCenterBox s.

Русский

Ящик J принадлежит центрированному разбиению I тогда и только тогда, когда существует центрально разбиенный ящик s с J = I.splitCenterBox s.

LaTeX

$$$ J \\in \\mathrm{splitCenter}(I) \\iff \\exists s,\\ I.\\mathrm{splitCenterBox}(s) = J $$$

Lean4

@[simp]
theorem mem_splitCenter : J ∈ splitCenter I ↔ ∃ s, I.splitCenterBox s = J := by simp [splitCenter]

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