InfOcc
📁 Source: Cslib/Foundations/Data/OmegaSequence/InfOcc.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsinfOcc | 1 |
| 4 | |
| Total | 5 |
Cslib.ωSequence
Definitions
| Name | Category | Theorems |
|---|---|---|
infOcc 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
frequently_iff_strictMono 📖 | — | — | — | — | — |
frequently_in_finite_type 📖 | mathematical | — | Cslib.ωSequenceCslib.instFunLikeωSequenceNat | — | — |
frequently_in_strictMono 📖 | — | — | — | — | — |
strictMono_of_infinite 📖 | — | — | — | — | — |
---