English
Given p, p' submodules, x ∈ p ⊔ p' iff there exist y ∈ p and z ∈ p' with y+z = x.
Русский
Пусть p и p' — подмодули. Тогда x принадлежит p ⊔ p' тогда и только тогда, когда существуют y ∈ p и z ∈ p' такие, что y+z = x.
LaTeX
$$$$ x \\in p \\; \\sqcup \\; p' \\iff \\exists y \\in p, \\exists z \\in p',\\ y+z = x. $$$$
Lean4
theorem mem_sup : x ∈ p ⊔ p' ↔ ∃ y ∈ p, ∃ z ∈ p', y + z = x :=
⟨fun h => by
rw [← span_eq p, ← span_eq p', ← span_union] at h
refine span_induction ?_ ?_ ?_ ?_ h
· rintro y (h | h)
· exact ⟨y, h, 0, by simp, by simp⟩
· exact ⟨0, by simp, y, h, by simp⟩
· exact ⟨0, by simp, 0, by simp⟩
· rintro _ _ - - ⟨y₁, hy₁, z₁, hz₁, rfl⟩ ⟨y₂, hy₂, z₂, hz₂, rfl⟩
exact
⟨_, add_mem hy₁ hy₂, _, add_mem hz₁ hz₂, by
rw [add_assoc, add_assoc, ← add_assoc y₂, ← add_assoc z₁, add_comm y₂]⟩
· rintro a - _ ⟨y, hy, z, hz, rfl⟩
exact ⟨_, smul_mem _ a hy, _, smul_mem _ a hz, by simp [smul_add]⟩,
by
rintro ⟨y, hy, z, hz, rfl⟩
exact add_mem ((le_sup_left : p ≤ p ⊔ p') hy) ((le_sup_right : p' ≤ p ⊔ p') hz)⟩
