Documentation Verification Report

Segment

📁 Source: Cslib/Foundations/Data/Nat/Segment.lean

Statistics

Metric	Count
Definitions `segment`, `segment'`	2
Theorems `base_zero_strictMono`, `count_notMem_range_pos`, `infinite_strictMono`, `nth_of_strictMono`, `nth_succ_gap`, `segment'_eq_segment`, `segment_galois_connection`, `segment_idem`, `segment_lower_bound`, `segment_lower_bound'`, `segment_plus_one`, `segment_pre_zero`, `segment_range_val`, `segment_upper_bound`, `segment_upper_bound'`, `segment_zero`, `segment_zero'`, `strictMono_infinite`, `strictMono_range_gap`	19
Total	21

Nat

Definitions

Name	Category	Theorems
`segment` 📖	CompOp	15 math math: `segment_range_val`, `segment_idem`, `segment_lower_bound'`, `segment_upper_bound`, `segment_plus_one`, `segment_zero`, `segment_upper_bound'`, `Cslib.ωSequence.flatten_def`, `segment_pre_zero`, `segment_galois_connection`, `Cslib.ωSequence.cumLen_segment_zero`, `segment_lower_bound`, `Cslib.ωSequence.cumLen_segment_one_add`, `segment'_eq_segment`, `segment_zero'`
`segment'` 📖	CompOp	1 math math: `segment'_eq_segment`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`base_zero_strictMono` 📖	—	—	—	—	—
`count_notMem_range_pos` 📖	—	—	—	—	—
`infinite_strictMono` 📖	—	—	—	—	—
`nth_of_strictMono` 📖	—	—	—	—	`strictMono_infinite`
`nth_succ_gap` 📖	—	—	—	—	—
`segment'_eq_segment` 📖	mathematical	—	`segment'` `segment`	—	—
`segment_galois_connection` 📖	mathematical	—	`segment`	—	`segment_upper_bound` `segment_lower_bound`
`segment_idem` 📖	mathematical	—	`segment`	—	`strictMono_infinite` `nth_of_strictMono`
`segment_lower_bound` 📖	mathematical	—	`segment`	—	`nth_of_strictMono` `segment.eq_1` `count_notMem_range_pos`
`segment_lower_bound'` 📖	mathematical	—	`segment`	—	`segment'_eq_segment` `segment'.eq_1` `segment_lower_bound` `base_zero_strictMono`
`segment_plus_one` 📖	mathematical	—	`segment`	—	—
`segment_pre_zero` 📖	mathematical	—	`segment`	—	`segment.eq_1`
`segment_range_val` 📖	mathematical	—	`segment`	—	`segment_idem` `strictMono_range_gap` `nth_of_strictMono`
`segment_upper_bound` 📖	mathematical	—	`segment`	—	`nth_of_strictMono` `segment_plus_one` `strictMono_infinite`
`segment_upper_bound'` 📖	mathematical	—	`segment`	—	`segment'_eq_segment` `segment'.eq_1` `segment_upper_bound` `base_zero_strictMono`
`segment_zero` 📖	mathematical	—	`segment`	—	`segment_idem`
`segment_zero'` 📖	mathematical	—	`segment`	—	`segment'_eq_segment` `segment'.eq_1`
`strictMono_infinite` 📖	—	—	—	—	—
`strictMono_range_gap` 📖	—	—	—	—	`strictMono_infinite` `nth_succ_gap` `nth_of_strictMono`

---

← Back to Index