rename — Mathlib

English

If φ is symmetric, then for any equivalence e, rename e φ is symmetric.

Русский

Если φ симметричен, то для любой эквивалентности e переименование rename e φ симметрично.

LaTeX

$$∀ e, (rename e φ).IsSymmetric$$

Lean4

protected theorem rename (hφ : φ.IsSymmetric) (e : σ ≃ τ) : (rename e φ).IsSymmetric := fun _ =>
  by
  apply rename_injective _ e.symm.injective
  simp_rw [rename_rename, ← Equiv.coe_trans, Equiv.self_trans_symm, Equiv.coe_refl, rename_id_apply]
  rw [hφ]

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