P. 110 of Theorem List - Intuitionistic Logic Explorer

Type

Label

Description

Statement

Theorem

fz1eqb 10901

Two possibly-empty 1-based finite sets of sequential integers are equal iff their endpoints are equal. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 29-Mar-2014.)

⊢ ((𝑀 ∈ ℕ₀ ∧ 𝑁 ∈ ℕ₀) → ((1...𝑀) = (1...𝑁) ↔ 𝑀 = 𝑁))

Theorem

filtinf 10902

The size of an infinite set is greater than the size of a finite set. (Contributed by Jim Kingdon, 21-Feb-2022.)

⊢ ((𝐴 ∈ Fin ∧ ω ≼ 𝐵) → (♯‘𝐴) < (♯‘𝐵))

Theorem

isfinite4im 10903

A finite set is equinumerous to the range of integers from one up to the hash value of the set. (Contributed by Jim Kingdon, 22-Feb-2022.)

⊢ (𝐴 ∈ Fin → (1...(♯‘𝐴)) ≈ 𝐴)

Theorem

fihasheq0 10904

Two ways of saying a finite set is empty. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 27-Jul-2014.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)

⊢ (𝐴 ∈ Fin → ((♯‘𝐴) = 0 ↔ 𝐴 = ∅))

Theorem

fihashneq0 10905

Two ways of saying a finite set is not empty. Also, "A is inhabited" would be equivalent by fin0 6955. (Contributed by Alexander van der Vekens, 23-Sep-2018.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)

⊢ (𝐴 ∈ Fin → (0 < (♯‘𝐴) ↔ 𝐴 ≠ ∅))

Theorem

hashnncl 10906

Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.)

⊢ (𝐴 ∈ Fin → ((♯‘𝐴) ∈ ℕ ↔ 𝐴 ≠ ∅))

Theorem

hash0 10907

The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.)

⊢ (♯‘∅) = 0

Theorem

fihashelne0d 10908

A finite set with an element has nonzero size. (Contributed by Rohan Ridenour, 3-Aug-2023.)

⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → ¬ (♯‘𝐴) = 0)

Theorem

hashsng 10909

The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 13-Feb-2013.)

⊢ (𝐴 ∈ 𝑉 → (♯‘{𝐴}) = 1)

Theorem

fihashen1 10910

A finite set has size 1 if and only if it is equinumerous to the ordinal 1. (Contributed by AV, 14-Apr-2019.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)

⊢ (𝐴 ∈ Fin → ((♯‘𝐴) = 1 ↔ 𝐴 ≈ 1_o))

Theorem

fihashfn 10911

A function on a finite set is equinumerous to its domain. (Contributed by Mario Carneiro, 12-Mar-2015.) (Intuitionized by Jim Kingdon, 24-Feb-2022.)

⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ Fin) → (♯‘𝐹) = (♯‘𝐴))

Theorem

fseq1hash 10912

The value of the size function on a finite 1-based sequence. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 12-Mar-2015.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐹 Fn (1...𝑁)) → (♯‘𝐹) = 𝑁)

Theorem

omgadd 10913

Mapping ordinal addition to integer addition. (Contributed by Jim Kingdon, 24-Feb-2022.)

⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    ⇒   ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐺‘(𝐴 +_o 𝐵)) = ((𝐺‘𝐴) + (𝐺‘𝐵)))

Theorem

fihashdom 10914

Dominance relation for the size function. (Contributed by Jim Kingdon, 24-Feb-2022.)

⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ((♯‘𝐴) ≤ (♯‘𝐵) ↔ 𝐴 ≼ 𝐵))

Theorem

hashunlem 10915

Lemma for hashun 10916. Ordinal size of the union. (Contributed by Jim Kingdon, 25-Feb-2022.)

⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ (𝜑 → 𝑁 ∈ ω)    &   ⊢ (𝜑 → 𝑀 ∈ ω)    &   ⊢ (𝜑 → 𝐴 ≈ 𝑁)    &   ⊢ (𝜑 → 𝐵 ≈ 𝑀)    ⇒   ⊢ (𝜑 → (𝐴 ∪ 𝐵) ≈ (𝑁 +_o 𝑀))

