TerminatedStable

Statistics

Metric	Count
Definitions	0
Theorems `contsAux_stable_of_terminated`, `contsAux_stable_step_of_terminated`, `conts_stable_of_terminated`, `convs'Aux_stable_of_terminated`, `convs'Aux_stable_step_of_terminated`, `convs'_stable_of_terminated`, `convs_stable_of_terminated`, `dens_stable_of_terminated`, `nums_stable_of_terminated`, `terminated_stable`	10
Total	10

Name	Kind	Assumes	Proves	Validates	Depends On
`contsAux_stable_of_terminated` 📖	mathematical	`TerminatedAt`	`contsAux`	—	`Nat.le_induction` `contsAux_stable_step_of_terminated` `terminated_stable`
`contsAux_stable_step_of_terminated` 📖	mathematical	`TerminatedAt`	`contsAux`	—	`terminatedAt_iff_s_none`
`conts_stable_of_terminated` 📖	mathematical	`TerminatedAt`	`conts`	—	`contsAux_stable_of_terminated`
`convs'Aux_stable_of_terminated` 📖	mathematical	`Stream'.Seq.TerminatedAt` `Pair`	`convs'Aux`	—	`convs'Aux_stable_step_of_terminated` `Stream'.Seq.terminated_stable`
`convs'Aux_stable_step_of_terminated` 📖	mathematical	`Stream'.Seq.TerminatedAt` `Pair`	`convs'Aux`	—	`convs'Aux.eq_2`
`convs'_stable_of_terminated` 📖	mathematical	`TerminatedAt`	`convs'`	—	`convs'Aux_stable_of_terminated`
`convs_stable_of_terminated` 📖	mathematical	`TerminatedAt`	`convs`	—	`nums_stable_of_terminated` `dens_stable_of_terminated`
`dens_stable_of_terminated` 📖	mathematical	`TerminatedAt`	`dens`	—	`conts_stable_of_terminated`
`nums_stable_of_terminated` 📖	mathematical	`TerminatedAt`	`nums`	—	`conts_stable_of_terminated`
`terminated_stable` 📖	—	`TerminatedAt`	—	—	`Stream'.Seq.terminated_stable`

---