Temporal

📁 Source: Cslib/Foundations/Data/OmegaSequence/Temporal.lean

Statistics

Metric	Count
Definitions LeadsTo, Step	2
Theorems mk, mk, drop_frequently_iff_frequently, frequently_leadsTo_frequently, leadsTo_cases_or, leadsTo_trans, step_leadsTo, until_frequently_leadsTo_and, until_frequently_not_leadsTo	9
Total	11

Cslib.ωSequence

Definitions

Name	Category	Theorems
LeadsTo 📖	MathDef	4 math math: LeadsTo.mk, until_frequently_leadsTo_and, step_leadsTo, until_frequently_not_leadsTo
Step 📖	MathDef	1 math math: Step.mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
drop_frequently_iff_frequently 📖	mathematical	—	Cslib.ωSequence Cslib.instFunLikeωSequenceNat drop	—	get_drop
frequently_leadsTo_frequently 📖	—	Cslib.ωSequence Cslib.instFunLikeωSequenceNat LeadsTo	—	—	—
leadsTo_cases_or 📖	—	LeadsTo	—	—	—
leadsTo_trans 📖	—	LeadsTo	—	—	—
step_leadsTo 📖	mathematical	Step	LeadsTo	—	—
until_frequently_leadsTo_and 📖	mathematical	Step Cslib.ωSequence Cslib.instFunLikeωSequenceNat	LeadsTo	—	—
until_frequently_not_leadsTo 📖	mathematical	Step Cslib.ωSequence Cslib.instFunLikeωSequenceNat	LeadsTo	—	—

Cslib.ωSequence.LeadsTo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk 📖	mathematical	Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.ωSequence.LeadsTo	—	—

Cslib.ωSequence.Step

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk 📖	mathematical	Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.ωSequence.Step	—	—

---

← Back to Index