Forcing antichain (source code)

= Forcing antichain

A <subset> of a <forcing> order whose distinct members have no common stronger extension. A maximal <forcing antichain> has a compatible member for every condition. For <forcing> by nodes of a <set-theoretic tree>, ordered by extension, this coincides with a <tree antichain>.