Theorem

hashun 10916

The size of the union of disjoint finite sets is the sum of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.) (Revised by Mario Carneiro, 15-Sep-2013.)

⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ (𝐴 ∩ 𝐵) = ∅) → (♯‘(𝐴 ∪ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵)))

Theorem

1elfz0hash 10917

1 is an element of the finite set of sequential nonnegative integers bounded by the size of a nonempty finite set. (Contributed by AV, 9-May-2020.)

⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → 1 ∈ (0...(♯‘𝐴)))

Theorem

hashunsng 10918

The size of the union of a finite set with a disjoint singleton is one more than the size of the set. (Contributed by Paul Chapman, 30-Nov-2012.)

⊢ (𝐵 ∈ 𝑉 → ((𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ 𝐴) → (♯‘(𝐴 ∪ {𝐵})) = ((♯‘𝐴) + 1)))

Theorem

hashprg 10919

The size of an unordered pair. (Contributed by Mario Carneiro, 27-Sep-2013.) (Revised by Mario Carneiro, 5-May-2016.) (Revised by AV, 18-Sep-2021.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ≠ 𝐵 ↔ (♯‘{𝐴, 𝐵}) = 2))

Theorem

prhash2ex 10920

There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 10926, numbers are used instead of sets because their representation is shorter (and more comprehensive). (Contributed by AV, 29-Jan-2020.)

⊢ (♯‘{0, 1}) = 2

Theorem

hashp1i 10921

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

⊢ 𝐴 ∈ ω    &   ⊢ 𝐵 = suc 𝐴    &   ⊢ (♯‘𝐴) = 𝑀    &   ⊢ (𝑀 + 1) = 𝑁    ⇒   ⊢ (♯‘𝐵) = 𝑁

Theorem

hash1 10922

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

⊢ (♯‘1_o) = 1

Theorem

hash2 10923

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

⊢ (♯‘2_o) = 2

Theorem

hash3 10924

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

⊢ (♯‘3_o) = 3

Theorem

hash4 10925

Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)

⊢ (♯‘4_o) = 4

Theorem

pr0hash2ex 10926

There is (at least) one set with two different elements: the unordered pair containing the empty set and the singleton containing the empty set. (Contributed by AV, 29-Jan-2020.)

⊢ (♯‘{∅, {∅}}) = 2

Theorem

fihashss 10927

The size of a subset is less than or equal to the size of its superset. (Contributed by Alexander van der Vekens, 14-Jul-2018.)

⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (♯‘𝐵) ≤ (♯‘𝐴))

Theorem

fiprsshashgt1 10928

The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021.)

⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐶 ∈ Fin) → ({𝐴, 𝐵} ⊆ 𝐶 → 2 ≤ (♯‘𝐶)))

Theorem

fihashssdif 10929

The size of the difference of a finite set and a finite subset is the set's size minus the subset's. (Contributed by Jim Kingdon, 31-May-2022.)

⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ∧ 𝐵 ⊆ 𝐴) → (♯‘(𝐴 ∖ 𝐵)) = ((♯‘𝐴) − (♯‘𝐵)))

Theorem

hashdifsn 10930

The size of the difference of a finite set and a singleton subset is the set's size minus 1. (Contributed by Alexander van der Vekens, 6-Jan-2018.)

⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝐴) → (♯‘(𝐴 ∖ {𝐵})) = ((♯‘𝐴) − 1))

Theorem

hashdifpr 10931

The size of the difference of a finite set and a proper ordered pair subset is the set's size minus 2. (Contributed by AV, 16-Dec-2020.)

⊢ ((𝐴 ∈ Fin ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶)) → (♯‘(𝐴 ∖ {𝐵, 𝐶})) = ((♯‘𝐴) − 2))

Theorem

hashfz 10932

Value of the numeric cardinality of a nonempty integer range. (Contributed by Stefan O'Rear, 12-Sep-2014.) (Proof shortened by Mario Carneiro, 15-Apr-2015.)

⊢ (𝐵 ∈ (ℤ_≥‘𝐴) → (♯‘(𝐴...𝐵)) = ((𝐵 − 𝐴) + 1))

Theorem

hashfzo 10933

Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)

