mem_add — Mathlib

English

An element x belongs to the sum C1 + C2 iff x can be written as y + z with y ∈ C1 and z ∈ C2.

Русский

Элемент x принадлежит сумме C1 + C2 тогда и только тогда, когда x можно представить как y + z с y ∈ C1 и z ∈ C2.

LaTeX

$$x ∈ C_1 + C_2 \iff ∃ y ∈ C_1, ∃ z ∈ C_2, y + z = x$$

Lean4

@[simp]
theorem mem_add : x ∈ C₁ + C₂ ↔ ∃ y ∈ C₁, ∃ z ∈ C₂, y + z = x :=
  .rfl

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