Documentation

Bookshelf.Enderton.Set.Chapter_3

Enderton.Set.Chapter_3 #

Relations and Functions

theorem Enderton.Set.Chapter_3.lemma_3b {α : Type u_1} {x : α} {y : α} {C : Set α} (hx : x C) (hy : y C) :

Lemma 3B #

If x ∈ C and y ∈ C, then ⟨x, y⟩ ∈ 𝒫 𝒫 C.

theorem Enderton.Set.Chapter_3.theorem_3d {α : Type u_1} {x : α} {y : α} {A : Set (Set (Set α))} (h : OrderedPair x y A) :

Theorem 3D #

If ⟨x, y⟩ ∈ A, then x and y belong to ⋃ ⋃ A.

theorem Enderton.Set.Chapter_3.theorem_3g_i {α : Type} {β : Type} {x : α} {F : Set.HRelation α β} (hF : Set.Relation.isOneToOne F) (hx : x Set.Relation.dom F) :
∃! (y : β), (x, y) F (y, x) Set.Relation.inv F

Theorem 3G (i) #

Assume that F is a one-to-one function. If x ∈ dom F, then F⁻¹(F(x)) = x.

theorem Enderton.Set.Chapter_3.theorem_3g_ii {α : Type} {β : Type} {y : β} {F : Set.HRelation α β} (hF : Set.Relation.isOneToOne F) (hy : y Set.Relation.ran F) :
∃! (x : α), (x, y) F (y, x) Set.Relation.inv F

Theorem 3G (ii) #

Assume that F is a one-to-one function. If y ∈ ran F, then F(F⁻¹(y)) = y.

Theorem 3H #

Assume that F and G are functions. Then

dom (F ∘ G) = {x ∈ dom G | G(x) ∈ dom F}.
theorem Enderton.Set.Chapter_3.theorem_3j_a {α : Type} {β : Type} {A : Set α} {B : Set β} {F : Set.HRelation α β} (hF : Set.Relation.mapsInto F A B) (hA : Set.Nonempty A) :
Set.Relation.isOneToOne F ∃ (G : Set.HRelation β α), Set.Relation.mapsInto G B A Set.Relation.comp G F = {p : α × α | p.1 A p.1 = p.2}

Theorem 3J (a) #

Assume that F : A → B, and that A is nonempty. There exists a function G : B → A (a "left inverse") such that G ∘ F is the identity function on A iff F is one-to-one.

theorem Enderton.Set.Chapter_3.theorem_3j_b {α : Type} {β : Type} {A : Set α} {B : Set β} {F : Set.HRelation α β} (hF : Set.Relation.mapsInto F A B) :
(∃ (H : Set.HRelation β α), Set.Relation.mapsInto H B A Set.Relation.comp F H = {p : β × β | p.1 B p.1 = p.2})Set.Relation.mapsOnto F A B

Theorem 3J (b) #

Assume that F : A → B, and that A is nonempty. There exists a function H : B → A (a "right inverse") such that F ∘ H is the identity function on B only if F maps A onto B.

theorem Enderton.Set.Chapter_3.theorem_3k_a {α : Type} {β : Type} {F : Set.HRelation α β} {𝓐 : Set (Set α)} :
Set.Relation.image F (⋃₀ 𝓐) = ⋃₀ {x : Set β | ∃ A ∈ 𝓐, Set.Relation.image F A = x}

Theorem 3K (a) #

The following hold for any sets. (F need not be a function.) The image of a union is the union of the images:

F⟦⋃ 𝓐⟧ = ⋃ {F⟦A⟧ | A ∈ 𝓐}

Theorem 3K (b) #

The following hold for any sets. (F need not be a function.) The image of an intersection is included in the intersection of the images:

F⟦⋂ 𝓐⟧ ⊆ ⋂ {F⟦A⟧ | A ∈ 𝓐}

Equality holds if F is single-rooted.

theorem Enderton.Set.Chapter_3.theorem_3k_b_i {α : Type} {β : Type} {F : Set.HRelation α β} {𝓐 : Set (Set α)} :
Set.Relation.image F (⋂₀ 𝓐) ⋂₀ {x : Set β | ∃ A ∈ 𝓐, Set.Relation.image F A = x}
theorem Enderton.Set.Chapter_3.theorem_3k_b_ii {α : Type} {β : Type} {F : Set.HRelation α β} {𝓐 : Set (Set α)} (hF : Set.Relation.isSingleRooted F) (h𝓐 : Set.Nonempty 𝓐) :
Set.Relation.image F (⋂₀ 𝓐) = ⋂₀ {x : Set β | ∃ A ∈ 𝓐, Set.Relation.image F A = x}

