Transport for Closure Predicates

This file records that the standard language-class closure predicates are extensional: they transport across pointwise equivalence of language classes.

theorem ClosedUnderUnion_of_iff {α : Type u_1} {P Q : Language α → Prop} (hiff : ∀ (L : Language α), P L ↔ Q L) : ClosedUnderUnion P → ClosedUnderUnion Q

Union closure is invariant under pointwise equivalence of language classes.

theorem ClosedUnderIntersection_of_iff {α : Type u_1} {P Q : Language α → Prop} (hiff : ∀ (L : Language α), P L ↔ Q L) : ClosedUnderIntersection P → ClosedUnderIntersection Q

Intersection closure is invariant under pointwise equivalence of language classes.

theorem ClosedUnderComplement_of_iff {α : Type u_1} {P Q : Language α → Prop} (hiff : ∀ (L : Language α), P L ↔ Q L) : ClosedUnderComplement P → ClosedUnderComplement Q

Complement closure is invariant under pointwise equivalence of language classes.

theorem ClosedUnderConcatenation_of_iff {α : Type u_1} {P Q : Language α → Prop} (hiff : ∀ (L : Language α), P L ↔ Q L) : ClosedUnderConcatenation P → ClosedUnderConcatenation Q

Concatenation closure is invariant under pointwise equivalence of language classes.

theorem ClosedUnderKleeneStar_of_iff {α : Type u_1} {P Q : Language α → Prop} (hiff : ∀ (L : Language α), P L ↔ Q L) : ClosedUnderKleeneStar P → ClosedUnderKleeneStar Q

Kleene-star closure is invariant under pointwise equivalence of language classes.

theorem ClosedUnderReverse_of_iff {α : Type u_1} {P Q : Language α → Prop} (hiff : ∀ (L : Language α), P L ↔ Q L) : ClosedUnderReverse P → ClosedUnderReverse Q

Reverse closure is invariant under pointwise equivalence of language classes.

theorem ClosedUnderIntersectionWithRegular_of_iff {α : Type u_1} {P Q : Language α → Prop} (hiff : ∀ (L : Language α), P L ↔ Q L) : ClosedUnderIntersectionWithRegular P → ClosedUnderIntersectionWithRegular Q

Closure under intersection with regular languages is invariant under pointwise equivalence of language classes.

theorem ClosedUnderRightQuotient_of_iff {α : Type u_1} {P Q : Language α → Prop} (hiff : ∀ (L : Language α), P L ↔ Q L) : ClosedUnderRightQuotient P → ClosedUnderRightQuotient Q

Right-quotient closure is invariant under pointwise equivalence of language classes.

theorem ClosedUnderRightQuotientWithRegular_of_iff {α : Type u_1} {P Q : Language α → Prop} (hiff : ∀ (L : Language α), P L ↔ Q L) : ClosedUnderRightQuotientWithRegular P → ClosedUnderRightQuotientWithRegular Q

Closure under right quotient with regular languages is invariant under pointwise equivalence of language classes.

theorem ClosedUnderHomomorphism_of_iff {isP isQ : {α : Type} → [Fintype α] → Language α → Prop} (hiff : ∀ {β : Type} [inst : Fintype β] (L : Language β), isP L ↔ isQ L) : (ClosedUnderHomomorphism fun {α : Type} [Fintype α] => isP) → ClosedUnderHomomorphism fun {α : Type} [Fintype α] => isQ

Homomorphism closure is invariant under pointwise equivalence of finite-alphabet-indexed language classes.

theorem ClosedUnderEpsFreeHomomorphism_of_iff {isP isQ : {α : Type} → [Fintype α] → Language α → Prop} (hiff : ∀ {β : Type} [inst : Fintype β] (L : Language β), isP L ↔ isQ L) : (ClosedUnderEpsFreeHomomorphism fun {α : Type} [Fintype α] => isP) → ClosedUnderEpsFreeHomomorphism fun {α : Type} [Fintype α] => isQ

Epsilon-free homomorphism closure is invariant under pointwise equivalence of finite-alphabet-indexed language classes.

theorem ClosedUnderInverseHomomorphism_of_iff {isP isQ : {α : Type} → [Fintype α] → Language α → Prop} (hiff : ∀ {β : Type} [inst : Fintype β] (L : Language β), isP L ↔ isQ L) : (ClosedUnderInverseHomomorphism fun {α : Type} [Fintype α] => isP) → ClosedUnderInverseHomomorphism fun {α : Type} [Fintype α] => isQ

Inverse-homomorphism closure is invariant under pointwise equivalence of finite-alphabet-indexed language classes.

theorem ClosedUnderSubstitution_of_iff {isP isQ : {α : Type} → [Fintype α] → Language α → Prop} (hiff : ∀ {β : Type} [inst : Fintype β] (L : Language β), isP L ↔ isQ L) : (ClosedUnderSubstitution fun {α : Type} [Fintype α] => isP) → ClosedUnderSubstitution fun {α : Type} [Fintype α] => isQ

Substitution closure is invariant under pointwise equivalence of finite-alphabet-indexed language classes.