setOf_subset_setOf — Mathlib

English

The inclusion relation between setOf predicates reduces to pointwise implication, i.e., setOf p ⊆ setOf q iff ∀ x, p x → q x.

Русский

Отношение включения между предикатами setOf сводится к поэлементному следованию: setOf p ⊆ setOf q тогда и только тогда, когда ∀x, p x → q x.

LaTeX

$$$\text{setOf } p \subseteq \text{setOf } q \iff \forall x, p x \rightarrow q x$$$

Lean4

@[simp]
theorem setOf_subset_setOf {p q : α → Prop} : {a | p a} ⊆ {a | q a} ↔ ∀ a, p a → q a :=
  Iff.rfl

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