Theorem 3K (c) #

The following hold for any sets. (F need not be a function.) The image of a difference includes the difference of the images:

F⟦A⟧ - F⟦B⟧ ⊆ F⟦A - B⟧.

Equality holds if F is single-rooted.

Corollary 3L #

For any function G and sets A, B, and 𝓐:

G⁻¹⟦⋃ 𝓐⟧ = ⋃ {G⁻¹⟦A⟧ | A ∈ 𝓐},
G⁻¹⟦𝓐⟧ = ⋂ {G⁻¹⟦A⟧ | A ∈ 𝓐} for 𝓐 ≠ ∅,
G⁻¹⟦A - B⟧ = G⁻¹⟦A⟧ - G⁻¹⟦B⟧.
theorem Enderton.Set.Chapter_3.corollary_3l_i {β : Type} {α : Type} {G : Set.HRelation β α} {𝓐 : Set (Set α)} :
theorem Enderton.Set.Chapter_3.corollary_3l_ii {β : Type} {α : Type} {G : Set.HRelation β α} {𝓐 : Set (Set α)} (hG : Set.Relation.isSingleValued G) (h𝓐 : Set.Nonempty 𝓐) :

Theorem 3M #

If R is a symmetric and transitive relation, then R is an equivalence relation on fld R.

theorem Enderton.Set.Chapter_3.theorem_3r {α : Type u_1} {R : Rel α α} (hR : IsStrictTotalOrder α R) :
(∀ (x : α), ¬R x x) ∀ (x y : α), x yR x y R y x

Theorem 3R #

Let R be a linear ordering on A.

(i) There is no x for which xRx. (ii) For distinct x and y in A, either xRy or yRx.

theorem Enderton.Set.Chapter_3.exercise_3_1 {x : } {y : } {z : } {u : } {v : } {w : } (hx : x = 1) (hy : y = 1) (hz : z = 2) (hu : u = 1) (hv : v = 2) (hw : w = 2) :
{{x}, {x, y}, {x, y, z}} = {{u}, {u, v}, {u, v, w}} y v

Exercise 3.1 #

Suppose that we attempted to generalize the Kuratowski definitions of ordered pairs to ordered triples by defining

⟨x, y, z⟩* = {{x}, {x, y}, {x, y, z}}.open Set

Show that this definition is unsuccessful by giving examples of objects u, v, w, x, y, z with ⟨x, y, z⟩* = ⟨u, v, w⟩* but with either y ≠ v or z ≠ w (or both).

theorem Enderton.Set.Chapter_3.exercise_3_2a {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} {C : Set β} :
Set.prod A (B C) = Set.prod A B Set.prod A C

Exercise 3.2a #

Show that A × (B ∪ C) = (A × B) ∪ (A × C).

theorem Enderton.Set.Chapter_3.exercise_3_2b {α : Type u_1} {β : Type u_2} {A : Set α} {B : Set β} {C : Set β} (h : Set.prod A B = Set.prod A C) (hA : Set.Nonempty A) :
B = C

Exercise 3.2b #

Show that if A × B = A × C and A ≠ ∅, then B = C.

theorem Enderton.Set.Chapter_3.exercise_3_3 {α : Type u_1} {β : Type u_2} {A : Set (Set α)} {𝓑 : Set (Set β)} :
Set.prod A (⋃₀ 𝓑) = ⋃₀ {x : Set (Set α × β) | ∃ X ∈ 𝓑, Set.prod A X = x}

Exercise 3.3 #

Show that A × ⋃ 𝓑 = ⋃ {A × X | X ∈ 𝓑}.

theorem Enderton.Set.Chapter_3.exercise_3_5a {α : Type u_1} {β : Type u_2} {y : Set (α × β)} {A : Set α} {B : Set β} :
∃ (C : Set (Set (α × β))), y C ∃ x ∈ A, y = Set.prod {x} B

Exercise 3.5a #

Assume that A and B are given sets, and show that there exists a set C such that for any y,

y ∈ C ↔ y = {x} × B for some x in A.

In other words, show that {{x} × B | x ∈ A} is a set.

