mem_corner_iff_mem_range_mul_left

English

Equality of membership to the corner is equivalent to membership in the range of multiplication by e.

Русский

Членство в углу эквивалентно членству в образе умножения на e.

LaTeX

$$$r \\in corner e \\iff r \\in \\{ e x : x \\in R \\}$$$

Lean4

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

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