rename_esymm — Mathlib

English

The esymm is symmetric under renaming: esymm is symmetric for all n.

Русский

Esymm симметрич по отношению к перестановкам: esymm симметричен для всех n.

LaTeX

$$$ IsSymmetric(\\text{esymm}(\\sigma,R,n)). $$$

Lean4

theorem rename_esymm (n : ℕ) (e : σ ≃ τ) : rename e (esymm σ R n) = esymm τ R n :=
  calc
    rename e (esymm σ R n) = ∑ x ∈ powersetCard n univ, ∏ i ∈ x, X (e i) := by
      simp_rw [esymm, map_sum, map_prod, rename_X]
    _ = ∑ t ∈ powersetCard n (univ.map e.toEmbedding), ∏ i ∈ t, X i := by
      simp [powersetCard_map, -map_univ_equiv, (mapEmbedding_apply)]
    _ = ∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i := by rw [map_univ_equiv]

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