prod_self_eq_iUnion_perm — Mathlib

English

Let f be a cycle-on s. Then the square s × s can be partitioned into shifted diagonals given by the cycle, i.e., s × s is the union over integers n of pairs (a, f^n(a)).

Русский

Пусть f — цикл на s. Тогда квадрат s × s распадается на диагонали, смещённые циклом: s × s = ⋃_{n∈ℤ} { (a, f^n(a)) : a∈s }.

LaTeX

$$$s\times s = \bigcup_{n \in \mathbb{Z}} \{ (a, f^n(a)) : a \in s \}$$$

Lean4

theorem prod_self_eq_iUnion_perm (hf : f.IsCycleOn s) : s ×ˢ s = ⋃ n : ℤ, (fun a => (a, (f ^ n) a)) '' s :=
  by
  ext ⟨a, b⟩
  simp only [Set.mem_prod, Set.mem_iUnion, Set.mem_image]
  refine ⟨fun hx => ?_, ?_⟩
  · obtain ⟨n, rfl⟩ := hf.2 hx.1 hx.2
    exact ⟨_, _, hx.1, rfl⟩
  · rintro ⟨n, a, ha, ⟨⟩⟩
    exact ⟨ha, (hf.1.perm_zpow _).mapsTo ha⟩

Похожие утверждения