Registry · Proposition I.P10 established formalized

I.P10 — Membership Decidability

The tau-membership relation is decidable: given A, B in tau-Idx, we can computably determine whether A in_tau B.

Book I Part 8 Ch. 32

Dependency Graph

Depends on (2)

I.D31 I.D19a

Lean Formalization

Module: TauLib.BookI.Sets.Membership

Symbol: Tau.Sets.instDecidableTauMem