Relation

📁 Source: Mathlib/Data/WSeq/Relation.lean

Statistics

Metric	Count
Definitions `BisimO`, `LiftRel`, `LiftRelO`, `«term_~ʷ_»`	4
Theorems `imp`, `equivalence`, `ext`, `refl`, `trans`, `equiv`, `refl`, `swap`, `swap_lem`, `trans`, `imp`, `imp_right`, `swap`, `bind_assoc`, `bind_assoc_comp`, `bind_congr`, `bind_ret`, `cons_congr`, `destruct_congr`, `destruct_congr_iff`, `dropn_congr`, `exists_of_liftRel_left`, `exists_of_liftRel_right`, `flatten_congr`, `flatten_equiv`, `get?_congr`, `head_congr`, `join_append`, `join_congr`, `join_join`, `join_map_ret`, `join_ret`, `liftRel_append`, `liftRel_bind`, `liftRel_cons`, `liftRel_destruct`, `liftRel_destruct_iff`, `liftRel_dropn_destruct`, `liftRel_flatten`, `liftRel_join`, `lem`, `liftRel_map`, `liftRel_nil`, `liftRel_think_left`, `liftRel_think_right`, `map_congr`, `mem_congr`, `ret_bind`, `tail_congr`, `think_congr`, `think_equiv`	51
Total	55

Stream'.WSeq

Definitions

