isIdempotent_left — Mathlib

English

If gb is idempotent and Semiconj₂ f ga gb holds and f is injective, then ga is idempotent.

Русский

Если gb идемпотентна и Semiconj₂ f ga gb, и f инъективна, то ga идемпотентна.

LaTeX

$$$ \forall x,\ga x x = x $$$

Lean4

theorem isIdempotent_left [Std.IdempotentOp gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) : Std.IdempotentOp ga :=
  ⟨fun x ↦ h_inj <| by rw [h.eq, Std.IdempotentOp.idempotent (op := gb)]⟩

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