mem_split_iff — Mathlib

English

For any boxes I,J, and real x, a box J belongs to the split I i x exactly when J equals the lower piece I.splitLower i x or the upper piece I.splitUpper i x.

Русский

Для любых ящиков I и J и вещественного x выполнено: J принадлежит разбиению split I i x тогда и только тогда, когда J равен либо нижнему куску I.splitLower i x, либо верхнему куску I.splitUpper i x.

LaTeX

$$$J \\in \\mathrm{split}\\ I\\ i\\ x \\iff J = I.\\mathrm{splitLower}\\ i\\ x \\lor J = I.\\mathrm{splitUpper}\\ i\\ x$$

Lean4

@[simp]
theorem mem_split_iff : J ∈ split I i x ↔ ↑J = I.splitLower i x ∨ ↑J = I.splitUpper i x := by simp [split]

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