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

Merged

fmontesi merged 24 commits into

leanprover:mainfrom

crei:relates_in_steps_bounded

Aug 27, 2026

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

Commits on Aug 25, 2026

Update Cslib/Foundations/Data/List/IsChainFromTo.lean

crei
and
thomaskwaring
authored
6f018c3
Fix and apply suggestions.
crei
committed
cdff1ee
Update Cslib/Foundations/Data/List/IsChainFromTo.lean

crei
and
thomaskwaring
authored
ca19e4f
Review comments and many more lemmas.
crei
committed
9d1ea10
Cleanup.
crei
committed
d66f76a
Add some more grind lemmas and update the module docstring.
crei
committed
4f2cd1b
Merge remote-tracking branch 'origin/main' into relates_in_steps_bounded
crei
committed
a2505e4

Commits on Aug 26, 2026

Move into List namespace, review suggestions
crei
committed
2a892a1

Commits on Aug 27, 2026

Update Cslib/Foundations/Data/List/IsChainFromTo.lean

crei
and
chenson2018
authored
6833eb1
Update Cslib/Foundations/Data/List/IsChainFromTo.lean

crei
and
chenson2018
authored
3ecf3e0
Update Cslib/Foundations/Data/List/IsChainFromTo.lean

crei
and
chenson2018
authored
da3cec4