transitive — Mathlib

English

The relation “there exists an element that semiconjugates a to b” on a semigroup is transitive.

Русский

Отношение «существует элемент, который полусопрягает a к b» на полугруппе распадается транзитивно.

LaTeX

$$$$\text{Transitive } \big(\{a,b\},\exists c: SemiconjBy c a b\big).$$$$

Lean4

/-- The relation “there exists an element that semiconjugates `a` to `b`” on a semigroup
is transitive. -/
@[to_additive /-- The relation “there exists an element that semiconjugates `a` to `b`” on an
    additive semigroup is transitive. -/
    ]
protected theorem transitive : Transitive fun a b : S ↦ ∃ c, SemiconjBy c a b
  | _, _, _, ⟨x, hx⟩, ⟨y, hy⟩ => ⟨y * x, hy.mul_left hx⟩

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