English
Define snoc to append the element a to an embedding x: Fin n ↪ ofStabilizer G a, yielding an embedding Fin (n+1) ↪ α.
Русский
Определим snoc как операцию добавления элемента a к концу отображения x: Fin n ↪ ofStabilizer G a, получая отображение Fin (n+1) ↪ α.
LaTeX
$$$\\mathrm{snoc} : (\\mathrm{Fin}\\, n \\hookrightarrow \\mathrm{ofStabilizer}(G,a)) \\to (\\mathrm{Fin}\\,(n+1) \\hookrightarrow \\alpha).$$$
Lean4
/-- Append `a` to `x : Fin n ↪ ofStabilizer G a` to get an element of `Fin n.succ ↪ α`. -/
@[to_additive /-- Append `a` to `x : Fin n ↪ ofStabilizer G a` to get an element of `Fin n.succ ↪ α`. -/
]
def snoc {n : ℕ} (x : Fin n ↪ ofStabilizer G a) : Fin n.succ ↪ α :=
Fin.Embedding.snoc (x.trans (subtype _)) (a := a)
(by
simp [Set.mem_range, trans_apply, not_exists]
exact fun i ↦ (x i).prop)
