Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-29 17:49 3ac9ae73

View on Github →

chore(data/stream): dedup take and approx (#10525) stream.take and stream.approx were propositionally equal. Merge them into one function stream.take; the definition comes from the old stream.approx.

Estimated changes

deleted theorem stream.length_take
deleted def stream.approx
modified def stream.take
deleted theorem stream.append_approx_drop
deleted theorem stream.approx_succ
deleted theorem stream.approx_zero
added theorem stream.length_take
deleted theorem stream.nth_approx
modified theorem stream.nth_inits
added theorem stream.nth_take_succ
added theorem stream.take_succ
modified theorem stream.take_theorem
added theorem stream.take_zero