mul_add_subset

Mathlib.Algebra.Ring.Pointwise.Set

URI: https://scilib.ai/kg/mathlib#Set.mul_add_subset

English

For sets s,t,u in a distributive algebra, s * (t + u) ⊆ s * t + s * u.

Русский

Для множеств s,t,u в распределенной алгебре произведение s над t+u подмножество s*t + s*u.

LaTeX

$$$s * (t + u) \subseteq s * t + s * u$$$

Lean4

theorem mul_add_subset : s * (t + u) ⊆ s * t + s * u :=
  image2_distrib_subset_left mul_add

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

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

Разделы

Аффилиация

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