Documentation Verification Report

Init

📁 Source: Mathlib/Data/Stream/Init.lean

Statistics

MetricCount
DefinitionsIsBisimulation, instInhabited
2
Theoremsall_def, any_def, append_append_stream, append_eq_cons, append_left_injective, append_right_inj, append_right_injective, append_stream_head_tail, append_take, append_take_drop, bisim_simple, coinduction, composition, concat_take_get, cons_append_stream, cons_get_inits_core, cons_head_tail, cons_injective2, cons_injective_left, cons_injective_right, const_eq, corec'_eq, corec_def, corec_eq, corec_id_f_eq_iterate, corec_id_id_eq_const, cycle_eq, cycle_g_cons, cycle_singleton, dropLast_take, drop_append_of_le_length, drop_append_stream, drop_const, drop_drop, drop_map, drop_succ, drop_tail', drop_zero, drop_zip, enum_eq_zip, eq_of_bisim, eq_or_mem_of_mem_cons, eta, even_cons_cons, even_interleave, even_tail, exists_of_mem_map, ext, ext_iff, getElem?_take, getElem?_take_succ, get_append_left, get_append_length, get_append_right, get_cons_append_zero, get_const, get_drop, get_enum, get_even, get_inits, get_interleave_left, get_interleave_right, get_map, get_nats, get_odd, get_of_bisim, get_succ, get_succ_cons, get_succ_iterate, get_succ_iterate', get_tail, get_tails, get_unfolds_head_tail, get_zero_cons, get_zero_iterate, get_zip, head_cons, head_drop, head_even, head_iterate, head_map, head_zip, homomorphism, identity, inits_core_eq, inits_eq, inits_tail, interchange, interleave_eq, interleave_even_odd, interleave_tail_tail, iterate_eq, iterate_id, length_take, map_append_stream, map_cons, map_const, map_eq, map_eq_apply, map_id, map_iterate, map_map, map_tail, map_take, mem_append_stream_left, mem_append_stream_right, mem_cons, mem_cons_of_mem, mem_const, mem_cycle, mem_iff_exists_get_eq, mem_interleave_left, mem_interleave_right, mem_map, mem_of_get_eq, mem_of_mem_even, mem_of_mem_odd, nats_eq, nil_append_stream, odd_eq, tail_cons, tail_const, tail_drop, tail_drop', tail_eq_drop, tail_even, tail_inits, tail_interleave, tail_iterate, tail_map, tail_zip, tails_eq, tails_eq_iterate, take_add, take_append_of_le_length, take_drop, take_get, take_prefix, take_prefix_take_left, take_succ, take_succ', take_succ_cons, take_take, take_theorem, take_zero, unfolds_eq, unfolds_head_eq, zip_eq, zip_inits_tails
149
Total151

Stream'

Definitions

NameCategoryTheorems
IsBisimulation 📖MathDef
instInhabited 📖CompOp

Theorems

