Registry · Definition I.D31 established formalized

I.D31 — tau-Membership Relation

A in_tau B iff A | B (in the multiplicative structure on tau-Idx). Membership earned from divisibility; decidable, reflexive, antisymmetric. No ZFC axioms imported.

Book I Part 8 Ch. 32

Dependency Graph

Depends on (3)

I.D19a I.T09 I.T04

Depended on by (9)

I.D32 I.D33 I.D75 I.D94 I.L06 I.P10 I.P11 I.P12 I.P42

Lean Formalization

Module: TauLib.BookI.Sets.Membership

Symbol: Tau.Sets.tau_mem