OmegaLanguage

📁 Source: Cslib/Computability/Languages/OmegaLanguage.lean

Statistics

Metric	Count
Definitions `ωLanguage`, `OmegaLim`, `omegaLim`, `OmegaPow`, `omegaPow`, `instCompleteAtomicBooleanAlgebra`, `instHMulLanguage`, `instHasSubset`, `instInhabited`, `instInsertωSequence`, `instMembershipωSequence`, `instOmegaLim`, `instOmegaPowLanguageOfInhabited`, `instSingletonωSequence`, `map`, `omegaLim`, `omegaPow`, `«term_^ω»`, `«term_↗ω»`	19
Theorems `add_hmul`, `append_mem_hmul`, `bot_def`, `compl_def`, `ext`, `ext_iff`, `flatten_mem_omegaPow`, `hmul_bot`, `hmul_def`, `hmul_iSup`, `hmul_omegaPow_eq_omegaPow`, `hmul_omegaPow_le_omegaPow`, `hmul_seq_prop`, `hmul_sup`, `iInf_def`, `iSup_def`, `iSup_hmul`, `inf_def`, `kstar_hmul_omegaPow_eq_omegaPow`, `kstar_omegaPow_eq_omegaPow`, `kstar_omegaPow_le_omegaPow`, `le_def`, `le_hmul_congr`, `le_omegaPow_congr`, `map_def`, `map_id`, `map_map`, `mem_compl`, `mem_hmul`, `mem_iInf`, `mem_iSup`, `mem_inf`, `mem_omegaLim`, `mem_omegaPow`, `mem_sup`, `mem_top`, `mul_hmul`, `notMem_bot`, `omegaLim_def`, `omegaLim_zero`, `omegaPow_coind`, `omegaPow_coind'`, `omegaPow_def`, `omegaPow_eq_empty`, `omegaPow_le_hmul_omegaPow`, `omegaPow_le_hmul_omegaPow'`, `omegaPow_le_kstar_omegaPow`, `omegaPow_of_le_one`, `omegaPow_of_sub_one`, `omegaPow_seq_prop`, `one_hmul`, `one_omegaPow`, `sup_def`, `top_def`, `zero_hmul`, `zero_omegaPow`	56
Total	75

Cslib

Definitions

Name	Category	Theorems
`ωLanguage` 📖	CompOp	63 math math: `ωLanguage.iSup_def`, `ωLanguage.iInf_def`, `ωLanguage.IsRegular.regular_omegaLim`, `ωLanguage.omegaPow_seq_prop`, `ωLanguage.omegaPow_le_kstar_omegaPow`, `ωLanguage.zero_hmul`, `ωLanguage.IsRegular.iSup`, `ωLanguage.sup_def`, `ωLanguage.compl_def`, `ωLanguage.omegaLim_zero`, `ωLanguage.iSup_hmul`, `ωLanguage.flatten_mem_omegaPow`, `ωLanguage.Example.eventually_zero_not_omegaLim`, `ωLanguage.mem_top`, `ωLanguage.ext_iff`, `ωLanguage.mem_compl`, `ωLanguage.IsRegular.inf`, `ωLanguage.zero_omegaPow`, `ωLanguage.kstar_omegaPow_le_omegaPow`, `ωLanguage.hmul_sup`, `ωLanguage.hmul_seq_prop`, `ωLanguage.mem_omegaPow`, `ωLanguage.IsRegular.omegaPow`, `ωLanguage.omegaPow_def`, `Automata.ωAcceptor.mem_language`, `ωLanguage.one_omegaPow`, `ωLanguage.le_omegaPow_congr`, `ωLanguage.hmul_def`, `ωLanguage.mem_inf`, `ωLanguage.IsRegular.iInf`, `ωLanguage.hmul_omegaPow_le_omegaPow`, `Automata.NA.Buchi.language_eq_fin_iSup_hmul_omegaPow`, `ωLanguage.one_hmul`, `ωLanguage.hmul_omegaPow_eq_omegaPow`, `ωLanguage.mem_iSup`, `ωLanguage.omegaPow_of_le_one`, `ωLanguage.kstar_omegaPow_eq_omegaPow`, `ωLanguage.hmul_bot`, `ωLanguage.mem_iInf`, `ωLanguage.omegaPow_le_hmul_omegaPow'`, `ωLanguage.omegaPow_of_sub_one`, `ωLanguage.bot_def`, `ωLanguage.IsRegular.top`, `ωLanguage.mem_omegaLim`, `ωLanguage.hmul_iSup`, `ωLanguage.IsRegular.eq_fin_iSup_hmul_omegaPow`, `ωLanguage.mem_hmul`, `ωLanguage.notMem_bot`, `ωLanguage.IsRegular.sup`, `ωLanguage.add_hmul`, `ωLanguage.omegaPow_le_hmul_omegaPow`, `ωLanguage.IsRegular.hmul`, `ωLanguage.mem_sup`, `Automata.NA.Buchi.loop_language_eq`, `ωLanguage.mul_hmul`, `ωLanguage.top_def`, `ωLanguage.inf_def`, `ωLanguage.kstar_hmul_omegaPow_eq_omegaPow`, `Automata.NA.Buchi.concat_language_eq`, `ωLanguage.omegaLim_def`, `Automata.DA.buchi_eq_finAcc_omegaLim`, `ωLanguage.IsRegular.bot`, `ωLanguage.le_def`