⊢ (𝐵 ∈ (ℤ_≥‘𝐴) → (♯‘(𝐴..^𝐵)) = (𝐵 − 𝐴))

Theorem

hashfzo0 10934

Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.)

⊢ (𝐵 ∈ ℕ₀ → (♯‘(0..^𝐵)) = 𝐵)

Theorem

hashfzp1 10935

Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.)

⊢ (𝐵 ∈ (ℤ_≥‘𝐴) → (♯‘((𝐴 + 1)...𝐵)) = (𝐵 − 𝐴))

Theorem

hashfz0 10936

Value of the numeric cardinality of a nonempty range of nonnegative integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.)

⊢ (𝐵 ∈ ℕ₀ → (♯‘(0...𝐵)) = (𝐵 + 1))

Theorem

hashxp 10937

The size of the Cartesian product of two finite sets is the product of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.)

⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) · (♯‘𝐵)))

Theorem

fimaxq 10938*

A finite set of rational numbers has a maximum. (Contributed by Jim Kingdon, 6-Sep-2022.)

⊢ ((𝐴 ⊆ ℚ ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)

Theorem

fiubm 10939*

Lemma for fiubz 10940 and fiubnn 10941. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.)

⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ ℚ)    &   ⊢ (𝜑 → 𝐶 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)

Theorem

fiubz 10940*

A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.)

⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)

Theorem

fiubnn 10941*

A finite set of natural numbers has an upper bound which is a a natural number. (Contributed by Jim Kingdon, 29-Oct-2024.)

⊢ ((𝐴 ⊆ ℕ ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ ℕ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)

Theorem

resunimafz0 10942

The union of a restriction by an image over an open range of nonnegative integers and a singleton of an ordered pair is a restriction by an image over an interval of nonnegative integers. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 20-Feb-2021.)

⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    ⇒   ⊢ (𝜑 → (𝐼 ↾ (𝐹 “ (0...𝑁))) = ((𝐼 ↾ (𝐹 “ (0..^𝑁))) ∪ {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩}))

Theorem

fnfz0hash 10943

The size of a function on a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 25-Jun-2018.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐹 Fn (0...𝑁)) → (♯‘𝐹) = (𝑁 + 1))

Theorem

ffz0hash 10944

The size of a function on a finite set of sequential nonnegative integers equals the upper bound of the sequence increased by 1. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Proof shortened by AV, 11-Apr-2021.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐹:(0...𝑁)⟶𝐵) → (♯‘𝐹) = (𝑁 + 1))

Theorem

ffzo0hash 10945

The size of a function on a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 25-Mar-2018.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐹 Fn (0..^𝑁)) → (♯‘𝐹) = 𝑁)

Theorem

fnfzo0hash 10946

The size of a function on a half-open range of nonnegative integers equals the upper bound of this range. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Proof shortened by AV, 11-Apr-2021.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐹:(0..^𝑁)⟶𝐵) → (♯‘𝐹) = 𝑁)

Theorem

hashfacen 10947*

The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.)

⊢ ((𝐴 ≈ 𝐵 ∧ 𝐶 ≈ 𝐷) → {𝑓 ∣ 𝑓:𝐴–1-1-onto→𝐶} ≈ {𝑓 ∣ 𝑓:𝐵–1-1-onto→𝐷})

Theorem

leisorel 10948

Version of isorel 5858 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.)

⊢ ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^*) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶 ≤ 𝐷 ↔ (𝐹‘𝐶) ≤ (𝐹‘𝐷)))

Theorem

zfz1isolemsplit 10949

Lemma for zfz1iso 10952. Removing one element from an integer range. (Contributed by Jim Kingdon, 8-Sep-2022.)

⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)}))

Theorem

zfz1isolemiso 10950*

Lemma for zfz1iso 10952. Adding one element to the order isomorphism. (Contributed by Jim Kingdon, 8-Sep-2022.)

⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ⊆ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)    &   ⊢ (𝜑 → 𝐺 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))    &   ⊢ (𝜑 → 𝐴 ∈ (1...(♯‘𝑋)))    &   ⊢ (𝜑 → 𝐵 ∈ (1...(♯‘𝑋)))    ⇒   ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ((𝐺 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝐴) < ((𝐺 ∪ {⟨(♯‘𝑋), 𝑀⟩})‘𝐵)))

Theorem

zfz1isolem1 10951*

Lemma for zfz1iso 10952. Existence of an order isomorphism given the existence of shorter isomorphisms. (Contributed by Jim Kingdon, 7-Sep-2022.)

⊢ (𝜑 → 𝐾 ∈ ω)    &   ⊢ (𝜑 → ∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)))    &   ⊢ (𝜑 → 𝑋 ⊆ ℤ)    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ (𝜑 → 𝑋 ≈ suc 𝐾)    &   ⊢ (𝜑 → 𝑀 ∈ 𝑋)    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀)    ⇒   ⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋))

Theorem

zfz1iso 10952*

A finite set of integers has an order isomorphism to a one-based finite sequence. (Contributed by Jim Kingdon, 3-Sep-2022.)

⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝐴)), 𝐴))

Theorem

seq3coll 10953*

The function 𝐹 contains a sparse set of nonzero values to be summed. The function 𝐺 is an order isomorphism from the set of nonzero values of 𝐹 to a 1-based finite sequence, and 𝐻 collects these nonzero values together. Under these conditions, the sum over the values in 𝐻 yields the same result as the sum over the original set 𝐹. (Contributed by Mario Carneiro, 2-Apr-2014.) (Revised by Jim Kingdon, 9-Apr-2023.)

⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑍 + 𝑘) = 𝑘)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑆) → (𝑘 + 𝑍) = 𝑘)    &   ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑛 ∈ 𝑆)) → (𝑘 + 𝑛) ∈ 𝑆)    &   ⊢ (𝜑 → 𝑍 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐺 Isom < , < ((1...(♯‘𝐴)), 𝐴))    &   ⊢ (𝜑 → 𝑁 ∈ (1...(♯‘𝐴)))    &   ⊢ (𝜑 → 𝐴 ⊆ (ℤ_≥‘𝑀))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘𝑀)) → (𝐹‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘1)) → (𝐻‘𝑘) ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝑀...(𝐺‘(♯‘𝐴))) ∖ 𝐴)) → (𝐹‘𝑘) = 𝑍)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (1...(♯‘𝐴))) → (𝐻‘𝑛) = (𝐹‘(𝐺‘𝑛)))    ⇒   ⊢ (𝜑 → (seq𝑀( + , 𝐹)‘(𝐺‘𝑁)) = (seq1( + , 𝐻)‘𝑁))

4.7  Words over a set

This section is about words (or strings) over a set (alphabet) defined as finite sequences of symbols (or characters) being elements of the alphabet. Although it is often required that the underlying set/alphabet be nonempty, finite and not a proper class, these restrictions are not made in the current definition df-word 10955. Note that the empty word ∅ (i.e., the empty set) is the only word over an empty alphabet, see 0wrd0 10980. The set Word 𝑆 of words over 𝑆 is the free monoid over 𝑆, where the monoid law is concatenation and the monoid unit is the empty word. Besides the definition of words themselves, several operations on words are defined in this section:

