mem_corner_iff_mem_range_mul_right

English

Let R be a semigroup and e an idempotent element. The corner e consists exactly of all elements that can be written as x e with x ranging over R. In particular, r belongs to corner(e) if and only if there exists x in R with r = x e.

Русский

Пусть R — полугруппа, а e — идемпотент. Уголок e состоит ровно из всех элементов, которые можно записать как x e, где x пробегает элементы R. То есть: r ∈ corner(e) тогда и только тогда, когда существует x ∈ R such that r = x e.

LaTeX

$$$\\forall r \\in R,\\, r \\in \\text{corner}(e) \\iff \\exists x \\in R,\\; r = x\,e.$$$

Lean4

theorem mem_corner_iff_mem_range_mul_right (hc : IsMulCentral e) {r : R} : r ∈ corner e ↔ r ∈ Set.range (· * e) := by
  simp_rw [mem_corner_iff_mem_range_mul_left idem hc, (hc.comm _).eq]

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