Registry · Lemma I.L06 established formalized

I.L06 — Well-Foundedness of Membership

No infinite descending in_tau-chains: if A_1 in_tau A_2 in_tau ... with strict containment, the chain terminates (divisibility is well-founded above 1).

Book I Part 8 Ch. 34

Dependency Graph

Depends on (2)

I.D31 I.D33

Depended on by (1)

I.P12

Lean Formalization

Module: TauLib.BookI.Sets.Powerset

Symbol: Tau.Sets.tau_strict_mem_wf