inductive Chapter11.BoundedInterval : Type

• Ioo (a b : ℝ) : BoundedInterval
• Icc (a b : ℝ) : BoundedInterval
• Ioc (a b : ℝ) : BoundedInterval
• Ico (a b : ℝ) : BoundedInterval

def Chapter11.BoundedInterval.toSet (I : BoundedInterval) : Set ℝ

There is a technical issue in that this coercion is not injective: the empty set is represented by multiple bounded intervals. This causes some of the statements in this section to be a little uglier than necessary.

Equations

• ↑(Chapter11.BoundedInterval.Ioo a b) = Set.Ioo a b
• ↑(Chapter11.BoundedInterval.Icc a b) = Set.Icc a b
• ↑(Chapter11.BoundedInterval.Ioc a b) = Set.Ioc a b
• ↑(Chapter11.BoundedInterval.Ico a b) = Set.Ico a b

@[implicit_reducible]

instance Chapter11.BoundedInterval.inst_coeSet : Coe BoundedInterval (Set ℝ)

Equations

• Chapter11.BoundedInterval.inst_coeSet = { coe := Chapter11.BoundedInterval.toSet }

@[implicit_reducible]

instance Chapter11.BoundedInterval.instEmpty : EmptyCollection BoundedInterval

Equations

• Chapter11.BoundedInterval.instEmpty = { emptyCollection := Chapter11.BoundedInterval.Ioo 0 0 }

@[simp]

theorem Chapter11.BoundedInterval.coe_empty : ↑∅ = ∅

@[implicit_reducible]

noncomputable instance Chapter11.BoundedInterval.decidableEq : DecidableEq BoundedInterval

This is to make Finsets of BoundedIntervals work properly

Equations

• Chapter11.BoundedInterval.decidableEq = instDecidableEqOfLawfulBEq

@[simp]

theorem Chapter11.BoundedInterval.set_Ioo (a b : ℝ) : ↑(Ioo a b) = Set.Ioo a b

@[simp]

theorem Chapter11.BoundedInterval.set_Icc (a b : ℝ) : ↑(Icc a b) = Set.Icc a b

@[simp]

theorem Chapter11.BoundedInterval.set_Ioc (a b : ℝ) : ↑(Ioc a b) = Set.Ioc a b

@[simp]

theorem Chapter11.BoundedInterval.set_Ico (a b : ℝ) : ↑(Ico a b) = Set.Ico a b

theorem Chapter11.Bornology.IsBounded.of_boundedInterval (I : BoundedInterval) : Bornology.IsBounded ↑I

Lemma 11.1.4 / Exercise 11.1.1

theorem Chapter11.BoundedInterval.ordConnected_iff (X : Set ℝ) : Bornology.IsBounded X ∧ X.OrdConnected ↔ ∃ (I : BoundedInterval), X = ↑I

theorem Chapter11.BoundedInterval.inter (I J : BoundedInterval) : ∃ (K : BoundedInterval), ↑I ∩ ↑J = ↑K

Corollary 11.1.6 / Exercise 11.1.2

@[implicit_reducible]

noncomputable instance Chapter11.BoundedInterval.instInter : Inter BoundedInterval

Equations

• Chapter11.BoundedInterval.instInter = { inter := fun (I J : Chapter11.BoundedInterval) => ⋯.choose }

@[simp]

theorem Chapter11.BoundedInterval.inter_eq (I J : BoundedInterval) : ↑(I ∩ J) = ↑I ∩ ↑J

@[implicit_reducible]

instance Chapter11.BoundedInterval.instMembership : Membership ℝ BoundedInterval

Equations

• Chapter11.BoundedInterval.instMembership = { mem := fun (I : Chapter11.BoundedInterval) (x : ℝ) => x ∈ ↑I }

theorem Chapter11.BoundedInterval.mem_iff (I : BoundedInterval) (x : ℝ) : x ∈ I ↔ x ∈ ↑I

@[implicit_reducible]

instance Chapter11.BoundedInterval.instSubset : HasSubset BoundedInterval

Equations

• Chapter11.BoundedInterval.instSubset = { Subset := fun (I J : Chapter11.BoundedInterval) => ∀ x ∈ I, x ∈ J }

theorem Chapter11.BoundedInterval.subset_iff (I J : BoundedInterval) : I ⊆ J ↔ ↑I ⊆ ↑J

@[reducible, inline]

abbrev Chapter11.BoundedInterval.a (I : BoundedInterval) : ℝ

Equations

