filter_const

Mathlib.Data.Finset.Filter

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

English

If p ≤ q (p implies q) then filtering by p is contained in filtering by q.

Русский

Если p следует q (p ⇒ q), то фильтрация по p подмножество фильтрации по q.

LaTeX

$$$s.filter p \\subseteq s.filter q \\text{ if } p \\le q$$$

Lean4

@[simp]
theorem filter_const (p : Prop) [Decidable p] (s : Finset α) : (s.filter fun _a => p) = if p then s else ∅ := by
  split_ifs <;> simp [*]

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

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

Разделы

Аффилиация

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