length_ne_zero — Mathlib

English

Length is nonzero iff the membership set is nontrivial, under irrefl.

Русский

Длина не ноль тогда и только тогда, когда множество элементов не тривиально, при иррефлексивности.

LaTeX

$$s.length ≠ 0 ↔ {x | x ∈ s}.Nontrivial$$

Lean4

theorem length_ne_zero [r.IsIrrefl] : s.length ≠ 0 ↔ {x | x ∈ s}.Nontrivial :=
  by
  refine
    ⟨fun h ↦ ⟨s 0, by simp [mem_def], s 1, by simp [mem_def], fun rid ↦ r.irrefl (s 0) ?_⟩,
      length_ne_zero_of_nontrivial⟩
  nth_rw 2 [rid]
  convert s.step ⟨0, by cutsat⟩
  ext
  simpa [Nat.pos_iff_ne_zero]

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