English
For any finite m,n and a permutation on m ⊕ n, the map preserves the left block iff it preserves the right block.
Русский
Для любой перестановки на m ⊕ n сохранение левого блока эквивалентно сохранению правого блока.
LaTeX
$$$\\forall {m n : \\mathrm{Type}*} [\\mathrm{Finite}~m] [\\mathrm{Finite}~n] (\\sigma : \\mathrm{Perm}(m \\oplus n)) \; \n \\mathrm{MapsTo}(\\sigma, \\mathrm{range}(\\mathrm{Sum}.inl), \\mathrm{range}(\\mathrm{Sum}.inl)) \\; \\Leftrightarrow \\; \n \\mathrm{MapsTo}(\\sigma, \\mathrm{range}(\\mathrm{Sum}.inr), \\mathrm{range}(\\mathrm{Sum}.inr))$$$
Lean4
theorem perm_mapsTo_inl_iff_mapsTo_inr {m n : Type*} [Finite m] [Finite n] (σ : Perm (m ⊕ n)) :
Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo σ (Set.range Sum.inr) (Set.range Sum.inr) :=
by
constructor <;>
( intro h
classical
rw [← perm_inv_mapsTo_iff_mapsTo] at h
intro x
rcases hx : σ x with l | r)
· rintro ⟨a, rfl⟩
obtain ⟨y, hy⟩ := h ⟨l, rfl⟩
rw [← hx, σ.inv_apply_self] at hy
exact absurd hy Sum.inl_ne_inr
· rintro _; exact ⟨r, rfl⟩
· rintro _; exact ⟨l, rfl⟩
· rintro ⟨a, rfl⟩
obtain ⟨y, hy⟩ := h ⟨r, rfl⟩
rw [← hx, σ.inv_apply_self] at hy
exact absurd hy Sum.inr_ne_inl
