Omega reg lang inter
omega_reg_lang_inter
Plain-language statement
ω-regular languages are closed under intersection.
Exact Lean statement
theorem omega_reg_lang_inter {L0 L1 : Set (Stream' A)}
(h0 : OmegaRegLang L0) (h1 : OmegaRegLang L1) : OmegaRegLang (L0 ∩ L1)Formal artifact
Lean source
theorem omega_reg_lang_inter {L0 L1 : Set (Stream' A)} (h0 : OmegaRegLang L0) (h1 : OmegaRegLang L1) : OmegaRegLang (L0 ∩ L1) := by obtain ⟨M0, acc0, h_fin0, h_l0⟩ := h0 obtain ⟨M1, acc1, h_fin1, h_l1⟩ := h1 let M_u : (i : Fin 2) → Automata.NA A | 0 => M0 | 1 => M1 let acc_u : (i : Fin 2) → Set (M_u i).State | 0 => acc0 | 1 => acc1 use (Automata.NA.OI2 M_u acc_u), (Automata.NA.OI2_Acc M_u acc_u) constructor · simp [Automata.NA.OI2, Automata.NA.addHist, Automata.NA.Prod] have h_fin1 : ∀ i, Finite (M_u i).State := by simp [Fin.forall_fin_two, M_u, h_fin0, h_fin1] have h_fin2 : Finite ((i : Fin 2) → (M_u i).State) := by exact Pi.finite exact Finite.instProd · ext as simp [h_l0, h_l1, Automata.acc_omega_lang_inter2 M_u acc_u, Fin.forall_fin_two, M_u, acc_u]- Project
- Automata Theory
- License
- Apache-2.0
- Commit
- f196548710ce
- Source
- AutomataTheory/Languages/OmegaRegLang.lean:85-102
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Acc lang congr
acc_lang_congr
Plain-language statement
The language accepted by c.toDA with a unique accepting state s is exactly the equivalence class of s.
Source project: Automata Theory
Person-level attribution pending.
Acc lang concat e
Automata.acc_lang_concat_e
Plain-language statement
The language of the concatenation NA that is accepted by M0's accepting states is the language accepted by M0.
Source project: Automata Theory
Person-level attribution pending.
Acc lang concat ne
Automata.acc_lang_concat_ne
Plain-language statement
The language of the concatenation NA that is accepted by M1's accepting states is the language accepted by M0 concatenated with the language accepted by M1 minus the empty word.
Source project: Automata Theory
Person-level attribution pending.