Regular Expressions (additional definitions and theorems)

This file contains additional definitions and theorems about RegularExpression as defined and developed in Mathlib.Computability.RegularExpressions.

@[simp]

theorem RegularExpression.mem_sum_matches' {α : Type u_1} (rs : List (RegularExpression α)) (x : List α) : x ∈ rs.sum.matches' ↔ ∃ r ∈ rs, x ∈ r.matches'

theorem RegularExpression.iSup_matches' {α : Type u_1} {I : Type u_2} [Finite I] {s : Set I} {l : I → Language α} (h : ∀ i ∈ s, ∃ (r : RegularExpression α), l i = r.matches') : ∃ (r : RegularExpression α), ⨆ i ∈ s, l i = r.matches'