ne_ones_iff — Mathlib

English

c ≠ ones n iff there exists i ∈ c.blocks with i > 1.

Русский

c ≠ ones n эквивалентно существованию элементов i > 1 в c.blocks.

LaTeX

$$$ c \\neq \\text{ones}(n) \\iff \\exists i \\in c.blocks, 1 < i $$$

Lean4

theorem ne_ones_iff {c : Composition n} : c ≠ ones n ↔ ∃ i ∈ c.blocks, 1 < i :=
  by
  refine (not_congr eq_ones_iff).trans ?_
  have : ∀ j ∈ c.blocks, j = 1 ↔ j ≤ 1 := fun j hj => by simp [le_antisymm_iff, c.one_le_blocks hj]
  simp +contextual [this]

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