instDecidablePred — Mathlib

English

There exists a decidable predicate for Finset.Nontrivial; i.e., the property of being nontrivial is decidable for Finsets.

Русский

Существует разрешимый предикат для свойства Finset.Nontrivial; то есть не-trivialность Finset допускает решение.

LaTeX

$$DecidablePred (Finset.Nontrivial (α := α))$$

Lean4

instance instDecidablePred : DecidablePred (Finset.Nontrivial (α := α)) :=
  fun s =>
    /-
      We don't use `Finset.one_lt_card_iff_nontrivial`
      because `Finset.card` is defined in a different file.
      -/

  Quotient.recOnSubsingleton (motive := fun (s : Multiset α) => (h : s.Nodup) → Decidable (Finset.Nontrivial ⟨s, h⟩))
    s.val
    (fun l h =>
      match l with
      | [] => isFalse (by simp)
      | [_] => isFalse (by simp [Finset.toSet])
      | a :: b :: _ => isTrue ⟨a, by simp, b, by simp, List.ne_of_not_mem_cons (List.nodup_cons.mp h).left⟩)
    s.nodup

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