subtype_eq_empty — Mathlib

English

For p : α → Prop decidable, s : Finset α, s.subtype p = ∅ iff for all x with p x, x ∉ s.

Русский

Пусть p : α → Prop решаемо. Тогда s.subtype p = ∅ тогда и только тогда, когда для всех x, удовлетворяющих p, x ∉ s.

LaTeX

$$s.subtype p = ∅ \\iff ∀ x, p x → x ∉ s$$

Lean4

theorem subtype_eq_empty {p : α → Prop} [DecidablePred p] {s : Finset α} : s.subtype p = ∅ ↔ ∀ x, p x → x ∉ s := by
  simp [Finset.ext_iff, Subtype.forall]

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