Parallel

📁 Source: Mathlib/Data/Seq/Parallel.lean

Statistics

Metric	Count
Definitions Parallel, parallel, parallelRec	3
Theorems exists_of_mem_parallel, map_parallel, mem_parallel, parallel_congr_left, parallel_congr_lem, parallel_congr_right, parallel_empty, parallel_promises, terminates_parallel, aux	10
Total	13

AffineSubspace

Definitions

Name	Category	Theorems
Parallel 📖	MathDef	10 math math: affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty, affineSpan_pair_parallel_iff_exists_unit_smul', parallel_bot_iff_eq_bot, parallel_iff_direction_eq_and_eq_bot_iff_eq_bot, affineSpan_pair_parallel_iff_exists_unit_smul, parallel_comm, EuclideanGeometry.Sphere.orthRadius_parallel_orthRadius_iff, Parallel.refl, bot_parallel_iff_eq_bot, affineSpan_pair_parallel_iff_vectorSpan_eq

Computation

Definitions

Name	Category	Theorems
parallel 📖	CompOp	7 math math: terminates_parallel, map_parallel, mem_parallel, parallel_congr_right, parallel_empty, parallel_promises, parallel_congr_left
parallelRec 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_of_mem_parallel 📖	mathematical	Computation instMembership parallel	Stream'.WSeq Stream'.WSeq.membership	—	destruct_eq_pure ret_mem destruct_eq_think think_mem corec_eq Stream'.WSeq.notMem_nil Stream'.Seq.destruct_eq_cons Stream'.Seq.mem_cons_of_mem Stream'.Seq.mem_cons destruct_think
map_parallel 📖	mathematical	—	map parallel Stream'.WSeq.map Computation	—	eq_of_bisim destruct_map corec_eq Stream'.WSeq.seq_destruct_cons Stream'.WSeq.map_cons Stream'.WSeq.seq_destruct_think Stream'.WSeq.map_think
mem_parallel 📖	mathematical	Promises Computation Stream'.WSeq Stream'.WSeq.membership instMembership	parallel	—	mem_of_promises terminates_parallel terminates_of_mem parallel_promises
parallel_congr_left 📖	mathematical	Promises Stream'.WSeq.LiftRel Computation Equiv	parallel	—	parallel_congr_lem parallel_promises exists_of_mem_parallel Stream'.WSeq.exists_of_liftRel_left mem_parallel Stream'.WSeq.exists_of_liftRel_right
parallel_congr_lem 📖	mathematical	Stream'.WSeq.LiftRel Computation Equiv	Promises	—	Stream'.WSeq.exists_of_liftRel_right promises_congr Stream'.WSeq.exists_of_liftRel_left
parallel_congr_right 📖	mathematical	Promises Stream'.WSeq.LiftRel Computation Equiv	parallel	—	parallel_congr_left parallel_congr_lem
parallel_empty 📖	mathematical	Promises Computation Stream'.WSeq.head	parallel empty	—	eq_empty_of_not_terminates exists_of_mem_parallel Stream'.WSeq.exists_get?_of_mem Stream'.WSeq.head_some_of_get?_some
parallel_promises 📖	mathematical	Promises	parallel	—	exists_of_mem_parallel
terminates_parallel 📖	mathematical	Computation Stream'.WSeq Stream'.WSeq.membership	Terminates parallel	—	terminates_parallel.aux destruct_eq_pure corec_eq ret_terminates destruct_eq_think think_terminates Stream'.Seq.get?_tail

Computation.terminates_parallel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aux 📖	mathematical	Computation	Computation.Terminates Stream'.WSeq	—	Computation.destruct_eq_pure Computation.corec_eq Computation.ret_terminates instIsEmptyFalse Computation.destruct_think Computation.destruct_eq_think Computation.think_terminates

---

← Back to Index