Theorems · Theorem · logic and foundations

Membership.mem.out

∀ {α : Type u} {a : α} {p : α → Prop}, a ∈ {x | p x} → p a

If h : a ∈ {x | p x} then h.out : p x. These are definitionally equal, but this can nevertheless be useful for various reasons, e.g. to apply further projection notation or in an argument to simp.

Defined in

Mathlib.Data.Set.Operations

Cited by

38 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms