mem_boundaries_iff_exists_blocks_sum_take_eq

English

A boundary value j occurs if and only if there exists an index i with i < card(boundaries) such that the sum of the first i blocks equals j.

Русский

Граница j встречается тогда и только тогда, когда существует индекс i < card(boundaries), для которого сумма первых i блоков равна j.

LaTeX

$$$j\\in c.boundaries\\ \\Leftrightarrow\\ \\exists i

Lean4

theorem mem_boundaries_iff_exists_blocks_sum_take_eq {j : Fin (n + 1)} : j ∈ c.boundaries ↔ ∃ i < c.boundaries.card, (c.blocks.take i).sum = j := by constructor · intro hj rcases (c.boundaries.orderIsoOfFin rfl).surjective ⟨j, hj⟩ with ⟨i, hi⟩ rw [Subtype.ext_iff, Subtype.coe_mk] at hi refine ⟨i.1, i.2, ?_⟩ dsimp at hi rw [← hi, c.blocks_partial_sum i.2] rfl · rintro ⟨i, hi, H⟩ convert (c.boundaries.orderIsoOfFin rfl ⟨i, hi⟩).2 have : c.boundary ⟨i, hi⟩ = j := by rwa [Fin.ext_iff, ← c.blocks_partial_sum hi] exact this.symm

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