Cslib.ωLanguage

Definitions

Name	Category	Theorems
`OmegaLim` 📖	CompData	—
`OmegaPow` 📖	CompData	—
`instCompleteAtomicBooleanAlgebra` 📖	CompOp	39 math math: `iSup_def`, `iInf_def`, `omegaPow_le_kstar_omegaPow`, `zero_hmul`, `IsRegular.iSup`, `sup_def`, `compl_def`, `omegaLim_zero`, `iSup_hmul`, `mem_top`, `mem_compl`, `IsRegular.inf`, `zero_omegaPow`, `kstar_omegaPow_le_omegaPow`, `hmul_sup`, `one_omegaPow`, `le_omegaPow_congr`, `mem_inf`, `IsRegular.iInf`, `hmul_omegaPow_le_omegaPow`, `Cslib.Automata.NA.Buchi.language_eq_fin_iSup_hmul_omegaPow`, `mem_iSup`, `omegaPow_of_le_one`, `hmul_bot`, `mem_iInf`, `omegaPow_le_hmul_omegaPow'`, `bot_def`, `IsRegular.top`, `hmul_iSup`, `IsRegular.eq_fin_iSup_hmul_omegaPow`, `notMem_bot`, `IsRegular.sup`, `add_hmul`, `omegaPow_le_hmul_omegaPow`, `mem_sup`, `top_def`, `inf_def`, `IsRegular.bot`, `le_def`
`instHMulLanguage` 📖	CompOp	22 math math: `zero_hmul`, `append_mem_hmul`, `iSup_hmul`, `hmul_sup`, `hmul_seq_prop`, `le_hmul_congr`, `hmul_def`, `hmul_omegaPow_le_omegaPow`, `Cslib.Automata.NA.Buchi.language_eq_fin_iSup_hmul_omegaPow`, `one_hmul`, `hmul_omegaPow_eq_omegaPow`, `hmul_bot`, `omegaPow_le_hmul_omegaPow'`, `hmul_iSup`, `IsRegular.eq_fin_iSup_hmul_omegaPow`, `mem_hmul`, `add_hmul`, `omegaPow_le_hmul_omegaPow`, `IsRegular.hmul`, `mul_hmul`, `kstar_hmul_omegaPow_eq_omegaPow`, `Cslib.Automata.NA.Buchi.concat_language_eq`
`instHasSubset` 📖	CompOp	1 math math: `le_def`
`instInhabited` 📖	CompOp	—
`instInsertωSequence` 📖	CompOp	—
`instMembershipωSequence` 📖	CompOp	14 math math: `flatten_mem_omegaPow`, `mem_top`, `ext_iff`, `mem_compl`, `hmul_seq_prop`, `mem_omegaPow`, `Cslib.Automata.ωAcceptor.mem_language`, `mem_inf`, `mem_iSup`, `mem_iInf`, `mem_omegaLim`, `mem_hmul`, `notMem_bot`, `mem_sup`
`instOmegaLim` 📖	CompOp	6 math math: `IsRegular.regular_omegaLim`, `omegaLim_zero`, `Example.eventually_zero_not_omegaLim`, `mem_omegaLim`, `omegaLim_def`, `Cslib.Automata.DA.buchi_eq_finAcc_omegaLim`
`instOmegaPowLanguageOfInhabited` 📖	CompOp	23 math math: `omegaPow_coind'`, `omegaPow_seq_prop`, `omegaPow_le_kstar_omegaPow`, `flatten_mem_omegaPow`, `zero_omegaPow`, `kstar_omegaPow_le_omegaPow`, `mem_omegaPow`, `IsRegular.omegaPow`, `omegaPow_def`, `one_omegaPow`, `le_omegaPow_congr`, `omegaPow_coind`, `hmul_omegaPow_le_omegaPow`, `Cslib.Automata.NA.Buchi.language_eq_fin_iSup_hmul_omegaPow`, `hmul_omegaPow_eq_omegaPow`, `omegaPow_of_le_one`, `kstar_omegaPow_eq_omegaPow`, `omegaPow_le_hmul_omegaPow'`, `omegaPow_of_sub_one`, `IsRegular.eq_fin_iSup_hmul_omegaPow`, `omegaPow_le_hmul_omegaPow`, `Cslib.Automata.NA.Buchi.loop_language_eq`, `kstar_hmul_omegaPow_eq_omegaPow`
`instSingletonωSequence` 📖	CompOp	—
`map` 📖	CompOp	3 math math: `map_id`, `map_def`, `map_map`
`omegaLim` 📖	CompOp	—
`omegaPow` 📖	CompOp	—
`«term_^ω»` 📖	CompOp	—
`«term_↗ω»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_hmul` 📖	mathematical	—	`Cslib.ωLanguage` `instHMulLanguage` `instCompleteAtomicBooleanAlgebra`	—	—
`append_mem_hmul` 📖	mathematical	`Cslib.ωSequence` `Cslib.ωLanguage` `instMembershipωSequence`	`instHMulLanguage` `Cslib.ωSequence.appendωSequence`	—	—
`bot_def` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `Cslib.ωSequence`	—	—
`compl_def` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `Cslib.ωSequence`	—	—
`ext` 📖	—	`Cslib.ωSequence` `Cslib.ωLanguage` `instMembershipωSequence`	—	—	—
`ext_iff` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.ωLanguage` `instMembershipωSequence`	—	`ext`
`flatten_mem_omegaPow` 📖	mathematical	`Cslib.ωSequence` `Cslib.instFunLikeωSequenceNat`	`Cslib.ωLanguage` `instMembershipωSequence` `OmegaPow.omegaPow` `instOmegaPowLanguageOfInhabited` `Cslib.ωSequence.flatten`	—	—
`hmul_bot` 📖	mathematical	—	`Cslib.ωLanguage` `instHMulLanguage` `instCompleteAtomicBooleanAlgebra`	—	—
`hmul_def` 📖	mathematical	—	`Cslib.ωLanguage` `instHMulLanguage` `Cslib.ωSequence` `Cslib.ωSequence.appendωSequence`	—	—
`hmul_iSup` 📖	mathematical	—	`Cslib.ωLanguage` `instHMulLanguage` `instCompleteAtomicBooleanAlgebra`	—	—
`hmul_omegaPow_eq_omegaPow` 📖	mathematical	—	`Cslib.ωLanguage` `instHMulLanguage` `OmegaPow.omegaPow` `instOmegaPowLanguageOfInhabited`	—	`hmul_omegaPow_le_omegaPow` `omegaPow_le_hmul_omegaPow`
`hmul_omegaPow_le_omegaPow` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `instHMulLanguage` `OmegaPow.omegaPow` `instOmegaPowLanguageOfInhabited`	—	`mul_hmul` `Language.sub_one_mul` `Language.mul_sub_one` `le_hmul_congr` `omegaPow_le_hmul_omegaPow'` `omegaPow_coind`
`hmul_seq_prop` 📖	mathematical	—	`Cslib.ωLanguage` `instHMulLanguage` `Cslib.ωSequence` `Cslib.ωSequence.take` `instMembershipωSequence` `Cslib.ωSequence.drop`	—	`ext` `Cslib.ωSequence.take_append_of_le_length` `Cslib.ωSequence.drop_append_ωSequence` `Cslib.ωSequence.append_take_drop`
`hmul_sup` 📖	mathematical	—	`Cslib.ωLanguage` `instHMulLanguage` `instCompleteAtomicBooleanAlgebra`	—	—
`iInf_def` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `Cslib.ωSequence`	—	—
`iSup_def` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `Cslib.ωSequence`	—	—
`iSup_hmul` 📖	mathematical	—	`Cslib.ωLanguage` `instHMulLanguage` `instCompleteAtomicBooleanAlgebra`	—	—
`inf_def` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `Cslib.ωSequence`	—	—
`kstar_hmul_omegaPow_eq_omegaPow` 📖	mathematical	—	`Cslib.ωLanguage` `instHMulLanguage` `OmegaPow.omegaPow` `instOmegaPowLanguageOfInhabited`	—	`kstar_omegaPow_eq_omegaPow` `hmul_omegaPow_eq_omegaPow`
`kstar_omegaPow_eq_omegaPow` 📖	mathematical	—	`OmegaPow.omegaPow` `Cslib.ωLanguage` `instOmegaPowLanguageOfInhabited`	—	`kstar_omegaPow_le_omegaPow` `omegaPow_le_kstar_omegaPow`
`kstar_omegaPow_le_omegaPow` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `OmegaPow.omegaPow` `instOmegaPowLanguageOfInhabited`	—	`omegaPow_le_hmul_omegaPow'` `Language.kstar_sub_one` `mul_hmul` `hmul_omegaPow_eq_omegaPow` `omegaPow_coind`
`le_def` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `instHasSubset`	—	—
`le_hmul_congr` 📖	mathematical	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra`	`instHMulLanguage`	—	—
`le_omegaPow_congr` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `OmegaPow.omegaPow` `instOmegaPowLanguageOfInhabited`	—	—
`map_def` 📖	mathematical	—	`map` `Cslib.ωSequence` `Cslib.ωSequence.map`	—	—
`map_id` 📖	mathematical	—	`map`	—	—
`map_map` 📖	mathematical	—	`map`	—	—
`mem_compl` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.ωLanguage` `instMembershipωSequence` `instCompleteAtomicBooleanAlgebra`	—	—
`mem_hmul` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.ωLanguage` `instMembershipωSequence` `instHMulLanguage` `Cslib.ωSequence.appendωSequence`	—	—
`mem_iInf` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.ωLanguage` `instMembershipωSequence` `instCompleteAtomicBooleanAlgebra`	—	—
`mem_iSup` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.ωLanguage` `instMembershipωSequence` `instCompleteAtomicBooleanAlgebra`	—	—
`mem_inf` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.ωLanguage` `instMembershipωSequence` `instCompleteAtomicBooleanAlgebra`	—	—
`mem_omegaLim` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.ωLanguage` `instMembershipωSequence` `OmegaLim.omegaLim` `instOmegaLim` `Cslib.ωSequence.extract`	—	—
`mem_omegaPow` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.ωLanguage` `instMembershipωSequence` `OmegaPow.omegaPow` `instOmegaPowLanguageOfInhabited` `Cslib.ωSequence.flatten` `Cslib.instFunLikeωSequenceNat`	—	—
`mem_sup` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.ωLanguage` `instMembershipωSequence` `instCompleteAtomicBooleanAlgebra`	—	—
`mem_top` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.ωLanguage` `instMembershipωSequence` `instCompleteAtomicBooleanAlgebra`	—	—
`mul_hmul` 📖	mathematical	—	`Cslib.ωLanguage` `instHMulLanguage`	—	`Cslib.ωSequence.append_append_ωSequence`
`notMem_bot` 📖	mathematical	—	`Cslib.ωSequence` `Cslib.ωLanguage` `instMembershipωSequence` `instCompleteAtomicBooleanAlgebra`	—	—
`omegaLim_def` 📖	mathematical	—	`OmegaLim.omegaLim` `Cslib.ωLanguage` `instOmegaLim` `Cslib.ωSequence` `Cslib.ωSequence.extract`	—	—
`omegaLim_zero` 📖	mathematical	—	`OmegaLim.omegaLim` `Cslib.ωLanguage` `instOmegaLim` `instCompleteAtomicBooleanAlgebra`	—	`ext`
`omegaPow_coind` 📖	mathematical	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `instHMulLanguage`	`OmegaPow.omegaPow` `instOmegaPowLanguageOfInhabited`	—	`omegaPow_of_sub_one` `omegaPow_coind'`
`omegaPow_coind'` 📖	mathematical	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `instHMulLanguage`	`OmegaPow.omegaPow` `instOmegaPowLanguageOfInhabited`	—	`hmul_seq_prop` `omegaPow_seq_prop`
`omegaPow_def` 📖	mathematical	—	`OmegaPow.omegaPow` `Cslib.ωLanguage` `instOmegaPowLanguageOfInhabited` `Cslib.ωSequence` `Cslib.ωSequence.flatten`	—	—
`omegaPow_eq_empty` 📖	—	`OmegaPow.omegaPow` `Cslib.ωLanguage` `instOmegaPowLanguageOfInhabited` `instCompleteAtomicBooleanAlgebra`	—	—	—
`omegaPow_le_hmul_omegaPow` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `OmegaPow.omegaPow` `instOmegaPowLanguageOfInhabited` `instHMulLanguage`	—	`omegaPow_le_hmul_omegaPow'` `le_hmul_congr`
`omegaPow_le_hmul_omegaPow'` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `OmegaPow.omegaPow` `instOmegaPowLanguageOfInhabited` `instHMulLanguage`	—	—
`omegaPow_le_kstar_omegaPow` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `OmegaPow.omegaPow` `instOmegaPowLanguageOfInhabited`	—	—
`omegaPow_of_le_one` 📖	mathematical	—	`OmegaPow.omegaPow` `Cslib.ωLanguage` `instOmegaPowLanguageOfInhabited` `instCompleteAtomicBooleanAlgebra`	—	`Language.le_one_iff_eq` `zero_omegaPow` `one_omegaPow`
`omegaPow_of_sub_one` 📖	mathematical	—	`OmegaPow.omegaPow` `Cslib.ωLanguage` `instOmegaPowLanguageOfInhabited`	—	`ext`
`omegaPow_seq_prop` 📖	mathematical	—	`OmegaPow.omegaPow` `Cslib.ωLanguage` `instOmegaPowLanguageOfInhabited` `Cslib.ωSequence`	—	`ext` `Cslib.ωSequence.strictMono_flatten`
`one_hmul` 📖	mathematical	—	`Cslib.ωLanguage` `instHMulLanguage`	—	—
`one_omegaPow` 📖	mathematical	—	`OmegaPow.omegaPow` `Cslib.ωLanguage` `instOmegaPowLanguageOfInhabited` `instCompleteAtomicBooleanAlgebra`	—	`omegaPow_of_sub_one` `zero_omegaPow`
`sup_def` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `Cslib.ωSequence`	—	—
`top_def` 📖	mathematical	—	`Cslib.ωLanguage` `instCompleteAtomicBooleanAlgebra` `Cslib.ωSequence`	—	—
`zero_hmul` 📖	mathematical	—	`Cslib.ωLanguage` `instHMulLanguage` `instCompleteAtomicBooleanAlgebra`	—	—
`zero_omegaPow` 📖	mathematical	—	`OmegaPow.omegaPow` `Cslib.ωLanguage` `instOmegaPowLanguageOfInhabited` `instCompleteAtomicBooleanAlgebra`	—	`ext`

