mem_restrict — Mathlib

English

Summing over the boxes of the constructed prepartition equals summing over the original boxes with Option.elim' 0.

Русский

Суммирование по коробкам сконструированного предразмещения эквивалентно суммированию по исходным коробкам через Option.elim' 0.

LaTeX

$$$ \\sum_{J \\in (ofWithBot boxes le_of_mem pairwise_disjoint).boxes} f(J) = \\sum_{J \\in boxes} \\mathrm{Option.elim' } 0\\, f(J) $$$

Lean4

@[simp]
theorem mem_restrict : J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, (J₁ : WithBot (Box ι)) = ↑J ⊓ ↑J' := by simp [restrict, eq_comm]

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