English
Let c be a composition of n, j ∈ Fin n, i ∈ Fin (c.length). Then j lies in the range of the embedding c.embedding i if and only if the position is after the end of the previous blocks and before the end of the i-th block: c.sizeUpTo i ≤ j and j < c.sizeUpTo (i).succ.
Русский
Пусть c — композиция длины n, i ∈ Fin c.length, j ∈ Fin n. Тогда j принадлежит диапазону вложения c.embedding i тогда и только тогда, когда j находится в пределах i-й блока: c.sizeUpTo i ≤ j и j < c.sizeUpTo (i).succ.
LaTeX
$$$ j \\in \\mathrm{Set.range}(c.embedding i) \\iff c.sizeUpTo i \\le j \\land (j : \\mathbb{N}) < c.sizeUpTo (i : \\mathbb{N}).succ $$$
Lean4
theorem mem_range_embedding_iff {j : Fin n} {i : Fin c.length} :
j ∈ Set.range (c.embedding i) ↔ c.sizeUpTo i ≤ j ∧ (j : ℕ) < c.sizeUpTo (i : ℕ).succ :=
by
constructor
· intro h
rcases Set.mem_range.2 h with ⟨k, hk⟩
rw [Fin.ext_iff] at hk
dsimp at hk
rw [← hk]
simp [sizeUpTo_succ', k.is_lt]
· intro h
apply Set.mem_range.2
refine ⟨⟨j - c.sizeUpTo i, ?_⟩, ?_⟩
· rw [tsub_lt_iff_left, ← sizeUpTo_succ']
· exact h.2
· exact h.1
· rw [Fin.ext_iff]
exact add_tsub_cancel_of_le h.1
