coe_filter_univ — Mathlib

English

The coercion of a filtered univ to a set equals the set of elements satisfying the predicate: (univ.filter p : Set α) = {x | p x}.

Русский

Приведение отфильтрованного универсума к множеству дает множество элементов, удовлетворяющих предикату.

LaTeX

$$$ (univ.filter p : Set\\, \\alpha) = \\{x \\mid p x\\} $$$

Lean4

theorem coe_filter_univ (p : α → Prop) [DecidablePred p] : (univ.filter p : Set α) = {x | p x} := by simp

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