bookshelf/Bookshelf/Enderton/Set/Chapter_1.lean

133 lines
3.3 KiB
Plaintext
Raw Normal View History

import Mathlib.Init.Set
2023-05-18 22:02:15 +00:00
import Mathlib.Data.Set.Basic
import Mathlib.Tactic.LibrarySearch
/-! # Enderton.Chapter_1
Introduction
-/
namespace Enderton.Set.Chapter_1
2023-05-19 15:25:37 +00:00
/-! ### Exercise 1.1
2023-05-18 22:02:15 +00:00
Which of the following become true when "∈" is inserted in place of the blank?
Which become true when "⊆" is inserted?
-/
/--
The `∅` does not equal the singleton set containing `∅`.
-/
lemma empty_ne_singleton_empty (h : ∅ = ({∅} : Set (Set α))) : False :=
absurd h (Ne.symm $ Set.singleton_ne_empty (∅ : Set α))
2023-05-19 15:25:37 +00:00
/-- #### Exercise 1.1a
2023-05-18 22:02:15 +00:00
`{∅} ___ {∅, {∅}}`
-/
2023-05-19 15:25:37 +00:00
theorem exercise_1_1a
2023-05-18 22:02:15 +00:00
: {∅} ∈ ({∅, {∅}} : Set (Set (Set α)))
∧ {∅} ⊆ ({∅, {∅}} : Set (Set (Set α))) := ⟨by simp, by simp⟩
2023-05-19 15:25:37 +00:00
/-- #### Exercise 1.1b
2023-05-18 22:02:15 +00:00
`{∅} ___ {∅, {{∅}}}`
-/
2023-05-19 15:25:37 +00:00
theorem exercise_1_1b
2023-05-18 22:02:15 +00:00
: {∅} ∉ ({∅, {{∅}}}: Set (Set (Set (Set α))))
∧ {∅} ⊆ ({∅, {{∅}}}: Set (Set (Set (Set α)))) := by
refine ⟨?_, by simp⟩
intro h
simp at h
exact empty_ne_singleton_empty h
2023-05-19 15:25:37 +00:00
/-- #### Exercise 1.1c
2023-05-18 22:02:15 +00:00
`{{∅}} ___ {∅, {∅}}`
-/
2023-05-19 15:25:37 +00:00
theorem exercise_1_1c
2023-05-18 22:02:15 +00:00
: {{∅}} ∉ ({∅, {∅}} : Set (Set (Set (Set α))))
∧ {{∅}} ⊆ ({∅, {∅}} : Set (Set (Set (Set α)))) := ⟨by simp, by simp⟩
2023-05-19 15:25:37 +00:00
/-- #### Exercise 1.1d
2023-05-18 22:02:15 +00:00
`{{∅}} ___ {∅, {{∅}}}`
-/
2023-05-19 15:25:37 +00:00
theorem exercise_1_1d
2023-05-18 22:02:15 +00:00
: {{∅}} ∈ ({∅, {{∅}}} : Set (Set (Set (Set α))))
∧ ¬ {{∅}} ⊆ ({∅, {{∅}}} : Set (Set (Set (Set α)))) := by
refine ⟨by simp, ?_⟩
intro h
simp at h
exact empty_ne_singleton_empty h
2023-05-19 15:25:37 +00:00
/-- #### Exercise 1.1e
2023-05-18 22:02:15 +00:00
`{{∅}} ___ {∅, {∅, {∅}}}`
-/
2023-05-19 15:25:37 +00:00
theorem exercise_1_1e
2023-05-18 22:02:15 +00:00
: {{∅}} ∉ ({∅, {∅, {∅}}} : Set (Set (Set (Set α))))
∧ ¬ {{∅}} ⊆ ({∅, {∅, {∅}}} : Set (Set (Set (Set α)))) := by
apply And.intro
· intro h
simp at h
rw [Set.ext_iff] at h
have nh := h ∅
simp at nh
exact empty_ne_singleton_empty nh
· intro h
simp at h
rw [Set.ext_iff] at h
have nh := h {∅}
simp at nh
2023-05-19 15:25:37 +00:00
/-- ### Exercise 1.2
2023-05-18 22:02:15 +00:00
Show that no two of the three sets `∅`, `{∅}`, and `{{∅}}` are equal to each
other.
-/
2023-05-19 15:25:37 +00:00
theorem exercise_1_2
2023-05-18 22:02:15 +00:00
: ∅ ≠ ({∅} : Set (Set α))
∧ ∅ ≠ ({{∅}} : Set (Set (Set α)))
∧ {∅} ≠ ({{∅}} : Set (Set (Set α))) := by
refine ⟨?_, ⟨?_, ?_⟩⟩
· intro h
exact empty_ne_singleton_empty h
· intro h
exact absurd h (Ne.symm $ Set.singleton_ne_empty ({∅} : Set (Set α)))
· intro h
simp at h
exact empty_ne_singleton_empty h
2023-05-19 15:25:37 +00:00
/-- ### Exercise 1.3
2023-05-18 22:02:15 +00:00
Show that if `B ⊆ C`, then `𝓟 B ⊆ 𝓟 C`.
-/
2023-05-19 15:25:37 +00:00
theorem exercise_1_3 (h : B ⊆ C) : Set.powerset B ⊆ Set.powerset C := by
2023-05-18 22:02:15 +00:00
unfold Set.powerset
simp
intro x hx
exact Set.Subset.trans hx h
2023-05-19 15:25:37 +00:00
/-- ### Exercise 1.4
2023-05-18 22:02:15 +00:00
Assume that `x` and `y` are members of a set `B`. Show that
`{{x}, {x, y}} ∈ 𝓟 𝓟 B`.
-/
2023-05-19 15:25:37 +00:00
theorem exercise_1_4 (x y : α) (hx : x ∈ B) (hy : y ∈ B)
2023-05-18 22:02:15 +00:00
: {{x}, {x, y}} ∈ Set.powerset (Set.powerset B) := by
unfold Set.powerset
simp only [Set.mem_singleton_iff, Set.mem_setOf_eq]
rw [Set.subset_def]
intro z hz
simp at hz
apply Or.elim hz
· intro h
rwa [h, Set.mem_setOf_eq, Set.singleton_subset_iff]
· intro h
rw [h, Set.mem_setOf_eq]
exact Set.union_subset
(Set.singleton_subset_iff.mpr hx)
(Set.singleton_subset_iff.mpr hy)
end Enderton.Set.Chapter_1