• (Chapter11.BoundedInterval.Ioo a b).a = a
• (Chapter11.BoundedInterval.Icc a b).a = a
• (Chapter11.BoundedInterval.Ioc a b).a = a
• (Chapter11.BoundedInterval.Ico a b).a = a

@[reducible, inline]

abbrev Chapter11.BoundedInterval.b (I : BoundedInterval) : ℝ

Equations

• (Chapter11.BoundedInterval.Ioo a b).b = b
• (Chapter11.BoundedInterval.Icc a b).b = b
• (Chapter11.BoundedInterval.Ioc a b).b = b
• (Chapter11.BoundedInterval.Ico a b).b = b

theorem Chapter11.BoundedInterval.subset_Icc (I : BoundedInterval) : I ⊆ Icc I.a I.b

theorem Chapter11.BoundedInterval.Ioo_subset (I : BoundedInterval) : Ioo I.a I.b ⊆ I

instance Chapter11.BoundedInterval.instTrans : IsTrans BoundedInterval fun (x1 x2 : BoundedInterval) => x1 ⊆ x2

@[simp]

theorem Chapter11.BoundedInterval.mem_inter (I J : BoundedInterval) (x : ℝ) : x ∈ I ∩ J ↔ x ∈ I ∧ x ∈ J

@[reducible, inline]

abbrev Chapter11.BoundedInterval.length (I : BoundedInterval) : ℝ

Equations

• I.length = max (I.b - I.a) 0

def Chapter11.«term|___|ₗ» : Lean.ParserDescr

Using ||ₗ subscript here to not override ||

Equations

• One or more equations did not get rendered due to their size.

theorem Chapter11.BoundedInterval.length_nonneg (I : BoundedInterval) : 0 ≤ I.length

theorem Chapter11.BoundedInterval.empty_of_lt {I : BoundedInterval} (h : I.b < I.a) : ↑I = ∅

theorem Chapter11.BoundedInterval.length_of_empty {I : BoundedInterval} (hI : ↑I = ∅) : I.length = 0

theorem Chapter11.BoundedInterval.length_of_subsingleton {I : BoundedInterval} : Subsingleton ↑↑I ↔ I.length = 0

theorem Chapter11.BoundedInterval.dist_le_length {I : BoundedInterval} {x y : ℝ} (hx : x ∈ I) (hy : y ∈ I) : |x - y| ≤ I.length

@[reducible, inline]

abbrev Chapter11.BoundedInterval.joins (K I J : BoundedInterval) : Prop

Equations

• K.joins I J = (↑I ∩ ↑J = ∅ ∧ ↑K = ↑I ∪ ↑J ∧ K.length = I.length + J.length)

theorem Chapter11.BoundedInterval.join_Icc_Ioc {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) : (Icc a c).joins (Icc a b) (Ioc b c)

theorem Chapter11.BoundedInterval.join_Icc_Ioo {a b c : ℝ} (hab : a ≤ b) (hbc : b < c) : (Ico a c).joins (Icc a b) (Ioo b c)

theorem Chapter11.BoundedInterval.join_Ioc_Ioc {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) : (Ioc a c).joins (Ioc a b) (Ioc b c)

theorem Chapter11.BoundedInterval.join_Ioc_Ioo {a b c : ℝ} (hab : a ≤ b) (hbc : b < c) : (Ioo a c).joins (Ioc a b) (Ioo b c)

theorem Chapter11.BoundedInterval.join_Ico_Icc {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) : (Icc a c).joins (Ico a b) (Icc b c)

theorem Chapter11.BoundedInterval.join_Ico_Ico {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) : (Ico a c).joins (Ico a b) (Ico b c)

theorem Chapter11.BoundedInterval.join_Ioo_Icc {a b c : ℝ} (hab : a < b) (hbc : b ≤ c) : (Ioc a c).joins (Ioo a b) (Icc b c)

theorem Chapter11.BoundedInterval.join_Ioo_Ico {a b c : ℝ} (hab : a < b) (hbc : b ≤ c) : (Ioo a c).joins (Ioo a b) (Ico b c)

structure Chapter11.Partition (I : BoundedInterval) : Type

• intervals : Finset BoundedInterval
• exists_unique (x : ℝ) (hx : x ∈ I) : ∃! J : BoundedInterval, J ∈ self.intervals ∧ x ∈ J
• contains (J : BoundedInterval) (hJ : J ∈ self.intervals) : J ⊆ I

theorem Chapter11.Partition.ext {I : BoundedInterval} {x y : Partition I} (intervals : x.intervals = y.intervals) : x = y

