subset_mul_left

Mathlib.Algebra.Group.Pointwise.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.subset_mul_left

← MathLib Explorer

English

If 1 ∈ t, then every element of t lies in s · t; i.e., t ⊆ s · t.

Русский

Если 1 ∈ t, то каждый элемент t принадлежит s · t; то есть t ⊆ s · t.

LaTeX

$$$$ t \\subseteq s * t \\quad\\text{if } 1 \\in t $$$$

Lean4

@[to_additive]
theorem subset_mul_left (s : Finset α) {t : Finset α} (ht : (1 : α) ∈ t) : s ⊆ s * t := fun a ha =>
  mem_mul.2 ⟨a, ha, 1, ht, mul_one _⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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