NameKindAssumesProvesValidatesDepends On
all_def 📖mathematicalAll
any_def 📖mathematicalAny
get
append_append_stream 📖mathematicalappendStream'cons_append_stream
append_eq_cons 📖mathematicalappendStream'
cons
append_left_injective 📖appendStream'get_append_left
append_right_inj 📖mathematicalappendStream'append_right_injective
append_right_injective 📖appendStream'ext
get_append_right
append_stream_head_tail 📖mathematicalappendStream'
head
tail
eta
append_take 📖mathematicaltake
appendStream'
append_take_drop 📖mathematicalappendStream'
take
drop
take_succ
drop_succ
cons_append_stream
eta
bisim_simple 📖head
tail
eq_of_bisim
coinduction 📖head
tail
eq_of_bisim
composition 📖mathematicalapply
pure
concat_take_get 📖mathematicaltake
get
take_succ'
cons_append_stream 📖mathematicalappendStream'
cons
cons_get_inits_core 📖mathematicalget
initsCore
get_succ
inits_core_eq
tail_cons
cons_head_tail 📖mathematicalcons
head
tail
eta
cons_injective2 📖mathematicalFunction.Injective2
Stream'
cons
get_zero_cons
ext
get_succ_cons
cons_injective_left 📖mathematicalStream'
cons
Function.Injective2.left
cons_injective2
cons_injective_right 📖mathematicalStream'
cons
Function.Injective2.right
cons_injective2
const_eq 📖mathematicalconst
cons
ext
corec'_eq 📖mathematicalcorec'
cons
corec_eq
corec_def 📖mathematicalmap
iterate
corec_eq 📖mathematicalconscorec_def
map_eq
head_iterate
tail_iterate
corec_id_f_eq_iterate 📖mathematicaliterate
corec_id_id_eq_const 📖mathematicalconstcorec_def
map_id
iterate_id
cycle_eq 📖mathematicalcycle
appendStream'
corec_eq
cycle_g_cons
cycle_g_cons 📖mathematicalcycleG
cycle_singleton 📖mathematicalcycle
const
coinduction
cycle_eq
const_eq
dropLast_take 📖mathematicaltaketake_succ'
drop_append_of_le_length 📖mathematicaldrop
appendStream'
ext
lt_or_ge
get_drop
get_append_left
get_append_right
drop_append_stream 📖mathematicaldrop
appendStream'
drop_succ
cons_append_stream
tail_cons
drop_const 📖mathematicaldrop
const
ext
drop_drop 📖mathematicaldropext
get_drop
drop_map 📖mathematicaldrop
map
ext
drop_succ 📖mathematicaldrop
tail
drop_tail' 📖mathematicaldrop
tail
drop_zero 📖mathematicaldrop
drop_zip 📖mathematicaldrop
zip
ext
enum_eq_zip 📖mathematicalenum
zip
nats
eq_of_bisim 📖IsBisimulationext
get_of_bisim
eq_or_mem_of_mem_cons 📖Stream'
instMembership
cons
tail_cons
get_succ
eta 📖mathematicalcons
head
tail
even_cons_cons 📖mathematicaleven
cons
corec_eq
even_interleave 📖mathematicaleven
interleave
eq_of_bisim
interleave_eq
even_cons_cons
tail_cons
even_tail 📖mathematicaleven
tail
odd
exists_of_mem_map 📖Stream'
instMembership
map
ext 📖get
ext_iff 📖mathematicalgetext
getElem?_take 📖mathematicaltake
get
length_take
take_succ
get_succ
getElem?_take_succ 📖mathematicaltake
get
getElem?_take
get_append_left 📖mathematicalget
appendStream'
get_append_length 📖mathematicalget
appendStream'
get_append_right
get_append_right 📖mathematicalget
appendStream'
get_cons_append_zero 📖mathematicalget
appendStream'
get_const 📖mathematicalget
const
get_drop 📖mathematicalget
drop
get_enum 📖mathematicalget
enum
get_even 📖mathematicalget
even
get_succ
tail_even
get_inits 📖mathematicalget
inits
take
get_succ
take_succ
tail_inits
inits_tail
cons_get_inits_core
get_interleave_left 📖mathematicalget
interleave
get_succ
interleave_eq
tail_cons
get_interleave_right 📖mathematicalget
interleave
get_succ
interleave_eq
tail_cons
get_map 📖mathematicalget
map
get_nats 📖mathematicalget
nats
get_odd 📖mathematicalget
odd
odd_eq
get_even
get_of_bisim 📖mathematicalIsBisimulationget
drop
get_succ 📖mathematicalget
tail
get_succ_cons 📖mathematicalget
cons
get_succ_iterate 📖mathematicalget
iterate
get_succ
tail_iterate
get_succ_iterate' 📖mathematicalget
iterate
get_tail 📖mathematicalget
tail
get_tails 📖mathematicalget
Stream'
tails
drop
tail
get_succ
drop_succ
tails_eq
tail_cons
get_unfolds_head_tail 📖mathematicalget
unfolds
Stream'
head
tail
get_succ
unfolds_eq
tail_cons
get_zero_cons 📖mathematicalget
cons
get_zero_iterate 📖mathematicalget
iterate
get_zip 📖mathematicalget
zip
head_cons 📖mathematicalhead
cons
head_drop 📖mathematicalhead
drop
get
get_drop
head_even 📖mathematicalhead
even
head_iterate 📖mathematicalhead
iterate
head_map 📖mathematicalhead
map
head_zip 📖mathematicalhead
zip
homomorphism 📖mathematicalapply
pure
identity 📖mathematicalapply
pure
inits_core_eq 📖mathematicalinitsCore
cons
head
tail
corec_eq
inits_eq 📖mathematicalinits
cons
head
map
tail
ext
get_inits
get_succ
tail_cons
get_map
inits_tail 📖mathematicalinits
tail
initsCore
head
interchange 📖mathematicalapply
pure
interleave_eq 📖mathematicalinterleave
cons
head
tail
corec_eq
interleave_even_odd 📖mathematicalinterleave
even
odd
eq_of_bisim
tail_interleave
tail_even
interleave_tail_tail 📖mathematicalinterleave
tail
interleave_eq
iterate_eq 📖mathematicaliterate
cons
eta
tail_iterate
iterate_id 📖mathematicaliterate
const
coinduction
tail_iterate
tail_const
length_take 📖mathematicaltake
map_append_stream 📖mathematicalmap
appendStream'
cons_append_stream
map_cons
map_cons 📖mathematicalmap
cons
eta
map_eq
map_const 📖mathematicalmap
const
map_eq 📖mathematicalmap
cons
head
tail
eta
tail_map
head_map
map_eq_apply 📖mathematicalmap
apply
pure
map_id 📖mathematicalmap
map_iterate 📖mathematicaliterate
map
iterate.eq_def
iterate.eq_2
get.eq_1
map.eq_1
map_map 📖mathematicalmap
map_tail 📖mathematicalmap
tail
map_take 📖mathematicaltake
map
length_take
take_get
mem_append_stream_left 📖mathematicalStream'
instMembership
appendStream'
mem_cons_of_mem
mem_append_stream_right 📖mathematicalStream'
instMembership
appendStream'mem_cons_of_mem
mem_cons 📖mathematicalStream'
instMembership
cons
mem_cons_of_mem 📖mathematicalStream'
instMembership
consget_succ
tail_cons
mem_const 📖mathematicalStream'
instMembership
const
mem_cycle 📖mathematicalStream'
instMembership
cycle
cycle_eq
mem_append_stream_left
mem_iff_exists_get_eq 📖mathematicalStream'
instMembership
get
mem_of_get_eq
mem_interleave_left 📖mathematicalStream'
instMembership
interleaveget_interleave_left
mem_interleave_right 📖mathematicalStream'
instMembership
interleaveget_interleave_right
mem_map 📖mathematicalStream'
instMembership
mapget_map
mem_of_get_eq 📖mathematicalgetStream'
instMembership
mem_of_mem_even 📖Stream'
instMembership
even
get_even
mem_of_mem_odd 📖Stream'
instMembership
odd
get_odd
nats_eq 📖mathematicalnats
cons
map
ext
get_succ
nil_append_stream 📖mathematicalappendStream'
odd_eq 📖mathematicalodd
even
tail
tail_cons 📖mathematicaltail
cons
tail_const 📖mathematicaltail
const
const_eq
tail_drop 📖mathematicaltail
drop
tail_drop'
tail_drop' 📖mathematicaltail
drop
ext
get_drop
tail_eq_drop 📖mathematicaltail
drop
tail_even 📖mathematicaltail
even
corec_eq
tail_inits 📖mathematicaltail
inits
initsCore
head
inits_core_eq
tail_interleave 📖mathematicaltail
interleave
corec_eq
tail_iterate 📖mathematicaltail
iterate
ext
get_tail
get_succ_iterate'
tail_map 📖mathematicaltail
map
tail_zip 📖mathematicaltail
zip
tails_eq 📖mathematicaltails
cons
Stream'
tail
corec_eq
tails_eq_iterate 📖mathematicaltails
iterate
Stream'
tail
take_add 📖mathematicaltake
drop
append_left_injective
append_take_drop
append_append_stream
length_take
take_append_of_le_length 📖mathematicaltake
appendStream'
length_take
take_get
get_append_left
take_drop 📖mathematicaltake
drop
length_take
take_get
get_drop
take_get 📖mathematicaltakegetappend_take_drop
get_append_left
take_prefix 📖mathematicaltakelength_take
take_prefix_take_left
take_prefix_take_left 📖mathematicaltaketake_take
take_succ 📖mathematicaltake
head
tail
take_succ' 📖mathematicaltake
get
take_succ
get_tail
take_succ_cons 📖mathematicaltake
cons
take_take 📖mathematicaltaketake_zero
take_succ
take_theorem 📖takeext
getElem?_take_succ
take_zero 📖mathematicaltake
unfolds_eq 📖mathematicalunfolds
cons
corec_eq
unfolds_head_eq 📖mathematicalunfolds
Stream'
head
tail
ext
get_unfolds_head_tail
zip_eq 📖mathematicalzip
cons
head
tail
eta
zip_inits_tails 📖mathematicalzip
Stream'
appendStream'
inits
tails
const
ext
get_inits
get_tails
append_take_drop

---

← Back to Index