mem_filter_univ

Mathlib.Data.Fintype.Defs

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

English

For any predicate p, x belongs to univ.filter p iff p(x).

Русский

Для любого p: α → Prop, x ∈ univ.filter p эквивалентно p(x).

LaTeX

$$$$ x \in \mathrm{univ}.\mathrm{filter}(p) \iff p(x) $$$$

Lean4

theorem mem_filter_univ {p : α → Prop} [DecidablePred p] : ∀ x, x ∈ univ.filter p ↔ p x := by simp

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

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

Разделы

Аффилиация

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