English
Two permutations on α extend a given permutation on a subset s if and only if their supports obey certain subset relations and their restricted forms match on s; more precisely, given hg: ∀ x, g x ∈ s ⇔ x ∈ s, the equality of extensions corresponds to a pair of conditions involving supports and restricted permutations.
Русский
Две перестановки на α являются расширениями перестановки на подмножестве s, если их опоры удовлетворяют определённым подмножественным отношениям и их ограничения совпадают на s.
LaTeX
$$$\text{Let } g,c: \operatorname{Perm}(\alpha),\; s\subseteq\alpha.\; (hg) : ∀x, g x ∈ s \iff x ∈ s.\; (ofSubtype (g.subtypePerm hg)) = c \iff c.\operatorname{support} \subseteq s \land \forall (hc' : ∀x, c x ∈ s \iff x ∈ s), c.subtypePerm hc' = g.subtypePerm hg.$$$
Lean4
/-- A permutation c is the extension of a restriction of g to s
iff its support is contained in s and its restriction is that of g -/
theorem ofSubtype_eq_iff {g c : Equiv.Perm α} {s : Finset α} (hg : ∀ x, g x ∈ s ↔ x ∈ s) :
ofSubtype (g.subtypePerm hg) = c ↔
c.support ≤ s ∧ ∀ (hc' : ∀ x, c x ∈ s ↔ x ∈ s), c.subtypePerm hc' = g.subtypePerm hg :=
by
simp only [Equiv.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]
constructor
· intro h
constructor
· intro a ha
by_contra ha'
rw [mem_support, ← h a, ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha'] at ha
exact ha rfl
· intro _ a ha
rw [← h a, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]
· rintro ⟨hc, h⟩ a
specialize h (isInvariant_of_support_le hc)
by_cases ha : a ∈ s
· rw [h a ha, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]
· rw [ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha, eq_comm, ← notMem_support]
exact Finset.notMem_mono hc ha
