one_le_mulConst

Mathlib.Combinatorics.Additive.DoublingConst

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

← MathLib Explorer

English

If t ⊆ s and u ⊆ s, then (∏ t) / (∏ u) ∈ mulSpan(s).

Русский

Если t ⊆ s и u ⊆ s, то (∏ t) / (∏ u) принадлежит mulSpan(s).

LaTeX

$$((\prod_{a\in t} a) / (\prod_{a\in u} a)) \in mulSpan(s) \quad (t \subseteq s, u \subseteq s)$$

Lean4

@[to_additive]
theorem one_le_mulConst (hA : A.Nonempty) (hB : B.Nonempty) : 1 ≤ σₘ[A, B] :=
  by
  rw [mulConst, one_le_div₀]
  · exact mod_cast card_le_card_mul_right hB
  · simpa

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

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

Разделы

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

Аффилиация

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