English
If f and g are cycles and the support of f is contained in the support of g, and f and g agree on all elements of f's support, then f equals g.
Русский
Если f и g — циклы и поддержка f ⊆ поддержка g, и f(x) = g(x) для всех x в поддержке f, то f = g.
LaTeX
$$$\\forall f,g:\\mathrm{Perm}(\\alpha),\\; \\mathrm{IsCycle}(f) \\land \\mathrm{IsCycle}(g) \\land f.\\mathrm{support} \\subseteq g.\\mathrm{support} \\land \\forall x \\in f.\\mathrm{support},\\; f x = g x \\Rightarrow f = g.$$$
Lean4
/-- Unlike `support_congr`, which assumes that `∀ (x ∈ g.support), f x = g x)`, here
we have the weaker assumption that `∀ (x ∈ f.support), f x = g x`. -/
theorem support_congr (hf : IsCycle f) (hg : IsCycle g) (h : f.support ⊆ g.support) (h' : ∀ x ∈ f.support, f x = g x) :
f = g :=
by
have : f.support = g.support := by
refine le_antisymm h ?_
intro z hz
obtain ⟨x, hx, _⟩ := id hf
have hx' : g x ≠ x := by rwa [← h' x (mem_support.mpr hx)]
obtain ⟨m, hm⟩ := hg.exists_pow_eq hx' (mem_support.mp hz)
have h'' : ∀ x ∈ f.support ∩ g.support, f x = g x :=
by
intro x hx
exact h' x (mem_of_mem_inter_left hx)
rwa [← hm, ← pow_eq_on_of_mem_support h'' _ x (mem_inter_of_mem (mem_support.mpr hx) (mem_support.mpr hx')),
pow_apply_mem_support, mem_support]
refine Equiv.Perm.support_congr h ?_
simpa [← this] using h'
