conj' — Mathlib

English

If S is normal, then for all p and γ with γ ∈ S.arrows c c, the conjugation p γ inv p lies in S.arrows d d.

Русский

Если S нормальна, то для всех p и γ с γ ∈ S.arrows c c, конъюгация p γ inv p лежит в S.arrows d d.

LaTeX

$$∀ {c d} (p : d ⟶ c) {γ : c ⟶ c}, γ ∈ S.arrows c c → p ≫ γ ≫ Groupoid.inv p ∈ S.arrows d d$$

Lean4

theorem conj' {S : Subgroupoid C} (Sn : IsNormal S) :
    ∀ {c d} (p : d ⟶ c) {γ : c ⟶ c}, γ ∈ S.arrows c c → p ≫ γ ≫ Groupoid.inv p ∈ S.arrows d d := fun p γ hs => by
  convert Sn.conj (Groupoid.inv p) hs; simp

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