Name	Category	Theorems
`BisimO` 📖	MathDef	3 math math: `BisimO.imp`, `destruct_congr_iff`, `destruct_congr`
`LiftRel` 📖	MathDef	18 math math: `liftRel_destruct`, `liftRel_join`, `liftRel_map`, `liftRel_cons`, `LiftRel.equiv`, `liftRel_append`, `liftRel_bind`, `LiftRel.refl`, `liftRel_nil`, `liftRel_think_right`, `liftRel_destruct_iff`, `LiftRel.symm`, `liftRel_flatten`, `liftRel_dropn_destruct`, `liftRel_think_left`, `LiftRel.swap`, `LiftRel.swap_lem`, `LiftRel.trans`
`LiftRelO` 📖	MathDef	7 math math: `liftRel_join.lem`, `liftRel_destruct`, `LiftRelO.imp`, `liftRel_destruct_iff`, `liftRel_dropn_destruct`, `LiftRelO.swap`, `LiftRelO.imp_right`
`«term_~ʷ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind_assoc` 📖	mathematical	—	`Equiv` `bind`	—	`bind_assoc_comp`
`bind_assoc_comp` 📖	mathematical	—	`Equiv` `bind` `Stream'.WSeq`	—	`map_join` `map_comp` `Function.comp_assoc` `join_join`
`bind_congr` 📖	mathematical	`Equiv`	`Equiv` `bind`	—	`liftRel_bind`
`bind_ret` 📖	mathematical	—	`Equiv` `bind` `Stream'.WSeq` `ret` `map`	—	`map_comp` `join_map_ret`
`cons_congr` 📖	mathematical	`Equiv`	`Equiv` `cons`	—	—
`destruct_congr` 📖	mathematical	`Equiv`	`Computation.LiftRel` `Stream'.WSeq` `BisimO` `Equiv` `destruct`	—	`liftRel_destruct`
`destruct_congr_iff` 📖	mathematical	—	`Equiv` `Computation.LiftRel` `Stream'.WSeq` `BisimO` `destruct`	—	`liftRel_destruct_iff`
`dropn_congr` 📖	mathematical	`Equiv`	`Equiv` `drop`	—	—
`exists_of_liftRel_left` 📖	mathematical	`LiftRel` `Stream'.WSeq` `membership`	`Stream'.WSeq` `membership`	—	`exists_get?_of_mem` `Computation.exists_of_mem_map` `liftRel_dropn_destruct` `get?_mem` `Computation.mem_map`
`exists_of_liftRel_right` 📖	mathematical	`LiftRel` `Stream'.WSeq` `membership`	`Stream'.WSeq` `membership`	—	`exists_of_liftRel_left` `LiftRel.swap`
`flatten_congr` 📖	mathematical	`Computation.LiftRel` `Stream'.WSeq` `Equiv`	`Equiv` `flatten`	—	`liftRel_flatten`
`flatten_equiv` 📖	mathematical	`Stream'.WSeq` `Computation` `Computation.instMembership`	`Equiv` `flatten`	—	`flatten_pure` `Equiv.trans` `flatten_think`
`get?_congr` 📖	mathematical	`Equiv`	`Computation.Equiv` `get?`	—	`head_congr` `dropn_congr`
`head_congr` 📖	mathematical	`Equiv`	`Computation.Equiv` `head`	—	`Computation.exists_of_mem_map` `destruct_congr` `Computation.mem_map` `Equiv.symm`
`join_append` 📖	mathematical	—	`Equiv` `join` `append` `Stream'.WSeq`	—	`nil_append` `join_nil` `destruct_nil` `join_cons` `destruct_think` `Computation.destruct_think` `join_think` `cons_append` `think_append` `append_assoc` `destruct_cons`
`join_congr` 📖	mathematical	`LiftRel` `Stream'.WSeq` `Equiv`	`Equiv` `join`	—	`liftRel_join`
`join_join` 📖	mathematical	—	`Equiv` `join` `Stream'.WSeq` `map`	—	`nil_append` `join_nil` `destruct_nil` `join_cons` `join_think` `destruct_think` `map_cons` `map_think` `cons_append` `Computation.destruct_think` `think_append` `append_assoc` `destruct_cons`
`join_map_ret` 📖	mathematical	—	`Equiv` `join` `map` `Stream'.WSeq` `ret`	—	`join_nil` `destruct_nil` `map_cons` `ofList_cons` `join_cons` `cons_append` `nil_append` `destruct_think` `destruct_cons` `Computation.destruct_think` `map_think` `join_think`
`join_ret` 📖	mathematical	—	`Equiv` `join` `ret` `Stream'.WSeq`	—	`ofList_cons` `join_cons` `join_nil` `append_nil` `think_equiv`
`liftRel_append` 📖	mathematical	`LiftRel`	`LiftRel` `append`	—	`Computation.LiftRel.imp` `LiftRelO.imp_right` `liftRel_destruct` `destruct_append` `Computation.liftRel_bind`
`liftRel_bind` 📖	mathematical	`LiftRel`	`LiftRel` `bind`	—	`liftRel_join` `liftRel_map`
`liftRel_cons` 📖	mathematical	—	`LiftRel` `cons`	—	`destruct_cons`
`liftRel_destruct` 📖	mathematical	`LiftRel`	`Computation.LiftRel` `Stream'.WSeq` `LiftRelO` `LiftRel` `destruct`	—	`Computation.LiftRel.imp` `LiftRelO.imp_right`
`liftRel_destruct_iff` 📖	mathematical	—	`LiftRel` `Computation.LiftRel` `Stream'.WSeq` `LiftRelO` `destruct`	—	`liftRel_destruct` `Computation.LiftRel.imp` `LiftRelO.imp_right`
`liftRel_dropn_destruct` 📖	mathematical	`LiftRel`	`Computation.LiftRel` `Stream'.WSeq` `LiftRelO` `LiftRel` `destruct` `drop`	—	`liftRel_destruct` `destruct_tail` `Computation.liftRel_bind`
`liftRel_flatten` 📖	mathematical	`Computation.LiftRel` `Stream'.WSeq` `LiftRel`	`LiftRel` `flatten`	—	`destruct_flatten` `Computation.liftRel_bind` `Computation.LiftRel.imp` `LiftRelO.imp_right` `flatten_pure` `liftRel_destruct`
`liftRel_join` 📖	mathematical	`LiftRel` `Stream'.WSeq`	`LiftRel` `join`	—	`nil_append` `destruct_append` `Computation.liftRel_bind` `liftRel_destruct` `liftRel_join.lem` `LiftRelO.swap` `LiftRel.swap`
`liftRel_map` 📖	mathematical	`LiftRel`	`LiftRel` `map`	—	`destruct_map` `Computation.liftRel_map` `liftRel_destruct`
`liftRel_nil` 📖	mathematical	—	`LiftRel` `nil`	—	`destruct_nil`
`liftRel_think_left` 📖	mathematical	—	`LiftRel` `think`	—	`liftRel_destruct_iff` `destruct_think`
`liftRel_think_right` 📖	mathematical	—	`LiftRel` `think`	—	`liftRel_destruct_iff` `destruct_think`
`map_congr` 📖	mathematical	`Equiv`	`Equiv` `map`	—	`liftRel_map`
`mem_congr` 📖	mathematical	`Equiv`	`Stream'.WSeq` `membership`	—	`exists_get?_of_mem` `get?_mem` `get?_congr` `Equiv.symm`
`ret_bind` 📖	mathematical	—	`Equiv` `bind` `ret`	—	`map_ret`
`tail_congr` 📖	mathematical	`Equiv`	`Equiv` `tail`	—	`flatten_congr` `Computation.bind_pure` `Computation.liftRel_bind` `destruct_congr` `Equiv.refl`
`think_congr` 📖	mathematical	`Equiv`	`Equiv` `think`	—	—
`think_equiv` 📖	mathematical	—	`Equiv` `think`	—	`Equiv.refl`

Stream'.WSeq.BisimO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`imp` 📖	mathematical	`Stream'.WSeq.BisimO`	`Stream'.WSeq.BisimO`	—	`Stream'.WSeq.LiftRelO.imp_right`

Stream'.WSeq.Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivalence` 📖	mathematical	—	`Stream'.WSeq` `Stream'.WSeq.Equiv`	—	`refl` `symm` `trans`
`ext` 📖	mathematical	`Computation.Equiv` `Stream'.WSeq.get?`	`Stream'.WSeq.Equiv`	—	`Computation.liftRel_def` `Stream'.WSeq.head_terminates_iff` `Computation.terminates_congr` `Computation.mem_unique` `Computation.mem_map` `Computation.Equiv.trans` `Computation.Equiv.symm` `Stream'.WSeq.get?_congr` `Stream'.WSeq.flatten_equiv` `Stream'.WSeq.get?_tail`
`refl` 📖	mathematical	—	`Stream'.WSeq.Equiv`	—	`Stream'.WSeq.LiftRel.refl`
`trans` 📖	mathematical	`Stream'.WSeq.Equiv`	`Stream'.WSeq.Equiv`	—	`IsTrans.trans` `Stream'.WSeq.LiftRel.trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv`

Stream'.WSeq.LiftRel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv` 📖	mathematical	—	`Stream'.WSeq` `Stream'.WSeq.LiftRel`	—	`refl` `symm` `IsTrans.trans` `trans` `Equivalence.isTrans`
`refl` 📖	mathematical	`Reflexive`	`Reflexive` `Stream'.WSeq` `Stream'.WSeq.LiftRel`	—	`Computation.LiftRel.refl`
`swap` 📖	mathematical	—	`Function.swap` `Stream'.WSeq` `Stream'.WSeq.LiftRel`	—	`swap_lem`
`swap_lem` 📖	mathematical	`Stream'.WSeq.LiftRel`	`Stream'.WSeq.LiftRel` `Function.swap`	—	`Stream'.WSeq.LiftRelO.swap` `Computation.LiftRel.swap` `Stream'.WSeq.liftRel_destruct`
`trans` 📖	mathematical	—	`IsTrans` `Stream'.WSeq` `Stream'.WSeq.LiftRel`	—	`Stream'.WSeq.liftRel_destruct` `Computation.liftRel_def` `Computation.terminates_of_liftRel` `Computation.rel_of_liftRel` `IsTrans.trans`

Stream'.WSeq.LiftRelO

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`imp` 📖	mathematical	`Stream'.WSeq.LiftRelO`	`Stream'.WSeq.LiftRelO`	—	—
`imp_right` 📖	mathematical	`Stream'.WSeq.LiftRelO`	`Stream'.WSeq.LiftRelO`	—	`imp`
`swap` 📖	mathematical	—	`Function.swap` `Stream'.WSeq` `Stream'.WSeq.LiftRelO`	—	—

Stream'.WSeq.liftRel_join

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lem` 📖	mathematical	`Stream'.WSeq.LiftRel` `Stream'.WSeq` `Computation` `Computation.instMembership` `Stream'.WSeq.destruct` `Stream'.WSeq.join`	`Stream'.WSeq` `Computation` `Computation.instMembership` `Stream'.WSeq.destruct` `Stream'.WSeq.join` `Stream'.WSeq.LiftRelO`	—	`Computation.exists_results_of_mem` `Computation.of_results_bind` `Stream'.WSeq.destruct_join` `Computation.exists_of_liftRel_left` `Stream'.WSeq.liftRel_destruct` `Computation.Results.mem` `Computation.mem_bind` `Computation.ret_mem` `Computation.eq_of_pure_mem` `Computation.of_results_think` `Stream'.WSeq.destruct_append` `lt_of_lt_of_le` `Computation.think_mem`

---

← Back to Index