add_mem

Mathlib.Algebra.Algebra.Subalgebra.Basic

URI: https://scilib.ai/kg/mathlib#Subalgebra.add_mem

English

If x,y ∈ S, then x+y ∈ S.

Русский

Если x,y ∈ S, то x+y ∈ S.

LaTeX

$$$\forall x,y \in S,\ x+y \in S$$$

Lean4

protected theorem add_mem {x y : A} (hx : x ∈ S) (hy : y ∈ S) : x + y ∈ S :=
  add_mem hx hy

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru