English
Extending the domain of a permutation g along an embedding f : α ≃ Subtype p yields a permutation on β whose support is the image of g’s support under f.asEmbedding.
Русский
Расширение области определения перестановки g вдоль вложения f даёт перестановку на β; опора этой перестановки равна образу опоры g через вложение f.asEmbedding.
LaTeX
$$$\operatorname{supp}(g.\ extendDomain f) = \operatorname{map} f.asEmbedding (\operatorname{supp} g)$$$
Lean4
@[simp]
theorem support_extend_domain (f : α ≃ Subtype p) {g : Perm α} :
support (g.extendDomain f) = g.support.map f.asEmbedding :=
by
ext b
simp only [mem_map, Ne, mem_support]
by_cases pb : p b
· rw [extendDomain_apply_subtype _ _ pb]
constructor
· rintro h
refine ⟨f.symm ⟨b, pb⟩, ?_, by simp⟩
contrapose! h
simp [h]
· rintro ⟨a, ha, hb⟩
contrapose! ha
obtain rfl : a = f.symm ⟨b, pb⟩ := by
rw [eq_symm_apply]
exact Subtype.coe_injective hb
rw [eq_symm_apply]
exact Subtype.coe_injective ha
· rw [extendDomain_apply_not_subtype _ _ pb]
simp only [not_exists, false_iff, not_and, not_true]
rintro a _ rfl
exact pb (Subtype.prop _)
