English
For two-sided ideals I, J in a nonunital nonassociative ring, x ∈ I ⊔ J iff there exist y ∈ I, z ∈ J with y + z = x.
Русский
Для двухсторонних идеалов I, J в кольце без единицы, неассоциативном, элемент x принадлежит сумме I ⊔ J тогда и только тогда, когда существуют y ∈ I и z ∈ J такие, что y + z = x.
LaTeX
$$$x \\in I \\sqcup J \\iff \\exists y \\in I, \\exists z \\in J, y + z = x$$$
Lean4
theorem mem_sup {I J : TwoSidedIdeal R} {x : R} : x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x :=
by
constructor
· let s : TwoSidedIdeal R :=
.mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⟨0, ⟨zero_mem _, ⟨0, ⟨zero_mem _, zero_add _⟩⟩⟩⟩
(by rintro _ _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩ ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩;
exact ⟨x + a, ⟨add_mem _ hx ha, ⟨y + b, ⟨add_mem _ hy hb, by abel⟩⟩⟩⟩)
(by
rintro _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
exact ⟨-x, ⟨neg_mem _ hx, ⟨-y, ⟨neg_mem _ hy, by abel⟩⟩⟩⟩)
(by
rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
exact ⟨_, ⟨mul_mem_left _ _ _ hx, ⟨_, ⟨mul_mem_left _ _ _ hy, mul_add _ _ _ |>.symm⟩⟩⟩⟩)
(by
rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
exact ⟨_, ⟨mul_mem_right _ _ _ hx, ⟨_, ⟨mul_mem_right _ _ _ hy, add_mul _ _ _ |>.symm⟩⟩⟩⟩)
suffices (I.ringCon ⊔ J.ringCon) ≤ s.ringCon by intro h; convert this h; rw [rel_iff, sub_zero, mem_mk']; rfl
refine sup_le (fun x y h => ?_) (fun x y h => ?_) <;> rw [rel_iff] at h ⊢ <;> rw [mem_mk']
exacts [⟨_, ⟨h, ⟨0, ⟨zero_mem _, add_zero _⟩⟩⟩⟩, ⟨0, ⟨zero_mem _, ⟨_, ⟨h, zero_add _⟩⟩⟩⟩]
· rintro ⟨y, ⟨hy, ⟨z, ⟨hz, rfl⟩⟩⟩⟩; exact add_mem _ (mem_sup_left hy) (mem_sup_right hz)
