mem_compPartialSumSource_iff — Mathlib

English

A pair i = (n, f) lies in compPartialSumSource(m,M,N) iff m ≤ n < M and ∀ a ∈ Fin n, 1 ≤ f(a) and f(a) < N.

Русский

Пара i = (n, f) принадлежит compPartialSumSource(m,M,N) тогда и только тогда, когда m ≤ n < M и ∀ a ∈ Fin n выполняется 1 ≤ f(a) < N.

LaTeX

$$$i \\in compPartialSumSource(m,M,N) \\iff (m \\le i.1 \\land i.1 < M) \\land \\forall a : Fin i.1, 1 \\le i.2 a \\land i.2 a < N$.$$

Lean4

@[simp]
theorem mem_compPartialSumSource_iff (m M N : ℕ) (i : Σ n, Fin n → ℕ) :
    i ∈ compPartialSumSource m M N ↔ (m ≤ i.1 ∧ i.1 < M) ∧ ∀ a : Fin i.1, 1 ≤ i.2 a ∧ i.2 a < N := by
  simp only [compPartialSumSource, Finset.mem_Ico, Fintype.mem_piFinset, Finset.mem_sigma]

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