Init

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

Statistics

Metric	Count
Definitions `instInhabited`	1
Theorems `append_append_ωSequence`, `append_eq_cons`, `append_extract_drop`, `append_extract_extract`, `append_left_injective`, `append_left_right_injective`, `append_right_inj`, `append_right_injective`, `append_take`, `append_take_drop`, `append_ωSequence_head_tail`, `concat_take_get`, `cons_append_ωSequence`, `cons_head_tail`, `cons_injective2`, `cons_injective_left`, `cons_injective_right`, `const_eq`, `dropLast_take`, `drop_append_of_ge_length`, `drop_append_of_le_length`, `drop_append_ωSequence`, `drop_const`, `drop_drop`, `drop_map`, `drop_succ`, `drop_tail'`, `drop_zero`, `drop_zip`, `eta`, `ext`, `ext_iff`, `extract_0u_extract_l`, `extract_0u_extract_lu`, `extract_append_zero_right`, `extract_apppend_right_right`, `extract_drop`, `extract_eq_drop_take`, `extract_eq_extract`, `extract_eq_nil`, `extract_eq_nil_iff`, `extract_eq_ofFn`, `extract_eq_take`, `extract_lu_extract_lu`, `extract_succ_right`, `getElem?_take`, `getElem?_take_succ`, `get_append_left`, `get_append_length`, `get_append_right`, `get_append_right'`, `get_cons_append_zero`, `get_const`, `get_drop`, `get_extract`, `get_fun`, `get_iterate`, `get_map`, `get_succ`, `get_succ_cons`, `get_succ_iterate`, `get_succ_iterate'`, `get_tail`, `get_zero_cons`, `get_zero_iterate`, `get_zip`, `head_cons`, `head_drop`, `head_iterate`, `head_map`, `head_zip`, `iterate_eq`, `iterate_id`, `length_extract`, `length_take`, `map_append_ωSequence`, `map_cons`, `map_const`, `map_eq`, `map_id`, `map_iterate`, `map_map`, `map_tail`, `map_take`, `nil_append_ωSequence`, `tail_cons`, `tail_const`, `tail_drop`, `tail_drop'`, `tail_eq_drop`, `tail_iterate`, `tail_map`, `tail_zip`, `take_add`, `take_append_of_le_length`, `take_drop`, `take_get`, `take_one`, `take_prefix`, `take_prefix_take_left`, `take_succ`, `take_succ'`, `take_succ_cons`, `take_take`, `take_theorem`, `take_zero`, `zip_eq`	107
Total	108

Cslib.ωSequence

Definitions

