isAssociative_left — Mathlib

English

If gb is associative and f is injective and f semiconjugates ga to gb, then ga is associative.

Русский

Если gb ассоциативна, f инъективна, и f полуприводит ga к gb, то ga ассоциативна.

LaTeX

$$$ \forall x,y,z,\ ga( ga(x,y), z) = ga(x, ga(y,z)) $$$

Lean4

theorem isAssociative_left [Std.Associative gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) : Std.Associative ga :=
  ⟨fun x₁ x₂ x₃ ↦ h_inj <| by simp only [h.eq, Std.Associative.assoc (op := gb)]⟩

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