subset_setOf — Mathlib

English

The set of all elements x of α such that p x holds is a subset of s if and only if every x ∈ s satisfies p x.

Русский

Множество всех элементов x α с выполнением p x является подмножеством s тогда и только тогда, когда для каждого x ∈ s верно p x.

LaTeX

$$$s \subseteq {x \mid p x}$ эквивалентно ∀ x, x ∈ s → p x$$$

Lean4

theorem subset_setOf {p : α → Prop} {s : Set α} : s ⊆ setOf p ↔ ∀ x, x ∈ s → p x :=
  Iff.rfl

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