theorem Enderton.Set.Chapter_3.exercise_3_5b {α : Type u_1} {β : Type u_2} {A : Set α} (B : Set β) :
Set.prod A B = ⋃₀ {x : Set (α × β) | ∃ x_1 ∈ A, Set.prod {x_1} B = x}

Exercise 3.5b #

With A, B, and C as above, show that A × B = ∪ C.

Exercise 3.6 #

Show that a set A is a relation iff A ⊆ dom A × ran A.

Exercise 3.7 #

Show that if R is a relation, then fld R = ⋃ ⋃ R.

theorem Enderton.Set.Chapter_3.exercise_3_8_i {α : Type} {β : Type} {A : Set (Set.HRelation α β)} :
Set.Relation.dom (⋃₀ A) = ⋃₀ {x : Set α | ∃ R ∈ A, Set.Relation.dom R = x}

Exercise 3.8 (i) #

Show that for any set 𝓐:

dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
theorem Enderton.Set.Chapter_3.exercise_3_8_ii {α : Type} {β : Type} {A : Set (Set.HRelation α β)} :
Set.Relation.ran (⋃₀ A) = ⋃₀ {x : Set β | ∃ R ∈ A, Set.Relation.ran R = x}

Exercise 3.8 (ii) #

Show that for any set 𝓐:

ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
theorem Enderton.Set.Chapter_3.exercise_3_9_i {α : Type} {β : Type} {A : Set (Set.HRelation α β)} :
Set.Relation.dom (⋂₀ A) ⋂₀ {x : Set α | ∃ R ∈ A, Set.Relation.dom R = x}

Exercise 3.9 (i) #

Discuss the result of replacing the union operation by the intersection operation in the preceding problem.

dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
theorem Enderton.Set.Chapter_3.exercise_3_9_ii {α : Type} {β : Type} {A : Set (Set.HRelation α β)} :
Set.Relation.ran (⋂₀ A) ⋂₀ {x : Set β | ∃ R ∈ A, Set.Relation.ran R = x}

Exercise 3.9 (ii) #

Discuss the result of replacing the union operation by the intersection operation in the preceding problem.

ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
theorem Enderton.Set.Chapter_3.exercise_3_12 {α : Type} {β : Type} {f : Set.HRelation α β} {g : Set.HRelation α β} (hf : Set.Relation.isSingleValued f) :
Set.Relation.isSingleValued g(f g Set.Relation.dom f Set.Relation.dom g xSet.Relation.dom f, ∃! (y : β), (x, y) f (x, y) g)

Exercise 3.12 #

Assume that f and g are functions and show that

f ⊆ g ↔ dom f ⊆ dom g ∧ (∀ x ∈ dom f) f(x) = g(x).

Exercise 3.13 #

Assume that f and g are functions with f ⊆ g and dom g ⊆ dom f. Show that f = g.

Exercise 3.14 (a) #

Assume that f and g are functions. Show that f ∩ g is a function.

Exercise 3.14 (b) #

Assume that f and g are functions. Show that f ∪ g is a function iff f(x) = g(x) for every x in (dom f) ∩ (dom g).

theorem Enderton.Set.Chapter_3.exercise_3_15 {α : Type} {β : Type} {𝓐 : Set (Set.HRelation α β)} (h𝓐 : F𝓐, Set.Relation.isSingleValued F) (h : ∀ (F G : Set.HRelation α β), F 𝓐G 𝓐F G G F) :

Exercise 3.15 #

Let 𝓐 be a set of functions such that for any f and g in 𝓐, either f ⊆ g or g ⊆ f. Show that ⋃ 𝓐 is a function.

Exercise 3.17 #

Show that the composition of two single-rooted sets is again single-rooted. Conclude that the composition of two one-to-one functions is again one-to-one.

Exercise 3.18 #

Let R be the set

{⟨0, 1⟩, ⟨0, 2⟩, ⟨0, 3⟩, ⟨1, 2⟩, ⟨1, 3⟩, ⟨2, 3⟩}

Evaluate the following: R ∘ R, R ↾ {1}, R⁻¹ ↾ {1}, R⟦{1}⟧, and R⁻¹⟦{1}⟧.

