one_le_chainHeight_iff — Mathlib

English

1 ≤ s.chainHeight iff s is nonempty.

Русский

1 ≤ s.chainHeight тогда и только тогда, когда s непусто.

LaTeX

$$$ 1 \\le s.chainHeight \\iff s.Nonempty. $$$

Lean4

@[simp]
theorem one_le_chainHeight_iff : 1 ≤ s.chainHeight ↔ s.Nonempty :=
  by
  rw [← Nat.cast_one, Set.le_chainHeight_iff]
  simp only [length_eq_one_iff, @and_comm (_ ∈ _), @eq_comm _ _ [_], exists_exists_eq_and, singleton_mem_subchain_iff,
    Set.Nonempty]

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