filter_ssubset — Mathlib

English

If s is a finite set, then s.filter p is a strict subset of s iff there exists an element in s that does not satisfy p.

Русский

Если s — конечное множество, то s.filter p является строгим подмножеством s тогда и только тогда, существует элемент в s, который не удовлетворяет p.

LaTeX

$$$s.filter p \\subset s \\iff \\exists x \\in s, \\neg p x$$$

Lean4

theorem filter_ssubset {s : Finset α} : s.filter p ⊂ s ↔ ∃ x ∈ s, ¬p x := by grind

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