theorem Enderton.Set.Chapter_3.exercise_3_18_i {R : Set.Relation } (hR : R = {(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)}) :
Set.Relation.comp R R = {(0, 2), (0, 3), (1, 3)}
theorem Enderton.Set.Chapter_3.exercise_3_18_ii {R : Set.Relation } (hR : R = {(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)}) :
Set.Relation.restriction R {1} = {(1, 2), (1, 3)}
theorem Enderton.Set.Chapter_3.exercise_3_18_iii {R : Set.Relation } (hR : R = {(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)}) :
theorem Enderton.Set.Chapter_3.exercise_3_18_iv {R : Set.Relation } (hR : R = {(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)}) :
Set.Relation.image R {1} = {2, 3}
theorem Enderton.Set.Chapter_3.exercise_3_18_v {R : Set.Relation } (hR : R = {(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)}) :

Exercise 3.19 #

Let

A = {⟨∅, {∅, {∅}}⟩, ⟨{∅}, ∅⟩}.

Evaluate each of the following: A(∅), A⟦∅⟧, A⟦{∅}⟧, A⟦{∅, {∅}}⟧, A⁻¹, A ∘ A, A ↾ ∅, A ↾ {∅, {∅}}, ⋃ ⋃ A.

theorem Enderton.Set.Chapter_3.exercise_3_19_i {α : Type} {A : Set.Relation (Set (Set (Set α)))} (hA : A = {(, {, {}}), ({}, )}) :
(, {, {}}) A
theorem Enderton.Set.Chapter_3.exercise_3_19_iii {α : Type} {A : Set.Relation (Set (Set (Set α)))} (hA : A = {(, {, {}}), ({}, )}) :
theorem Enderton.Set.Chapter_3.exercise_3_19_iv {α : Type} {A : Set.Relation (Set (Set (Set α)))} (hA : A = {(, {, {}}), ({}, )}) :
theorem Enderton.Set.Chapter_3.exercise_3_19_v {α : Type} {A : Set.Relation (Set (Set (Set α)))} (hA : A = {(, {, {}}), ({}, )}) :
Set.Relation.inv A = {({, {}}, ), (, {})}
theorem Enderton.Set.Chapter_3.exercise_3_19_vi {α : Type} {A : Set.Relation (Set (Set (Set α)))} (hA : A = {(, {, {}}), ({}, )}) :
Set.Relation.comp A A = {({}, {, {}})}
theorem Enderton.Set.Chapter_3.exercise_3_19_viii {α : Type} {A : Set.Relation (Set (Set (Set α)))} (hA : A = {(, {, {}}), ({}, )}) :
theorem Enderton.Set.Chapter_3.exercise_3_19_ix {α : Type} {A : Set.Relation (Set (Set (Set α)))} (hA : A = {(, {, {}}), ({}, )}) :

Exercise 3.20 #

Show that F ↾ A = F ∩ (A × ran F).

theorem Enderton.Set.Chapter_3.exercise_3_22_a {α : Type} {β : Type} {A : Set α} {B : Set α} {F : Set.HRelation α β} (h : A B) :

Exercise 3.22 (a) #

Show that the following is correct for any sets.

A ⊆ B → F⟦A⟧ ⊆ F⟦B⟧

Exercise 3.22 (b) #

Show that the following is correct for any sets.

(F ∘ G)⟦A⟧ = F⟦G⟦A⟧⟧

Exercise 3.22 (c) #

Show that the following is correct for any sets.

Q ↾ (A ∪ B) = (Q ↾ A) ∪ (Q ↾ B)
theorem Enderton.Set.Chapter_3.exercise_3_23_i {α : Type} {β : Type} {A : Set α} {B : Set.HRelation α β} {I : Set.Relation α} (hI : I = {p : α × α | p.1 A p.1 = p.2}) :

Exercise 3.23 (i) #

Let I be the identity function on the set A. Show that for any sets B and C, B ∘ I = B ↾ A.

theorem Enderton.Set.Chapter_3.exercise_3_23_ii {α : Type} {A : Set α} {C : Set α} {I : Set.Relation α} (hI : I = {p : α × α | p.1 A p.1 = p.2}) :

Exercise 3.23 (ii) #

Let I be the identity function on the set A. Show that for any sets B and C, I⟦C⟧ = A ∩ C.

theorem Enderton.Set.Chapter_3.exercise_3_24 {α : Type} {β : Type} {F : Set.HRelation α β} {A : Set β} (hF : Set.Relation.isSingleValued F) :
Set.Relation.image (Set.Relation.inv F) A = {x : α | x Set.Relation.dom F ∃! (y : β), (x, y) F y A}

Exercise 3.24 #

Show that for a function F, F⁻¹⟦A⟧ = { x ∈ dom F | F(x) ∈ A }.

Exercise 3.25 (b) #

