mem_sup' — Mathlib

English

For submodules p, p', x ∈ p ⊔ p' iff ∃ (y : p) (z : p'), (y : M) + z = x.

Русский

Для подподмодулей p, p' и x, x ∈ p ⊔ p' тогда и только тогда, когда существует y в p и z в p', такие что (y : M) + z = x.

LaTeX

$$$$ x \\in p \\sqcup p' \\iff \\exists (y: p) (z: p'), (y : M) + z = x. $$$$

Lean4

theorem mem_sup' : x ∈ p ⊔ p' ↔ ∃ (y : p) (z : p'), (y : M) + z = x :=
  mem_sup.trans <| by simp only [Subtype.exists, exists_prop]

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