divConst_le_card — Mathlib

English

Dense sets have small doubling: for any A,B, σ_m[A,B] ≤ A.dens^{-1}.

Русский

Плотные множества имеют маленькое удвоение: для любых A,B, σ_m[A,B] ≤ A.dens^{-1}.

LaTeX

$$\sigma_m[A,B] \leq A_{\text{dens}}^{-1}$$

Lean4

@[to_additive]
theorem divConst_le_card : δₘ[A, B] ≤ #B :=
  by
  obtain rfl | hA' := A.eq_empty_or_nonempty
  · simp
  rw [divConst, div_le_iff₀' (by positivity)]
  exact mod_cast card_div_le

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