mem_compPartialSumTarget_iff — Mathlib

English

The target set compPartialSumTarget_tendsto_prod_atTop asserts that the family of target sets grows to contain all compositions asymptotically; i.e., Tendsto of the target map to atTop holds.

Русский

Целевые множества compPartialSumTarget_tendsto_prod_atTop формируют асимптотическое включение всех композиций; то есть Tendsto этой карты к бесконечности.

LaTeX

$$$\\operatorname{Tendsto}_{\\toTop}(\\lambda p.\\mathrm{compPartialSumTarget}_{0} \\ p.1\\ p.2,\\; \\text{atTop},\\; \\text{atTop}).$$$

Lean4

@[simp]
theorem mem_compPartialSumTarget_iff {m M N : ℕ} {a : Σ n, Composition n} :
    a ∈ compPartialSumTarget m M N ↔ m ≤ a.2.length ∧ a.2.length < M ∧ ∀ j : Fin a.2.length, a.2.blocksFun j < N := by
  simp [compPartialSumTarget, compPartialSumTargetSet]

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