Name	Category	Theorems
`instInhabited` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`append_append_ωSequence` 📖	mathematical	—	`appendωSequence`	—	`cons_append_ωSequence`
`append_eq_cons` 📖	mathematical	—	`appendωSequence` `cons`	—	—
`append_extract_drop` 📖	mathematical	—	`appendωSequence` `extract` `drop`	—	`extract_eq_take` `append_take_drop`
`append_extract_extract` 📖	mathematical	—	`extract`	—	—
`append_left_injective` 📖	—	`appendωSequence`	—	—	`get_append_left`
`append_left_right_injective` 📖	—	`appendωSequence`	—	—	`append_left_injective`
`append_right_inj` 📖	mathematical	—	`appendωSequence`	—	`append_right_injective`
`append_right_injective` 📖	—	`appendωSequence`	—	—	`ext` `get_append_right`
`append_take` 📖	mathematical	—	`take` `appendωSequence`	—	—
`append_take_drop` 📖	mathematical	—	`appendωSequence` `take` `drop`	—	`take_succ` `drop_succ` `cons_append_ωSequence` `eta`
`append_ωSequence_head_tail` 📖	mathematical	—	`appendωSequence` `head` `tail`	—	`eta`
`concat_take_get` 📖	mathematical	—	`take` `Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	`take_succ'`
`cons_append_ωSequence` 📖	mathematical	—	`appendωSequence` `cons`	—	—
`cons_head_tail` 📖	mathematical	—	`cons` `head` `tail`	—	`eta`
`cons_injective2` 📖	mathematical	—	`Cslib.ωSequence` `cons`	—	`get_zero_cons` `ext` `get_succ_cons`
`cons_injective_left` 📖	mathematical	—	`Cslib.ωSequence` `cons`	—	`cons_injective2`
`cons_injective_right` 📖	mathematical	—	`Cslib.ωSequence` `cons`	—	`cons_injective2`
`const_eq` 📖	mathematical	—	`const` `cons`	—	`ext`
`dropLast_take` 📖	mathematical	—	`take`	—	`take_succ'`
`drop_append_of_ge_length` 📖	mathematical	—	`drop` `appendωSequence`	—	`ext` `get_drop` `get_append_right'`
`drop_append_of_le_length` 📖	mathematical	—	`drop` `appendωSequence`	—	`ext` `get_drop` `get_append_left` `get_append_right`
`drop_append_ωSequence` 📖	mathematical	—	`drop` `appendωSequence`	—	`drop_succ` `cons_append_ωSequence` `tail_cons`
`drop_const` 📖	mathematical	—	`drop` `const`	—	`ext`
`drop_drop` 📖	mathematical	—	`drop`	—	`ext` `get_drop`
`drop_map` 📖	mathematical	—	`drop` `map`	—	`ext`
`drop_succ` 📖	mathematical	—	`drop` `tail`	—	—
`drop_tail'` 📖	mathematical	—	`drop` `tail`	—	—
`drop_zero` 📖	mathematical	—	`drop`	—	—
`drop_zip` 📖	mathematical	—	`drop` `zip`	—	`ext`
`eta` 📖	mathematical	—	`cons` `head` `tail`	—	—
`ext` 📖	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	—	—
`ext_iff` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	`ext`
`extract_0u_extract_l` 📖	mathematical	—	`extract`	—	—
`extract_0u_extract_lu` 📖	mathematical	—	`extract`	—	—
`extract_append_zero_right` 📖	mathematical	—	`extract` `appendωSequence`	—	`extract_eq_take`
`extract_apppend_right_right` 📖	mathematical	—	`extract` `appendωSequence`	—	—
`extract_drop` 📖	mathematical	—	`extract` `drop`	—	—
`extract_eq_drop_take` 📖	mathematical	—	`extract` `take` `drop`	—	—
`extract_eq_extract` 📖	mathematical	`extract`	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	`extract_eq_ofFn`
`extract_eq_nil` 📖	mathematical	—	`extract`	—	`extract_eq_drop_take`
`extract_eq_nil_iff` 📖	mathematical	—	`extract`	—	—
`extract_eq_ofFn` 📖	mathematical	—	`extract` `Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	—
`extract_eq_take` 📖	mathematical	—	`extract` `take`	—	`extract_eq_drop_take`
`extract_lu_extract_lu` 📖	mathematical	—	`extract`	—	—
`extract_succ_right` 📖	mathematical	—	`extract` `Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	`append_extract_extract`
`getElem?_take` 📖	mathematical	—	`take` `Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	`length_take` `take_succ` `get_succ`
`getElem?_take_succ` 📖	mathematical	—	`take` `Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	`getElem?_take`
`get_append_left` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `appendωSequence`	—	—
`get_append_length` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `appendωSequence`	—	`get_append_right`
`get_append_right` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `appendωSequence`	—	—
`get_append_right'` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `appendωSequence`	—	`get_append_right`
`get_cons_append_zero` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `appendωSequence`	—	—
`get_const` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `const`	—	—
`get_drop` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `drop`	—	—
`get_extract` 📖	mathematical	—	`extract` `Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	`extract_eq_drop_take` `take_get` `get_drop`
`get_fun` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	—
`get_iterate` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `iterate`	—	—
`get_map` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `map`	—	—
`get_succ` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `tail`	—	—
`get_succ_cons` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `cons`	—	—
`get_succ_iterate` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `iterate`	—	`get_succ` `tail_iterate`
`get_succ_iterate'` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `iterate`	—	`get_iterate`
`get_tail` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `tail`	—	—
`get_zero_cons` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `cons`	—	—
`get_zero_iterate` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `iterate`	—	—
`get_zip` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat` `zip`	—	—
`head_cons` 📖	mathematical	—	`head` `cons`	—	—
`head_drop` 📖	mathematical	—	`head` `drop` `Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	`get_drop`
`head_iterate` 📖	mathematical	—	`head` `iterate`	—	—
`head_map` 📖	mathematical	—	`head` `map`	—	—
`head_zip` 📖	mathematical	—	`head` `zip`	—	—
`iterate_eq` 📖	mathematical	—	`iterate` `cons`	—	`eta` `tail_iterate`
`iterate_id` 📖	mathematical	—	`iterate` `const`	—	`ext`
`length_extract` 📖	mathematical	—	`extract`	—	`extract_eq_drop_take` `length_take`
`length_take` 📖	mathematical	—	`take`	—	—
`map_append_ωSequence` 📖	mathematical	—	`map` `appendωSequence`	—	`cons_append_ωSequence` `map_cons`
`map_cons` 📖	mathematical	—	`map` `cons`	—	`eta` `map_eq`
`map_const` 📖	mathematical	—	`map` `const`	—	—
`map_eq` 📖	mathematical	—	`map` `cons` `head` `tail`	—	`eta` `tail_map` `head_map`
`map_id` 📖	mathematical	—	`map`	—	—
`map_iterate` 📖	mathematical	—	`iterate` `map`	—	`ext` `get_map` `get_succ_iterate` `get_succ_iterate'`
`map_map` 📖	mathematical	—	`map`	—	—
`map_tail` 📖	mathematical	—	`map` `tail`	—	—
`map_take` 📖	mathematical	—	`take` `map`	—	`length_take` `take_get`
`nil_append_ωSequence` 📖	mathematical	—	`appendωSequence`	—	—
`tail_cons` 📖	mathematical	—	`tail` `cons`	—	—
`tail_const` 📖	mathematical	—	`tail` `const`	—	`const_eq`
`tail_drop` 📖	mathematical	—	`tail` `drop`	—	`tail_drop'`
`tail_drop'` 📖	mathematical	—	`tail` `drop`	—	`ext` `get_drop`
`tail_eq_drop` 📖	mathematical	—	`tail` `drop`	—	—
`tail_iterate` 📖	mathematical	—	`tail` `iterate`	—	`ext` `get_tail` `get_succ_iterate'`
`tail_map` 📖	mathematical	—	`tail` `map`	—	—
`tail_zip` 📖	mathematical	—	`tail` `zip`	—	—
`take_add` 📖	mathematical	—	`take` `drop`	—	`append_left_injective` `append_take_drop` `append_append_ωSequence` `length_take`
`take_append_of_le_length` 📖	mathematical	—	`take` `appendωSequence`	—	`length_take` `take_get` `get_append_left`
`take_drop` 📖	mathematical	—	`take` `drop`	—	`length_take` `take_get` `get_drop`
`take_get` 📖	mathematical	`take`	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	`append_take_drop` `get_append_left`
`take_one` 📖	mathematical	—	`take` `Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	—
`take_prefix` 📖	mathematical	—	`take`	—	`length_take` `take_prefix_take_left`
`take_prefix_take_left` 📖	mathematical	—	`take`	—	`take_take`
`take_succ` 📖	mathematical	—	`take` `head` `tail`	—	—
`take_succ'` 📖	mathematical	—	`take` `Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	—	`take_succ` `get_tail`
`take_succ_cons` 📖	mathematical	—	`take` `cons`	—	—
`take_take` 📖	mathematical	—	`take`	—	`take_zero` `take_succ`
`take_theorem` 📖	—	`take`	—	—	`ext` `getElem?_take_succ`
`take_zero` 📖	mathematical	—	`take`	—	—
`zip_eq` 📖	mathematical	—	`zip` `cons` `head` `tail`	—	`eta`

---

← Back to Index