injective — Mathlib

English

For any a ∈ g.Basis and cycle factor c taken from g.cycleFactorsFinset, the cycleOf of a c equals c.

Русский

Для любого a ∈ g.Basis и цикла c, cycleOf(a c) = c.

LaTeX

$$$g.cycleOf (a c) = c$$$

Lean4

theorem injective : Function.Injective a := by
  intro c d h
  rw [← Subtype.coe_inj]
  apply g.cycleFactorsFinset_pairwise_disjoint.eq c.prop d.prop
  simp only [Disjoint, not_forall, not_or]
  use a c
  conv_rhs => rw [h]
  simp only [← Perm.mem_support, a.mem_support_self c, a.mem_support_self d, and_self]

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