Cslib.ωLanguage.OmegaLim

Definitions

Name	Category	Theorems
`omegaLim` 📖	CompOp	6 math math: `Cslib.ωLanguage.IsRegular.regular_omegaLim`, `Cslib.ωLanguage.omegaLim_zero`, `Cslib.ωLanguage.Example.eventually_zero_not_omegaLim`, `Cslib.ωLanguage.mem_omegaLim`, `Cslib.ωLanguage.omegaLim_def`, `Cslib.Automata.DA.buchi_eq_finAcc_omegaLim`

Cslib.ωLanguage.OmegaPow

Definitions

Name	Category	Theorems
`omegaPow` 📖	CompOp	23 math math: `Cslib.ωLanguage.omegaPow_coind'`, `Cslib.ωLanguage.omegaPow_seq_prop`, `Cslib.ωLanguage.omegaPow_le_kstar_omegaPow`, `Cslib.ωLanguage.flatten_mem_omegaPow`, `Cslib.ωLanguage.zero_omegaPow`, `Cslib.ωLanguage.kstar_omegaPow_le_omegaPow`, `Cslib.ωLanguage.mem_omegaPow`, `Cslib.ωLanguage.IsRegular.omegaPow`, `Cslib.ωLanguage.omegaPow_def`, `Cslib.ωLanguage.one_omegaPow`, `Cslib.ωLanguage.le_omegaPow_congr`, `Cslib.ωLanguage.omegaPow_coind`, `Cslib.ωLanguage.hmul_omegaPow_le_omegaPow`, `Cslib.Automata.NA.Buchi.language_eq_fin_iSup_hmul_omegaPow`, `Cslib.ωLanguage.hmul_omegaPow_eq_omegaPow`, `Cslib.ωLanguage.omegaPow_of_le_one`, `Cslib.ωLanguage.kstar_omegaPow_eq_omegaPow`, `Cslib.ωLanguage.omegaPow_le_hmul_omegaPow'`, `Cslib.ωLanguage.omegaPow_of_sub_one`, `Cslib.ωLanguage.IsRegular.eq_fin_iSup_hmul_omegaPow`, `Cslib.ωLanguage.omegaPow_le_hmul_omegaPow`, `Cslib.Automata.NA.Buchi.loop_language_eq`, `Cslib.ωLanguage.kstar_hmul_omegaPow_eq_omegaPow`

---

← Back to Index