mulConst_le_card

Mathlib.Combinatorics.Additive.DoublingConst

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

← MathLib Explorer

English

The doubling constant is at most the cardinality of B: σ_m[A,B] ≤ |B|.

Русский

Удвоительная константа не превосходит кардинальности множества B: σ_m[A,B] ≤ |B|.

LaTeX

$$\sigma_m[A,B] \leq |B|$$

Lean4

@[to_additive]
theorem mulConst_le_card : σₘ[A, B] ≤ #B :=
  by
  obtain rfl | hA' := A.eq_empty_or_nonempty
  · simp
  rw [mulConst, div_le_iff₀' (by positivity)]
  exact mod_cast card_mul_le

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

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

Разделы

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

Аффилиация

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