eq_ones_iff — Mathlib

English

c = ones n iff for all i, i ∈ blocks implies i = 1.

Русский

c = ones n тогда и только тогда, когда каждый элемент блока равен 1.

LaTeX

$$$ c = \\text{ones}(n) \\iff \\forall i \\in c.blocks, i = 1 $$$

Lean4

theorem eq_ones_iff {c : Composition n} : c = ones n ↔ ∀ i ∈ c.blocks, i = 1 :=
  by
  constructor
  · rintro rfl
    exact fun i => eq_of_mem_replicate
  · intro H
    ext1
    have A : c.blocks = replicate c.blocks.length 1 := eq_replicate_of_mem H
    have : c.blocks.length = n := by
      conv_rhs => rw [← c.blocks_sum, A]
      simp
    rw [A, this, ones_blocks]

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