one_le_divConst

Mathlib.Combinatorics.Additive.DoublingConst

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

← MathLib Explorer

English

If A and B are nonempty, then 1 ≤ σ_m[A,B].

Русский

Если A и B непустые, то 1 ≤ σ_m[A,B].

LaTeX

$$1 \leq \sigma_m[A,B] \quad (A\neq \emptyset, B\neq \emptyset)$$

Lean4

@[to_additive]
theorem one_le_divConst (hA : A.Nonempty) (hB : B.Nonempty) : 1 ≤ δₘ[A, B] :=
  by
  rw [← mulConst_inv_right]
  apply one_le_mulConst hA (by simpa)

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

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

Разделы

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

Аффилиация

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