English
Append operations stitch finite enumerations of fixing subgroups via embeddings.
Русский
Операции дополнения объединяют конечные перечисления фиксационных подгрупп через вложения.
LaTeX
$$$\text{append}: \text{Fin } n \hookrightarrow \text{FixSubgroup}(M,s) \to \text{Fin } (|s|+n) \hookrightarrow \alpha$$$
Lean4
/-- Append `Fin m ↪ ofFixingSubgroup M s` at the end of an enumeration of `s`. -/
@[to_additive /-- Append `Fin m ↪ ofFixingSubgroup M s` at the end of an enumeration of `s`. -/
]
noncomputable def append {n : ℕ} [Finite s] (x : Fin n ↪ ofFixingSubgroup M s) : Fin (s.ncard + n) ↪ α :=
by
have : Nonempty (Fin (s.ncard) ≃ s) := Finite.card_eq.mp (by simp [Nat.card_coe_set_eq])
let y := (Classical.choice this).toEmbedding
apply Fin.Embedding.append (x := y.trans (subtype _)) (y := x.trans (subtype _))
rw [Set.disjoint_iff_forall_ne]
rintro _ ⟨j, rfl⟩ _ ⟨i, rfl⟩ H
apply (x i).prop
simp only [trans_apply, Function.Embedding.subtype_apply] at H
simpa [H] using Subtype.coe_prop (y j)