Name	Reference	Explanation	Example	Remarks
Length (or size) of a word	df-ihash 10887: (♯‘𝑊)	Operation which determines the number of the symbols within the word.	𝑊:(0..^𝑁)⟶𝑆 → (𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 𝑁	This is not a special definition for words, but for arbitrary sets.
First symbol of a word	df-fv 5267: (𝑊‘0)	Operation which extracts the first symbol of a word. The result is the symbol at the first place in the sequence representing the word.	𝑊:(0..^1)⟶𝑆 → (𝑊 ∈ Word 𝑆 ∧ (𝑊‘0) ∈ 𝑆	This is not a special definition for words, but for arbitrary functions with a half-open range of nonnegative integers as domain.

Conventions:

• Words are usually represented by class variable 𝑊, or if two words are involved, by 𝑊 and 𝑈 or by 𝐴 and 𝐵.
• The alphabets are usually represented by class variable 𝑉 (because any arbitrary set can be an alphabet), sometimes also by 𝑆 (especially as codomain of the function representing a word, because the alphabet is the set of symbols).
• The symbols are usually represented by class variables 𝑆 or 𝐴, or if two symbols are involved, by 𝑆 and 𝑇 or by 𝐴 and 𝐵.
• The indices of the sequence representing a word are usually represented by class variable 𝐼, if two indices are involved (especially for subwords) by 𝐼 and 𝐽, or by 𝑀 and 𝑁.
• The length of a word is usually represented by class variables 𝑁 or 𝐿.
• The number of positions by which to cyclically shift a word is usually represented by class variables 𝑁 or 𝐿.

4.7.1  Definitions and basic theorems

Syntax

cword 10954

Syntax for the Word operator.

class Word 𝑆

Definition

df-word 10955*

Define the class of words over a set. A word (sometimes also called a string) is a finite sequence of symbols from a set (alphabet) 𝑆. Definition in Section 9.1 of [AhoHopUll] p. 318. The domain is forced to be an initial segment of ℕ₀ so that two words with the same symbols in the same order be equal. The set Word 𝑆 is sometimes denoted by S*, using the Kleene star, although the Kleene star, or Kleene closure, is sometimes reserved to denote an operation on languages. The set Word 𝑆 equipped with concatenation is the free monoid over 𝑆, and the monoid unit is the empty word. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

⊢ Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ₀ 𝑤:(0..^𝑙)⟶𝑆}

Theorem

iswrd 10956*

Property of being a word over a set with an existential quantifier over the length. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.)

⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ₀ 𝑊:(0..^𝑙)⟶𝑆)

Theorem

wrdval 10957*

Value of the set of words over a set. (Contributed by Stefan O'Rear, 10-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)

⊢ (𝑆 ∈ 𝑉 → Word 𝑆 = ∪ 𝑙 ∈ ℕ₀ (𝑆 ↑_𝑚 (0..^𝑙)))

Theorem

lencl 10958

The length of a word is a nonnegative integer. This corresponds to the definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 27-Aug-2015.)

⊢ (𝑊 ∈ Word 𝑆 → (♯‘𝑊) ∈ ℕ₀)

Theorem

iswrdinn0 10959

A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 16-Aug-2025.)

⊢ ((𝑊:(0..^𝐿)⟶𝑆 ∧ 𝐿 ∈ ℕ₀) → 𝑊 ∈ Word 𝑆)

Theorem

wrdf 10960

A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.)

⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)

Theorem

iswrdiz 10961

A zero-based sequence is a word. In iswrdinn0 10959 we can specify a length as an nonnegative integer. However, it will occasionally be helpful to allow a negative length, as well as zero, to specify an empty sequence. (Contributed by Jim Kingdon, 18-Aug-2025.)

⊢ ((𝑊:(0..^𝐿)⟶𝑆 ∧ 𝐿 ∈ ℤ) → 𝑊 ∈ Word 𝑆)

Theorem

wrddm 10962

The indices of a word (i.e. its domain regarded as function) are elements of an open range of nonnegative integers (of length equal to the length of the word). (Contributed by AV, 2-May-2020.)

⊢ (𝑊 ∈ Word 𝑆 → dom 𝑊 = (0..^(♯‘𝑊)))

Theorem

sswrd 10963

The set of words respects ordering on the base set. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.)

⊢ (𝑆 ⊆ 𝑇 → Word 𝑆 ⊆ Word 𝑇)

Theorem

snopiswrd 10964

A singleton of an ordered pair (with 0 as first component) is a word. (Contributed by AV, 23-Nov-2018.) (Proof shortened by AV, 18-Apr-2021.)

⊢ (𝑆 ∈ 𝑉 → {⟨0, 𝑆⟩} ∈ Word 𝑉)

Theorem

wrdexg 10965

The set of words over a set is a set. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by JJ, 18-Nov-2022.)

⊢ (𝑆 ∈ 𝑉 → Word 𝑆 ∈ V)

Theorem

wrdexb 10966

The set of words over a set is a set, bidirectional version. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 23-Nov-2018.)

