setOf_subset — Mathlib

English

The subset relation between setOf p and s is equivalent to the universal statement that every x with p x lies in s.

Русский

Отношение подмножества между setOf p и s эквивалентно всеобщему утверждению, что каждый x с p x принадлежит s.

LaTeX

$$$setOf p \subseteq s \iff \forall x, p x \rightarrow x \in s$$$

Lean4

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

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