feat(Data): Results about RelatesInSteps with bounds on the reachable set - #779

Open

crei wants to merge 13 commits into

leanprover:mainfrom

crei:relates_in_steps_bounded

Commits on Aug 6, 2026

Results about reachability with repeated visits.
crei
committed
cce51a6

Commits on Aug 12, 2026

Use isChain.
crei
committed
c462faa
Merge remote-tracking branch 'origin/main' into relates_in_steps_bounded
crei
committed
dea453a
Extract a lemma and clean up.
crei
committed
877f6d5
Undo some golfing.
crei
committed
ba0c2b5
Undo some more golfing.
crei
committed
cd5c63f

Commits on Aug 17, 2026

Extract results related to List.isChain into their own file.
crei
committed
c4c92c1
Merge remote-tracking branch 'origin/main' into relates_in_steps_bounded
crei
committed
9ec5246
Minor tweaks.
crei
committed
af70d3b
Remove simp.
crei
committed
f03aca6

Commits on Aug 19, 2026

Merge remote-tracking branch 'origin/main' into relates_in_steps_bounded
crei
committed
a54f681

Commits on Aug 20, 2026

Move file.
crei
committed
f85d8ed
Review comments.
crei
committed
bd393f3