theorem Chapter11.Partition.ext_iff {I : BoundedInterval} {x y : Partition I} : x = y ↔ x.intervals = y.intervals

@[implicit_reducible]

instance Chapter11.Partition.instMembership (I : BoundedInterval) : Membership BoundedInterval (Partition I)

Equations

• Chapter11.Partition.instMembership I = { mem := fun (P : Chapter11.Partition I) (J : Chapter11.BoundedInterval) => J ∈ P.intervals }

@[implicit_reducible]

instance Chapter11.Partition.instBot (I : BoundedInterval) : Bot (Partition I)

Equations

• Chapter11.Partition.instBot I = { bot := { intervals := {I}, exists_unique := ⋯, contains := ⋯ } }

@[simp]

theorem Chapter11.Partition.intervals_of_bot (I : BoundedInterval) : ⊥.intervals = {I}

@[reducible, inline]

noncomputable abbrev Chapter11.Partition.join {I J K : BoundedInterval} (P : Partition I) (Q : Partition J) (h : K.joins I J) : Partition K

Equations

• P.join Q h = { intervals := P.intervals ∪ Q.intervals, exists_unique := ⋯, contains := ⋯ }

@[simp]

theorem Chapter11.Partition.intervals_of_join {I J K : BoundedInterval} {h : K.joins I J} (P : Partition I) (Q : Partition J) : (P.join Q h).intervals = P.intervals ∪ Q.intervals

@[reducible, inline]

noncomputable abbrev Chapter11.Partition.add_empty {I : BoundedInterval} (P : Partition I) : Partition I

Equations

• P.add_empty = { intervals := P.intervals ∪ {∅}, exists_unique := ⋯, contains := ⋯ }

@[reducible, inline]

noncomputable abbrev Chapter11.Partition.remove_empty {I : BoundedInterval} (P : Partition I) : Partition I

Equations

• P.remove_empty = { intervals := {J ∈ P.intervals | (↑J).Nonempty}, exists_unique := ⋯, contains := ⋯ }

@[simp]

theorem Chapter11.Partition.intervals_of_add_empty (I : BoundedInterval) (P : Partition I) : P.add_empty.intervals = P.intervals ∪ {∅}

theorem Chapter11.Partition.exist_right {I : BoundedInterval} (hI : I.a < I.b) (hI' : I.b ∉ I) {P : Partition I} : ∃ c ∈ Set.Ico I.a I.b, BoundedInterval.Ioo c I.b ∈ P ∨ BoundedInterval.Ico c I.b ∈ P

Exercise 11.1.3. The exercise only claims c ≤ b, but the stronger claim c < b is true and useful.

theorem Chapter11.Partition.sum_of_length (I : BoundedInterval) (P : Partition I) : ∑ J ∈ P.intervals, J.length = I.length

Theorem 11.1.13 (Length is finitely additive).

@[implicit_reducible]

instance Chapter11.Partition.instLE (I : BoundedInterval) : LE (Partition I)

Definition 11.1.14 (Finer and coarser partitions)

Equations

• Chapter11.Partition.instLE I = { le := fun (P P' : Chapter11.Partition I) => ∀ J ∈ P'.intervals, ∃ K ∈ P, J ⊆ K }

@[implicit_reducible]

instance Chapter11.Partition.instPreOrder (I : BoundedInterval) : Preorder (Partition I)

Equations

• Chapter11.Partition.instPreOrder I = { toLE := Chapter11.Partition.instLE I, lt := fun (a b : Chapter11.Partition I) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[implicit_reducible]

instance Chapter11.Partition.instOrderBot (I : BoundedInterval) : OrderBot (Partition I)

Equations

• Chapter11.Partition.instOrderBot I = { toBot := Chapter11.Partition.instBot I, bot_le := ⋯ }

@[implicit_reducible]

noncomputable instance Chapter11.Partition.instMax (I : BoundedInterval) : Max (Partition I)

Definition 11.1.16 (Common refinement)

Equations

• One or more equations did not get rendered due to their size.

theorem Chapter11.BoundedInterval.le_max {I : BoundedInterval} (P P' : Partition I) : P ≤ P ⊔ P' ∧ P' ≤ P ⊔ P'

Lemma 11.1.8 / Exercise 11.1.4

theorem Chapter11.BoundedInterval.max_le_iff (I : BoundedInterval) {P P' P'' : Partition I} {hP : P ≤ P''} {hP' : P' ≤ P''} : P ⊔ P' ≤ P''

Not from textbook: the reverse inclusion