Show that the result of part (a) holds for any function G, not necessarily one-to-one.

Exercise 3.25 (a) #

Assume that G is a one-to-one function. Show that G ∘ G⁻¹ is the identity function on ran G.

Exercise 3.27 #

Show that dom (F ∘ G) = G⁻¹⟦dom F⟧ for any sets F and G. (F and G need not be functions.)

theorem Enderton.Set.Chapter_3.exercise_3_28 {α : Type} {β : Type} {A : Set α} {B : Set β} {f : Set.HRelation α β} {G : Set.HRelation (Set α) (Set β)} (hf : Set.Relation.isOneToOne f Set.Relation.mapsInto f A B) (hG : G = {p : Set α × Set β | p.1 𝒫 A p.2 = Set.Relation.image f p.1}) :

Exercise 3.28 #

Assume that f is a one-to-one function from A into B, and that G is the function with dom G = 𝒫 A defined by the equation G(X) = f⟦X⟧. Show that G maps 𝒫 A one-to-one into 𝒫 B.

theorem Enderton.Set.Chapter_3.exercise_3_29 {α : Type} {β : Type} {f : Set.HRelation α β} {G : Set.HRelation β (Set α)} {A : Set α} {B : Set β} (hf : Set.Relation.mapsOnto f A B) (hG : Set.Relation.mapsInto G B (𝒫 A) G = {p : β × Set α | p.1 B p.2 = {x : α | x A (x, p.1) f}}) :

Exercise 3.29 #

Assume that f : A → B and define a function G : B → 𝒫 A by

G(b) = {x ∈ A | f(x) = b}

Show that if f maps A onto B, then G is one-to-one. Does the converse hold?

Exercise 3.30 #

Assume that F : 𝒫 A → 𝒫 A and that F has the monotonicity property:

X ⊆ Y ⊆ A → F(X) ⊆ F(Y).

Define B = ⋂ {X ⊆ A | F(X) ⊆ X} and C = ⋃ {X ⊆ A | X ⊆ F(X)}.

theorem Enderton.Set.Chapter_3.exercise_3_30_a {α : Type u_1} {F : Set αSet α} {A : Set α} {B : Set α} {C : Set α} (hF : Set.MapsTo F (𝒫 A) (𝒫 A)) (hMono : ∀ (X Y : Set α), X Y Y AF X F Y) (hB : B = ⋂₀ {X : Set α | X A F X X}) (hC : C = ⋃₀ {X : Set α | X A X F X}) :
F B = B F C = C

Exercise 3.30 (a) #

Show that F(B) = B and F(C) = C.

theorem Enderton.Set.Chapter_3.exercise_3_30_b {α : Type u_1} {F : Set αSet α} {A : Set α} {B : Set α} {C : Set α} (hB : B = ⋂₀ {X : Set α | X A F X X}) (hC : C = ⋃₀ {X : Set α | X A X F X}) (X : Set α) :
X A F X = XB X X C

Exercise 3.30 (b) #

Show that if F(X) = X, then B ⊆ X ⊆ C.

Exercise 3.32 (a) #

Show that R is symmetric iff R⁻¹ ⊆ R.

Exercise 3.32 (b) #

Show that R is transitive iff R ∘ R ⊆ R.

Exercise 3.33 #

Show that R is a symmetric and transitive relation iff R = R⁻¹ ∘ R.

Exercise 3.34 (a) #

Assume that 𝓐 is a nonempty set, every member of which is a transitive relation. Is the set ⋂ 𝓐 a transitive relation?

theorem Enderton.Set.Chapter_3.exercise_3_34_b {𝓐 : Set (Set.Relation )} :
Set.Nonempty 𝓐𝓐 = {{(1, 2), (2, 3), (1, 3)}, {(2, 1)}}(A𝓐, Set.Relation.isTransitive A) ¬Set.Relation.isTransitive (⋃₀ 𝓐)

Exercise 3.34 (b) #

Assume that 𝓐 is a nonempty set, every member of which is a transitive relation. Is ⋃ 𝓐 a transitive relation?

Exercise 3.35 #

Show that for any R and x, we have [x]_R = R⟦{x}⟧.

theorem Enderton.Set.Chapter_3.exercise_3_36 {α : Type} {β : Type} {f : Set.HRelation α β} {Q : Set.Relation α} {R : Set.Relation β} {A : Set α} {B : Set β} (hf : Set.Relation.mapsInto f A B) (hR : Set.Relation.isEquivalence R B) (hQ : Q = {p : α × α | ∃ (fx : β) (fy : β), (p.1, fx) f (p.2, fy) f (fx, fy) R}) :