⊢ (𝑆 ∈ V ↔ Word 𝑆 ∈ V)

Theorem

wrdexi 10967

The set of words over a set is a set, inference form. (Contributed by AV, 23-May-2021.)

⊢ 𝑆 ∈ V    ⇒   ⊢ Word 𝑆 ∈ V

Theorem

wrdsymbcl 10968

A symbol within a word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.)

⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊‘𝐼) ∈ 𝑉)

Theorem

wrdfn 10969

A word is a function with a zero-based sequence of integers as domain. (Contributed by Alexander van der Vekens, 13-Apr-2018.)

⊢ (𝑊 ∈ Word 𝑆 → 𝑊 Fn (0..^(♯‘𝑊)))

Theorem

wrdv 10970

A word over an alphabet is a word over the universal class. (Contributed by AV, 8-Feb-2021.) (Proof shortened by JJ, 18-Nov-2022.)

⊢ (𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word V)

Theorem

wrdlndm 10971

The length of a word is not in the domain of the word (regarded as a function). (Contributed by AV, 3-Mar-2021.) (Proof shortened by JJ, 18-Nov-2022.)

⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∉ dom 𝑊)

Theorem

iswrdsymb 10972*

An arbitrary word is a word over an alphabet if all of its symbols belong to the alphabet. (Contributed by AV, 23-Jan-2021.)

⊢ ((𝑊 ∈ Word V ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ∈ 𝑉) → 𝑊 ∈ Word 𝑉)

Theorem

wrdfin 10973

A word is a finite set. (Contributed by Stefan O'Rear, 2-Nov-2015.) (Proof shortened by AV, 18-Nov-2018.)

⊢ (𝑊 ∈ Word 𝑆 → 𝑊 ∈ Fin)

Theorem

lennncl 10974

The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015.)

⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℕ)

Theorem

wrdffz 10975

A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021.)

⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0...((♯‘𝑊) − 1))⟶𝑆)

Theorem

wrdeq 10976

Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016.)

⊢ (𝑆 = 𝑇 → Word 𝑆 = Word 𝑇)

Theorem

wrdeqi 10977

Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021.)

⊢ 𝑆 = 𝑇    ⇒   ⊢ Word 𝑆 = Word 𝑇

Theorem

iswrddm0 10978

A function with empty domain is a word. (Contributed by AV, 13-Oct-2018.)

⊢ (𝑊:∅⟶𝑆 → 𝑊 ∈ Word 𝑆)

Theorem

wrd0 10979

The empty set is a word (the empty word, frequently denoted ε in this context). This corresponds to the definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 13-May-2020.)

⊢ ∅ ∈ Word 𝑆

Theorem

0wrd0 10980

The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.)

⊢ (𝑊 ∈ Word ∅ ↔ 𝑊 = ∅)

Theorem

wrdsymb 10981

A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022.)

⊢ (𝑆 ∈ Word 𝐴 → 𝑆 ∈ Word (𝑆 “ (0..^(♯‘𝑆))))

Theorem

nfwrd 10982

Hypothesis builder for Word 𝑆. (Contributed by Mario Carneiro, 26-Feb-2016.)

⊢ Ⅎ𝑥𝑆    ⇒   ⊢ Ⅎ𝑥Word 𝑆

Theorem

csbwrdg 10983*

Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.)

⊢ (𝑆 ∈ 𝑉 → ⦋𝑆 / 𝑥⦌Word 𝑥 = Word 𝑆)

Theorem

wrdnval 10984*

Words of a fixed length are mappings from a fixed half-open integer interval. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Proof shortened by AV, 13-May-2020.)

⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ₀) → {𝑤 ∈ Word 𝑉 ∣ (♯‘𝑤) = 𝑁} = (𝑉 ↑_𝑚 (0..^𝑁)))

Theorem

wrdmap 10985

Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.)

⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ₀) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ↔ 𝑊 ∈ (𝑉 ↑_𝑚 (0..^𝑁))))

Theorem

wrdsymb0 10986

A symbol at a position "outside" of a word. (Contributed by Alexander van der Vekens, 26-May-2018.) (Proof shortened by AV, 2-May-2020.)

⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝐼 < 0 ∨ (♯‘𝑊) ≤ 𝐼) → (𝑊‘𝐼) = ∅))

Theorem

wrdlenge1n0 10987

A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.)

⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ ↔ 1 ≤ (♯‘𝑊)))

Theorem

len0nnbi 10988

The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022.)

⊢ (𝑊 ∈ Word 𝑆 → (𝑊 ≠ ∅ ↔ (♯‘𝑊) ∈ ℕ))

Theorem

wrdlenge2n0 10989

A word with length at least 2 is not empty. (Contributed by AV, 18-Jun-2018.) (Proof shortened by AV, 14-Oct-2018.)

⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → 𝑊 ≠ ∅)

Theorem

wrdsymb1 10990

The first symbol of a nonempty word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.)

⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑊)) → (𝑊‘0) ∈ 𝑉)

Theorem

wrdlen1 10991*

A word of length 1 starts with a symbol. (Contributed by AV, 20-Jul-2018.) (Proof shortened by AV, 19-Oct-2018.)

⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 1) → ∃𝑣 ∈ 𝑉 (𝑊‘0) = 𝑣)

Theorem

fstwrdne 10992

The first symbol of a nonempty word is element of the alphabet for the word. (Contributed by AV, 28-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)

⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊‘0) ∈ 𝑉)

Theorem

fstwrdne0 10993

The first symbol of a nonempty word is element of the alphabet for the word. (Contributed by AV, 29-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)

⊢ ((𝑁 ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁)) → (𝑊‘0) ∈ 𝑉)

Theorem

eqwrd 10994*

Two words are equal iff they have the same length and the same symbol at each position. (Contributed by AV, 13-Apr-2018.) (Revised by JJ, 30-Dec-2023.)

⊢ ((𝑈 ∈ Word 𝑆 ∧ 𝑊 ∈ Word 𝑇) → (𝑈 = 𝑊 ↔ ((♯‘𝑈) = (♯‘𝑊) ∧ ∀𝑖 ∈ (0..^(♯‘𝑈))(𝑈‘𝑖) = (𝑊‘𝑖))))

Theorem

elovmpowrd 10995*

Implications for the value of an operation defined by the maps-to notation with a class abstraction of words as a result having an element. Note that 𝜑 may depend on 𝑧 as well as on 𝑣 and 𝑦. (Contributed by Alexander van der Vekens, 15-Jul-2018.)

⊢ 𝑂 = (𝑣 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∈ Word 𝑣 ∣ 𝜑})    ⇒   ⊢ (𝑍 ∈ (𝑉𝑂𝑌) → (𝑉 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ Word 𝑉))

Theorem

wrdred1 10996

A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.)

⊢ (𝐹 ∈ Word 𝑆 → (𝐹 ↾ (0..^((♯‘𝐹) − 1))) ∈ Word 𝑆)

Theorem

wrdred1hash 10997

The length of a word truncated by a symbol. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.)

⊢ ((𝐹 ∈ Word 𝑆 ∧ 1 ≤ (♯‘𝐹)) → (♯‘(𝐹 ↾ (0..^((♯‘𝐹) − 1)))) = ((♯‘𝐹) − 1))

4.8  Elementary real and complex functions

4.8.1  The "shift" operation

Syntax

cshi 10998

Extend class notation with function shifter.

class shift

Definition

df-shft 10999*

Define a function shifter. This operation offsets the value argument of a function (ordinarily on a subset of ℂ) and produces a new function on ℂ. See shftval 11009 for its value. (Contributed by NM, 20-Jul-2005.)

⊢ shift = (𝑓 ∈ V, 𝑥 ∈ ℂ ↦ {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ ℂ ∧ (𝑦 − 𝑥)𝑓𝑧)})

Theorem

shftlem 11000*

Two ways to write a shifted set (𝐵 + 𝐴). (Contributed by Mario Carneiro, 3-Nov-2013.)

⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ⊆ ℂ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝐴) ∈ 𝐵} = {𝑥 ∣ ∃𝑦 ∈ 𝐵 𝑥 = (𝑦 + 𝐴)})