English
For any i in compPartialSumTargetSet, there exist j in compPartialSumSource and orientation such that compChangeOfVariables maps j to i; i.e., the change of variables covers the target index by a corresponding source index.
Русский
Для любого i в compPartialSumTargetSet существует j в compPartialSumSource так, что compChangeOfVariables отображает j в i; смена переменных покрывает целевой индекс соответствующим источником.
LaTeX
$$$\\exists j\\in compPartialSumSource(m,M,N),\\; compChangeOfVariables(j, hj) = i.$$$
Lean4
theorem compPartialSumTargetSet_image_compPartialSumSource (m M N : ℕ) (i : Σ n, Composition n)
(hi : i ∈ compPartialSumTargetSet m M N) :
∃ (j : _) (hj : j ∈ compPartialSumSource m M N), compChangeOfVariables m M N j hj = i :=
by
rcases i with ⟨n, c⟩
refine ⟨⟨c.length, c.blocksFun⟩, ?_, ?_⟩
· simp only [compPartialSumTargetSet, Set.mem_setOf_eq] at hi
simp only [mem_compPartialSumSource_iff, hi.left, hi.right, true_and, and_true]
exact fun a => c.one_le_blocks' _
· dsimp [compChangeOfVariables]
rw [Composition.sigma_eq_iff_blocks_eq]
simp only [Composition.blocksFun]
conv_rhs => rw [← List.ofFn_get c.blocks]