Exercise 3.36 #

Assume that f : A → B and that R is an equivalence relation on B. Define Q to be the set {⟨x, y⟩ ∈ A × A | ⟨f(x), f(y)⟩ ∈ R}. Show that Q is an equivalence relation on A.

theorem Enderton.Set.Chapter_3.exercise_3_37 {α : Type} {P : Set (Set α)} {A : Set α} (hP : Set.Relation.Partition P A) (Rₚ : Set.Relation α) (hRₚ : ∀ (x y : α), (x, y) Rₚ ∃ B ∈ P, x B y B) :

Exercise 3.37 #

Assume that P is a partition of a set A. Define the relation Rₚ as follows:

xRₚy ↔ (∃ B ∈ Π)(x ∈ B ∧ y ∈ B).

Show that Rₚ is an equivalence relation on A. (This is a formalized version of the discussion at the beginning of this section.)

theorem Enderton.Set.Chapter_3.exercise_3_38 {α : Type} {P : Set (Set α)} {A : Set α} (hP : Set.Relation.Partition P A) (Rₚ : Set.Relation α) (hRₚ : ∀ (x y : α), (x, y) Rₚ ∃ B ∈ P, x B y B) :

Exercise 3.38 #

Theorem 3P shows that A / R is a partition of A whenever R is an equivalence relation on A. Show that if we start with the equivalence relation Rₚ of the preceding exercise, then the partition A / Rₚ is just P.

theorem Enderton.Set.Chapter_3.exercise_3_39 {α : Type} {P : Set (Set α)} {R : Set.Relation α} {Rₚ : Set.Relation α} {A : Set α} (hR : Set.Relation.isEquivalence R A) (hP : P = Set.Relation.modEquiv hR) (hRₚ : ∀ (x y : α), (x, y) Rₚ ∃ B ∈ P, x B y B) :
Rₚ = R

Exercise 3.39 #

Assume that we start with an equivalence relation R on A and define P to be the partition A / R. Show that Rₚ, as defined in Exercise 37, is just R.

theorem Enderton.Set.Chapter_3.exercise_3_41_a {Q : Set.Relation ( × )} (hQ : ∀ (u v x y : ), ((u, v), x, y) Q u + y = x + v) :

Exercise 3.41 (a) #

Let be the set of real numbers and define the realtion Q on ℝ × ℝ by ⟨u, v⟩ Q ⟨x, y⟩ iff u + y = x + v. Show that Q is an equivalence relation on ℝ × ℝ.

Exercise 3.43 #

Assume that R is a linear ordering on a set A. Show that R⁻¹ is also a linear ordering on A.

Exercise 3.44 #

Assume that < is a linear ordering on a set A. Assume that f : A → A and that f has the property that whenever x < y, then f(x) < f(y). Show that f is one-to-one and that whenever f(x) < f(y), then x < y.

theorem Enderton.Set.Chapter_3.exercise_3_44_i {α : Type u_1} {R : Rel α α} (hR : IsStrictTotalOrder α R) (f : αα) (hf : ∀ (x y : α), R x yR (f x) (f y)) :
theorem Enderton.Set.Chapter_3.exercise_3_44_ii {α : Type u_1} {x : α} {y : α} {R : Rel α α} (hR : IsStrictTotalOrder α R) (f : αα) (hf : ∀ (x y : α), R x yR (f x) (f y)) :
R (f x) (f y)R x y
theorem Enderton.Set.Chapter_3.exercise_3_45 {α : Type u_1} {β : Type u_2} {A : Rel α α} {B : Rel β β} {R : Rel (α × β) (α × β)} (hA : IsStrictTotalOrder α A) (hB : IsStrictTotalOrder β B) (hR : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), R (a₁, b₁) (a₂, b₂) A a₁ a₂ a₁ = a₂ B b₁ b₂) :

Exercise 3.45 #

Assume that <_A and <_B are linear orderings on A and B, respectively. Define the binary relation <_L on the Cartesian product A × B by:

⟨a₁, b₁⟩ <_L ⟨a₂, b₂⟩ iff either a₁ <_A a₂ or (a₁ = a₂ ∧ b₁ <_B b₂).

Show that <_L is a linear ordering on A × B. (The relation <_L is called lexicographic ordering, being the ordering used in making dictionaries.)