mem_sup — Mathlib

English

For any x in M, x belongs to the supremum N ⊔ N' iff there exist y ∈ N and z ∈ N' with y + z = x.

Русский

Для любого x ∈ M верно: x ∈ N ⊔ N' тогда и только тогда существует y ∈ N, z ∈ N' такие, что y + z = x.

LaTeX

$$x \\in N \\sqcup N' \\\\iff \\\\ \\exists y \\in N, \\exists z \\in N',\\; y + z = x$$

Lean4

theorem mem_sup (x : M) : x ∈ N ⊔ N' ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x := by
  rw [← mem_toSubmodule, sup_toSubmodule, Submodule.mem_sup]; exact Iff.rfl

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