Subset_of_Set_with_Propositional_Function

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

mapping-theoryproofwikisubsets

Let $S$ be a set. Let $P: S \to \set {\text{true}, \text{false} }$ be a propositional function on $S$ . Then $\set {x \in S: \map P x} \subseteq S$

Preamble

import Mathlib.Data.Set.Basic

Formal statement

theorem Subset_of_Set_with_Propositional_Function {α : Type*} (S : Set α) (P : α → Prop) : {x ∈ S | P x} ⊆ S := by sorry

Source