filter_true_of_mem

Mathlib.Data.Finset.Filter

URI: https://scilib.ai/kg/mathlib#Finset.filter_true_of_mem

← MathLib Explorer

English

If no element of s satisfies p, then s.filter p is the empty set.

Русский

Если ни один элемент s не удовлетворяет p, то s.filter p — пустое множество.

LaTeX

$$$\\forall x \\in s, \\neg p x \\Rightarrow s.filter p = \\emptyset$$$

Lean4

/-- If all elements of a `Finset` satisfy the predicate `p`, `s.filter p` is `s`. -/
theorem filter_true_of_mem (h : ∀ x ∈ s, p x) : s.filter p = s :=
  filter_eq_self.2 h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru