1. Analysis
  2. 11.1. Partitions
Imports
import Mathlib.Tactic

Analysis I, Section 11.1: Partitions

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

  • Bounded intervals and partitions.

  • Length of an interval; the lengths of a partition sum to the length of the interval.

namespace Chapter11inductive BoundedInterval where | Ioo (a b:ℝ) : BoundedInterval | Icc (a b:ℝ) : BoundedInterval | Ioc (a b:ℝ) : BoundedInterval | Ico (a b:ℝ) : BoundedIntervalopen BoundedInterval

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.

@[coe] def BoundedInterval.toSet (I: BoundedInterval) : Set ℝ := match I with | Ioo a b => .Ioo a b | Icc a b => .Icc a b | Ioc a b => .Ioc a b | Ico a b => .Ico a b
instance BoundedInterval.inst_coeSet : Coe BoundedInterval (Set ℝ) where coe := toSetinstance BoundedInterval.instEmpty : EmptyCollection BoundedInterval where emptyCollection := Ioo 0 0@[simp] theorem BoundedInterval.coe_empty : ((∅ : BoundedInterval):Set ℝ) = ∅ := ⊢ ↑∅ = ∅ All goals completed! 🐙

This is to make Finsets of BoundedIntervals work properly

open Classical innoncomputable instance BoundedInterval.decidableEq : DecidableEq BoundedInterval := instDecidableEqOfLawfulBEq
@[simp] theorem BoundedInterval.set_Ioo (a b:ℝ) : (Ioo a b : Set ℝ) = .Ioo a b := a:ℝb:ℝ⊢ ↑(Ioo a b) = Set.Ioo a b All goals completed! 🐙@[simp] theorem BoundedInterval.set_Icc (a b:ℝ) : (Icc a b : Set ℝ) = .Icc a b := a:ℝb:ℝ⊢ ↑(Icc a b) = Set.Icc a b All goals completed! 🐙@[simp] theorem BoundedInterval.set_Ioc (a b:ℝ) : (Ioc a b : Set ℝ) = .Ioc a b := a:ℝb:ℝ⊢ ↑(Ioc a b) = Set.Ioc a b All goals completed! 🐙@[simp] theorem BoundedInterval.set_Ico (a b:ℝ) : (Ico a b : Set ℝ) = .Ico a b := a:ℝb:ℝ⊢ ↑(Ico a b) = Set.Ico a b All goals completed! 🐙-- Definition 11.1.1 Set.ordConnected_def.{u_1} {α : Type u_1} [Preorder α] {s : Set α} : s.OrdConnected ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.Icc x y ⊆ s#check Set.ordConnected_def/-- Examples 11.1.3 -/ declaration uses `sorry`example : (Set.Icc 1 2 : Set ℝ).OrdConnected := ⊢ (Set.Icc 1 2).OrdConnected All goals completed! 🐙declaration uses `sorry`example : (Set.Ioo 1 2 : Set ℝ).OrdConnected := ⊢ (Set.Ioo 1 2).OrdConnected All goals completed! 🐙declaration uses `sorry`example : ¬(Set.Icc 1 2 ∪ Set.Icc 3 4 : Set ℝ).OrdConnected := ⊢ ¬(Set.Icc 1 2 ∪ Set.Icc 3 4).OrdConnected All goals completed! 🐙declaration uses `sorry`example : (∅:Set ℝ).OrdConnected := ⊢ ∅.OrdConnected All goals completed! 🐙declaration uses `sorry`example (x:ℝ) : ({x}: Set ℝ).OrdConnected := x:ℝ⊢ {x}.OrdConnected All goals completed! 🐙

Lemma 11.1.4 / Exercise 11.1.1

theorem declaration uses `sorry`Bornology.IsBounded.of_boundedInterval (I: BoundedInterval) : Bornology.IsBounded (I:Set ℝ) := I:BoundedInterval⊢ Bornology.IsBounded ↑I All goals completed! 🐙
theorem declaration uses `sorry`BoundedInterval.ordConnected_iff (X:Set ℝ) : Bornology.IsBounded X ∧ X.OrdConnected ↔ ∃ I: BoundedInterval, X = I := X:Set ℝ⊢ Bornology.IsBounded X ∧ X.OrdConnected ↔ ∃ I, X = ↑I All goals completed! 🐙

Corollary 11.1.6 / Exercise 11.1.2

theorem declaration uses `sorry`BoundedInterval.inter (I J: BoundedInterval) : ∃ K : BoundedInterval, (I:Set ℝ) ∩ (J:Set ℝ) = (K:Set ℝ) := I:BoundedIntervalJ:BoundedInterval⊢ ∃ K, ↑I ∩ ↑J = ↑K All goals completed! 🐙
noncomputable instance BoundedInterval.instInter : Inter BoundedInterval where inter I J := (inter I J).choose@[simp] theorem BoundedInterval.inter_eq (I J: BoundedInterval) : (I ∩ J : BoundedInterval) = (I:Set ℝ) ∩ (J:Set ℝ) := (BoundedInterval.inter I J).choose_spec.symmdeclaration uses `sorry`example : (Icc 2 4 ∩ Icc 4 6) = (Icc 4 4 : Set ℝ) := ⊢ ↑(Icc 2 4 ∩ Icc 4 6) = ↑(Icc 4 4) All goals completed! 🐙instance BoundedInterval.instMembership : Membership ℝ BoundedInterval where mem I x := x ∈ (I:Set ℝ)theorem BoundedInterval.mem_iff (I: BoundedInterval) (x:ℝ) : x ∈ I ↔ x ∈ (I:Set ℝ) := I:BoundedIntervalx:ℝ⊢ x ∈ I ↔ x ∈ ↑I All goals completed! 🐙instance BoundedInterval.instSubset : HasSubset BoundedInterval where Subset I J := ∀ x, x ∈ I → x ∈ Jtheorem BoundedInterval.subset_iff (I J: BoundedInterval) : I ⊆ J ↔ (I:Set ℝ) ⊆ (J:Set ℝ) := I:BoundedIntervalJ:BoundedInterval⊢ I ⊆ J ↔ ↑I ⊆ ↑J All goals completed! 🐙abbrev BoundedInterval.a (I: BoundedInterval) : ℝ := match I with | Ioo a _ => a | Icc a _ => a | Ioc a _ => a | Ico a _ => aabbrev BoundedInterval.b (I: BoundedInterval) : ℝ := match I with | Ioo _ b => b | Icc _ b => b | Ioc _ b => b | Ico _ b => btheorem BoundedInterval.subset_Icc (I: BoundedInterval) : I ⊆ Icc I.a I.b := match I with I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ioo a✝ b✝ ⊆ Icc (Ioo a✝ b✝).a (Ioo a✝ b✝).b I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ioo a✝ b✝ ⊆ Icc (Ioo a✝ b✝).a (Ioo a✝ b✝).b All goals completed! 🐙 I:BoundedIntervala✝:ℝb✝:ℝ⊢ Icc a✝ b✝ ⊆ Icc (Icc a✝ b✝).a (Icc a✝ b✝).b I:BoundedIntervala✝:ℝb✝:ℝ⊢ Icc a✝ b✝ ⊆ Icc (Icc a✝ b✝).a (Icc a✝ b✝).b All goals completed! 🐙 I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ioc a✝ b✝ ⊆ Icc (Ioc a✝ b✝).a (Ioc a✝ b✝).b I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ioc a✝ b✝ ⊆ Icc (Ioc a✝ b✝).a (Ioc a✝ b✝).b All goals completed! 🐙 I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ico a✝ b✝ ⊆ Icc (Ico a✝ b✝).a (Ico a✝ b✝).b I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ico a✝ b✝ ⊆ Icc (Ico a✝ b✝).a (Ico a✝ b✝).b All goals completed! 🐙theorem BoundedInterval.Ioo_subset (I: BoundedInterval) : Ioo I.a I.b ⊆ I := match I with I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ioo (Ioo a✝ b✝).a (Ioo a✝ b✝).b ⊆ Ioo a✝ b✝ I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ioo (Ioo a✝ b✝).a (Ioo a✝ b✝).b ⊆ Ioo a✝ b✝ All goals completed! 🐙 I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ioo (Icc a✝ b✝).a (Icc a✝ b✝).b ⊆ Icc a✝ b✝ I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ioo (Icc a✝ b✝).a (Icc a✝ b✝).b ⊆ Icc a✝ b✝ All goals completed! 🐙 I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ioo (Ioc a✝ b✝).a (Ioc a✝ b✝).b ⊆ Ioc a✝ b✝ I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ioo (Ioc a✝ b✝).a (Ioc a✝ b✝).b ⊆ Ioc a✝ b✝ All goals completed! 🐙 I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ioo (Ico a✝ b✝).a (Ico a✝ b✝).b ⊆ Ico a✝ b✝ I:BoundedIntervala✝:ℝb✝:ℝ⊢ Ioo (Ico a✝ b✝).a (Ico a✝ b✝).b ⊆ Ico a✝ b✝ All goals completed! 🐙instance BoundedInterval.instTrans : IsTrans BoundedInterval (· ⊆ ·) where trans I J K hIJ hJK := I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalhIJ:I ⊆ JhJK:J ⊆ K⊢ I ⊆ K All goals completed! 🐙@[simp] theorem BoundedInterval.mem_inter (I J: BoundedInterval) (x:ℝ) : x ∈ (I ∩ J : BoundedInterval) ↔ x ∈ I ∧ x ∈ J := I:BoundedIntervalJ:BoundedIntervalx:ℝ⊢ x ∈ I ∩ J ↔ x ∈ I ∧ x ∈ J All goals completed! 🐙abbrev BoundedInterval.length (I: BoundedInterval) : ℝ := max (I.b - I.a) 0/-- Using ||ₗ subscript here to not override || -/ macro:max atomic("|" noWs) a:term noWs "|ₗ" : term => `(BoundedInterval.length $a)declaration uses `sorry`example : |Icc 3 5|ₗ = 2 := ⊢ (Icc 3 5).length = 2 All goals completed! 🐙declaration uses `sorry`example : |Ioo 3 5|ₗ = 2 := ⊢ (Ioo 3 5).length = 2 All goals completed! 🐙declaration uses `sorry`example : |Icc 5 5|ₗ = 0 := ⊢ (Icc 5 5).length = 0 All goals completed! 🐙theorem BoundedInterval.length_nonneg (I: BoundedInterval) : 0 ≤ |I|ₗ := I:BoundedInterval⊢ 0 ≤ I.length All goals completed! 🐙theorem BoundedInterval.empty_of_lt {I: BoundedInterval} (h: I.b < I.a) : (I:Set ℝ) = ∅ := I:BoundedIntervalh:I.b < I.a⊢ ↑I = ∅ cases I with a✝:ℝb✝:ℝh:(Ioo a✝ b✝).b < (Ioo a✝ b✝).a⊢ ↑(Ioo a✝ b✝) = ∅ All goals completed! 🐙 a✝:ℝb✝:ℝh:(Icc a✝ b✝).b < (Icc a✝ b✝).a⊢ ↑(Icc a✝ b✝) = ∅ All goals completed! 🐙 a✝:ℝb✝:ℝh:(Ioc a✝ b✝).b < (Ioc a✝ b✝).a⊢ ↑(Ioc a✝ b✝) = ∅ All goals completed! 🐙 a✝:ℝb✝:ℝh:(Ico a✝ b✝).b < (Ico a✝ b✝).a⊢ ↑(Ico a✝ b✝) = ∅ All goals completed! 🐙theorem declaration uses `sorry`BoundedInterval.length_of_empty {I: BoundedInterval} (hI: (I:Set ℝ) = ∅) : |I|ₗ = 0 := I:BoundedIntervalhI:↑I = ∅⊢ I.length = 0 All goals completed! 🐙theorem declaration uses `sorry`BoundedInterval.length_of_subsingleton {I: BoundedInterval} : Subsingleton (I:Set ℝ) ↔ |I|ₗ = 0 := I:BoundedInterval⊢ Subsingleton ↑↑I ↔ I.length = 0 All goals completed! 🐙theorem BoundedInterval.dist_le_length {I:BoundedInterval} {x y:ℝ} (hx: x ∈ I) (hy: y ∈ I) : |x - y| ≤ |I|ₗ := I:BoundedIntervalx:ℝy:ℝhx:x ∈ Ihy:y ∈ I⊢ |x - y| ≤ I.length I:BoundedIntervalx:ℝy:ℝhy:y ∈ Ihx:x ∈ Icc I.a I.b⊢ |x - y| ≤ I.length; I:BoundedIntervalx:ℝy:ℝhx:x ∈ Icc I.a I.bhy:y ∈ Icc I.a I.b⊢ |x - y| ≤ I.length; I:BoundedIntervalx:ℝy:ℝhx:I.a ≤ x ∧ x ≤ I.bhy:I.a ≤ y ∧ y ≤ I.b⊢ x ≤ I.b - I.a + y ∧ y ≤ I.b - I.a + x ∨ x ≤ y ∧ y ≤ x; All goals completed! 🐙abbrev BoundedInterval.joins (K I J: BoundedInterval) : Prop := (I:Set ℝ) ∩ (J:Set ℝ) = ∅ ∧ (K:Set ℝ) = (I:Set ℝ) ∪ (J:Set ℝ) ∧ |K|ₗ = |I|ₗ + |J|ₗtheorem BoundedInterval.join_Icc_Ioc {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Icc a c).joins (Icc a b) (Ioc b c) := a:ℝb:ℝc:ℝhab:a ≤ bhbc:b ≤ c⊢ (Icc a c).joins (Icc a b) (Ioc b c) a:ℝb:ℝc:ℝhab:a ≤ bhbc:b ≤ c⊢ Set.Icc a b ∩ Set.Ioc b c = ∅ ∧ (Icc a c).a ≤ (Icc a c).b; All goals completed! 🐙theorem BoundedInterval.join_Icc_Ioo {a b c:ℝ} (hab: a ≤ b) (hbc: b < c) : (Ico a c).joins (Icc a b) (Ioo b c) := a:ℝb:ℝc:ℝhab:a ≤ bhbc:b < c⊢ (Ico a c).joins (Icc a b) (Ioo b c) a:ℝb:ℝc:ℝhab:a ≤ bhbc:b < c⊢ Set.Icc a b ∩ Set.Ioo b c = ∅ ∧ (Ico a c).a ≤ (Ico a c).b; All goals completed! 🐙theorem BoundedInterval.join_Ioc_Ioc {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Ioc a c).joins (Ioc a b) (Ioc b c) := a:ℝb:ℝc:ℝhab:a ≤ bhbc:b ≤ c⊢ (Ioc a c).joins (Ioc a b) (Ioc b c) a:ℝb:ℝc:ℝhab:a ≤ bhbc:b ≤ c⊢ Set.Ioc a b ∩ Set.Ioc b c = ∅ ∧ (Ioc a c).a ≤ (Ioc a c).b; All goals completed! 🐙theorem BoundedInterval.join_Ioc_Ioo {a b c:ℝ} (hab: a ≤ b) (hbc: b < c) : (Ioo a c).joins (Ioc a b) (Ioo b c) := a:ℝb:ℝc:ℝhab:a ≤ bhbc:b < c⊢ (Ioo a c).joins (Ioc a b) (Ioo b c) a:ℝb:ℝc:ℝhab:a ≤ bhbc:b < c⊢ Set.Ioc a b ∩ Set.Ioo b c = ∅ ∧ (Ioo a c).a ≤ (Ioo a c).b; All goals completed! 🐙theorem BoundedInterval.join_Ico_Icc {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Icc a c).joins (Ico a b) (Icc b c) := a:ℝb:ℝc:ℝhab:a ≤ bhbc:b ≤ c⊢ (Icc a c).joins (Ico a b) (Icc b c) a:ℝb:ℝc:ℝhab:a ≤ bhbc:b ≤ c⊢ Set.Ico a b ∩ Set.Icc b c = ∅ ∧ (Icc a c).a ≤ (Icc a c).b; All goals completed! 🐙theorem BoundedInterval.join_Ico_Ico {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Ico a c).joins (Ico a b) (Ico b c) := a:ℝb:ℝc:ℝhab:a ≤ bhbc:b ≤ c⊢ (Ico a c).joins (Ico a b) (Ico b c) a:ℝb:ℝc:ℝhab:a ≤ bhbc:b ≤ c⊢ Set.Ico a b ∩ Set.Ico b c = ∅ ∧ (Ico a c).a ≤ (Ico a c).b; All goals completed! 🐙theorem BoundedInterval.join_Ioo_Icc {a b c:ℝ} (hab: a < b) (hbc: b ≤ c) : (Ioc a c).joins (Ioo a b) (Icc b c) := a:ℝb:ℝc:ℝhab:a < bhbc:b ≤ c⊢ (Ioc a c).joins (Ioo a b) (Icc b c) a:ℝb:ℝc:ℝhab:a < bhbc:b ≤ c⊢ Set.Ioo a b ∩ Set.Icc b c = ∅ ∧ (Ioc a c).a ≤ (Ioc a c).b; All goals completed! 🐙theorem BoundedInterval.join_Ioo_Ico {a b c:ℝ} (hab: a < b) (hbc: b ≤ c) : (Ioo a c).joins (Ioo a b) (Ico b c) := a:ℝb:ℝc:ℝhab:a < bhbc:b ≤ c⊢ (Ioo a c).joins (Ioo a b) (Ico b c) a:ℝb:ℝc:ℝhab:a < bhbc:b ≤ c⊢ Set.Ioo a b ∩ Set.Ico b c = ∅ ∧ (Ioo a c).a ≤ (Ioo a c).b; All goals completed! 🐙@[ext] structure Partition (I: BoundedInterval) where intervals : Finset BoundedInterval exists_unique (x:ℝ) (hx : x ∈ I) : ∃! J, J ∈ intervals ∧ x ∈ J contains (J : BoundedInterval) (hJ : J ∈ intervals) : J ⊆ IChapter11.Partition.mk {I : BoundedInterval} (intervals : Finset BoundedInterval) (exists_unique : ∀ x ∈ I, ∃! J, J ∈ intervals ∧ x ∈ J) (contains : ∀ J ∈ intervals, J ⊆ I) : Partition I#check Partition.mk
Chapter11.Partition.mk {I : BoundedInterval} (intervals : Finset BoundedInterval)
  (exists_unique : ∀ x ∈ I, ∃! J, J ∈ intervals ∧ x ∈ J) (contains : ∀ J ∈ intervals, J ⊆ I) : Partition I
instance Partition.instMembership (I: BoundedInterval) : Membership BoundedInterval (Partition I) where mem P J := J ∈ P.intervalsinstance Partition.instBot (I: BoundedInterval) : Bot (Partition I) where bot := { intervals := {I} exists_unique x hx := I:BoundedIntervalx:ℝhx:x ∈ I⊢ ∃! J, J ∈ {I} ∧ x ∈ J I:BoundedIntervalx:ℝhx:x ∈ I⊢ I ∈ {I} ∧ x ∈ II:BoundedIntervalx:ℝhx:x ∈ I⊢ ∀ (y : BoundedInterval), y ∈ {I} ∧ x ∈ y → y = I I:BoundedIntervalx:ℝhx:x ∈ I⊢ I ∈ {I} ∧ x ∈ II:BoundedIntervalx:ℝhx:x ∈ I⊢ ∀ (y : BoundedInterval), y ∈ {I} ∧ x ∈ y → y = I All goals completed! 🐙 contains := I:BoundedInterval⊢ ∀ J ∈ {I}, J ⊆ I All goals completed! 🐙 }@[simp] theorem Partition.intervals_of_bot (I:BoundedInterval) : (⊥:Partition I).intervals = {I} := I:BoundedInterval⊢ ⊥.intervals = {I} All goals completed! 🐙noncomputable abbrev Partition.join {I J K:BoundedInterval} (P: Partition I) (Q: Partition J) (h: K.joins I J) : Partition K := { intervals := P.intervals ∪ Q.intervals exists_unique x hx := I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝhx:x ∈ K⊢ ∃! J_1, J_1 ∈ P.intervals ∪ Q.intervals ∧ x ∈ J_1 I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝhx:x ∈ Kthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)⊢ ∃! J_1, J_1 ∈ P.intervals ∪ Q.intervals ∧ x ∈ J_1 I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑I ∨ x ∈ ↑J⊢ ∃! J_1, J_1 ∈ P.intervals ∪ Q.intervals ∧ x ∈ J_1; I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑I⊢ ∃! J_1, J_1 ∈ P.intervals ∪ Q.intervals ∧ x ∈ J_1I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑J⊢ ∃! J_1, J_1 ∈ P.intervals ∪ Q.intervals ∧ x ∈ J_1 I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑I⊢ ∃! J_1, J_1 ∈ P.intervals ∪ Q.intervals ∧ x ∈ J_1 I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑IL:BoundedIntervalh✝:L ∈ P.intervalsa✝:x ∈ L⊢ ∃! J_1, J_1 ∈ P.intervals ∪ Q.intervals ∧ x ∈ J_1 apply ExistsUnique.intro L (I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑IL:BoundedIntervalh✝:L ∈ P.intervalsa✝:x ∈ L⊢ L ∈ P.intervals ∪ Q.intervals ∧ x ∈ L All goals completed! 🐙) intro K I:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑IL:BoundedIntervalh✝:L ∈ P.intervalsa✝:x ∈ LK:BoundedIntervalhK:K ∈ P.intervals ∪ Q.intervalshxK:x ∈ K⊢ K = L; I:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑IL:BoundedIntervalh✝:L ∈ P.intervalsa✝:x ∈ LK:BoundedIntervalhxK:x ∈ KhK:K ∈ P.intervals ∨ K ∈ Q.intervals⊢ K = L; I:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑IL:BoundedIntervalh✝¹:L ∈ P.intervalsa✝:x ∈ LK:BoundedIntervalhxK:x ∈ Kh✝:K ∈ P.intervals⊢ K = LI:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑IL:BoundedIntervalh✝:L ∈ P.intervalsa✝:x ∈ LK:BoundedIntervalhxK:x ∈ KhKQ:K ∈ Q.intervals⊢ K = L map_tacs [I:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑IL:BoundedIntervalh✝¹:L ∈ P.intervalsa✝:x ∈ LK:BoundedIntervalhxK:x ∈ Kh✝:K ∈ P.intervals⊢ K ∈ P.intervals ∧ x ∈ KI:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑IL:BoundedIntervalh✝¹:L ∈ P.intervalsa✝:x ∈ LK:BoundedIntervalhxK:x ∈ Kh✝:K ∈ P.intervals⊢ L ∈ P.intervals ∧ x ∈ L; I:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑IL:BoundedIntervalh✝:L ∈ P.intervalsa✝:x ∈ LK:BoundedIntervalhKQ:K ∈ Q.intervalshxK:x ∈ ↑J⊢ K = L] all_goals All goals completed! 🐙 I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑JL:BoundedIntervalhLQ:L ∈ Q.intervalshxL:x ∈ L⊢ ∃! J_1, J_1 ∈ P.intervals ∪ Q.intervals ∧ x ∈ J_1 apply ExistsUnique.intro L (I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑JL:BoundedIntervalhLQ:L ∈ Q.intervalshxL:x ∈ L⊢ L ∈ P.intervals ∪ Q.intervals ∧ x ∈ L All goals completed! 🐙) intro K I:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑JL:BoundedIntervalhLQ:L ∈ Q.intervalshxL:x ∈ LK:BoundedIntervalhK:K ∈ P.intervals ∪ Q.intervalshxK:x ∈ K⊢ K = L; I:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑JL:BoundedIntervalhLQ:L ∈ Q.intervalshxL:x ∈ LK:BoundedIntervalhxK:x ∈ KhK:K ∈ P.intervals ∨ K ∈ Q.intervals⊢ K = L; I:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑JL:BoundedIntervalhLQ:L ∈ Q.intervalshxL:x ∈ LK:BoundedIntervalhxK:x ∈ KhKP:K ∈ P.intervals⊢ K = LI:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑JL:BoundedIntervalhLQ:L ∈ Q.intervalshxL:x ∈ LK:BoundedIntervalhxK:x ∈ Kh✝:K ∈ Q.intervals⊢ K = L map_tacs [I:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑JL:BoundedIntervalhLQ:L ∈ Q.intervalshxL:x ∈ LK:BoundedIntervalhKP:K ∈ P.intervalshxK:x ∈ ↑I⊢ K = L; I:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑JL:BoundedIntervalhLQ:L ∈ Q.intervalshxL:x ∈ LK:BoundedIntervalhxK:x ∈ Kh✝:K ∈ Q.intervals⊢ K ∈ Q.intervals ∧ x ∈ KI:BoundedIntervalJ:BoundedIntervalK✝:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I Jx:ℝthis:(x ∈ ↑I ∩ ↑J) = (x ∈ ∅)hx:x ∈ ↑JL:BoundedIntervalhLQ:L ∈ Q.intervalshxL:x ∈ LK:BoundedIntervalhxK:x ∈ Kh✝:K ∈ Q.intervals⊢ L ∈ Q.intervals ∧ x ∈ L] all_goals All goals completed! 🐙 contains L hL := I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I JL:BoundedIntervalhL:L ∈ P.intervals ∪ Q.intervals⊢ L ⊆ K I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I JL:BoundedIntervalhL:L ∈ P.intervals ∨ L ∈ Q.intervals⊢ L ⊆ K; I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I JL:BoundedIntervalhLP:L ∈ P.intervals⊢ L ⊆ KI:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I JL:BoundedIntervalhLQ:L ∈ Q.intervals⊢ L ⊆ K I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I JL:BoundedIntervalhLP:L ∈ P.intervals⊢ L ⊆ K I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I JL:BoundedIntervalhLP:L ∈ P.intervals⊢ I ⊆ K; All goals completed! 🐙 I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalP:Partition IQ:Partition Jh:K.joins I JL:BoundedIntervalhLQ:L ∈ Q.intervals⊢ J ⊆ K; All goals completed! 🐙 }@[simp] theorem 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 := I:BoundedIntervalJ:BoundedIntervalK:BoundedIntervalh:K.joins I JP:Partition IQ:Partition J⊢ (P.join Q h).intervals = P.intervals ∪ Q.intervals All goals completed! 🐙noncomputable abbrev Partition.add_empty {I:BoundedInterval} (P: Partition I) : Partition I := { intervals := P.intervals ∪ {∅} exists_unique x hx := I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ I⊢ ∃! J, J ∈ P.intervals ∪ {∅} ∧ x ∈ J I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ J⊢ ∃! J, J ∈ P.intervals ∪ {∅} ∧ x ∈ J apply ExistsUnique.intro J (I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ J⊢ J ∈ P.intervals ∪ {∅} ∧ x ∈ J All goals completed! 🐙) intro K I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ JK:BoundedIntervalhK:K ∈ P.intervals ∪ {∅}right✝:x ∈ K⊢ K = J; I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ JK:BoundedIntervalright✝:x ∈ KhK:K = ∅ ∨ K ∈ P.intervals⊢ K = J; I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ Jright✝:x ∈ ∅⊢ ∅ = JI:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ JK:BoundedIntervalright✝:x ∈ KhK:K ∈ P.intervals⊢ K = J I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ Jright✝:x ∈ ∅⊢ ∅ = J All goals completed! 🐙 I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ JK:BoundedIntervalright✝:x ∈ KhK:K ∈ P.intervals⊢ K ∈ P.intervals ∧ x ∈ KI:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ JK:BoundedIntervalright✝:x ∈ KhK:K ∈ P.intervals⊢ J ∈ P.intervals ∧ x ∈ J I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ JK:BoundedIntervalright✝:x ∈ KhK:K ∈ P.intervals⊢ K ∈ P.intervals ∧ x ∈ KI:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ JK:BoundedIntervalright✝:x ∈ KhK:K ∈ P.intervals⊢ J ∈ P.intervals ∧ x ∈ J All goals completed! 🐙 contains L hL := I:BoundedIntervalP:Partition IL:BoundedIntervalhL:L ∈ P.intervals ∪ {∅}⊢ L ⊆ I I:BoundedIntervalP:Partition IL:BoundedIntervalhL:L = ∅ ∨ L ∈ P.intervals⊢ L ⊆ I; I:BoundedIntervalP:Partition I⊢ ∅ ⊆ II:BoundedIntervalP:Partition IL:BoundedIntervalhL:L ∈ P.intervals⊢ L ⊆ I I:BoundedIntervalP:Partition I⊢ ∅ ⊆ I All goals completed! 🐙 All goals completed! 🐙 }open Classical in noncomputable abbrev Partition.remove_empty {I:BoundedInterval} (P: Partition I) : Partition I := { intervals := P.intervals.filter (fun J ↦ (J:Set ℝ).Nonempty) exists_unique x hx := I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ I⊢ ∃! J, J ∈ {J ∈ P.intervals | (↑J).Nonempty} ∧ x ∈ J I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ J⊢ ∃! J, J ∈ {J ∈ P.intervals | (↑J).Nonempty} ∧ x ∈ J apply ExistsUnique.intro J (I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ J⊢ J ∈ {J ∈ P.intervals | (↑J).Nonempty} ∧ x ∈ J All goals completed! 🐙) intro K I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ JK:BoundedIntervalhK:K ∈ {J ∈ P.intervals | (↑J).Nonempty}right✝:x ∈ K⊢ K = J; I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ JK:BoundedIntervalright✝:x ∈ KhK:K ∈ P.intervals ∧ (↑K).Nonempty⊢ K = J I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ JK:BoundedIntervalright✝:x ∈ KhK:K ∈ P.intervals ∧ (↑K).Nonempty⊢ K ∈ P.intervals ∧ x ∈ KI:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ JK:BoundedIntervalright✝:x ∈ KhK:K ∈ P.intervals ∧ (↑K).Nonempty⊢ J ∈ P.intervals ∧ x ∈ J I:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ JK:BoundedIntervalright✝:x ∈ KhK:K ∈ P.intervals ∧ (↑K).Nonempty⊢ K ∈ P.intervals ∧ x ∈ KI:BoundedIntervalP:Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervalsa✝:x ∈ JK:BoundedIntervalright✝:x ∈ KhK:K ∈ P.intervals ∧ (↑K).Nonempty⊢ J ∈ P.intervals ∧ x ∈ J All goals completed! 🐙 contains _ _ := P.contains _ (I:BoundedIntervalP:Partition Ix✝¹:BoundedIntervalx✝:x✝¹ ∈ {J ∈ P.intervals | (↑J).Nonempty}⊢ x✝¹ ∈ P.intervals All goals completed! 🐙) }@[simp] theorem Partition.intervals_of_add_empty (I: BoundedInterval) (P: Partition I) : (P.add_empty).intervals = P.intervals ∪ {∅} := I:BoundedIntervalP:Partition I⊢ P.add_empty.intervals = P.intervals ∪ {∅} All goals completed! 🐙example : ∃ P:Partition (Icc 1 8), P.intervals = {Icc 1 1, Ioo 1 3, Ico 3 5, Icc 5 5, Ioc 5 8, ∅} := ⊢ ∃ P, P.intervals = {Icc 1 1, Ioo 1 3, Ico 3 5, Icc 5 5, Ioc 5 8, ∅} P1:Partition (Icc 1 1) := ⊥⊢ ∃ P, P.intervals = {Icc 1 1, Ioo 1 3, Ico 3 5, Icc 5 5, Ioc 5 8, ∅} set P2 : Partition (Ico 1 3) := P1.join (⊥:Partition (Ioo 1 3)) (join_Icc_Ioo (P1:Partition (Icc 1 1) := ⊥⊢ 1 ≤ 1 All goals completed! 🐙) (P1:Partition (Icc 1 1) := ⊥⊢ 1 < 3 All goals completed! 🐙) ) set P3 : Partition (Ico 1 5) := P2.join (⊥:Partition (Ico 3 5)) (join_Ico_Ico (P1:Partition (Icc 1 1) := ⊥P2:Partition (Ico 1 3) := P1.join ⊥ ⋯⊢ 1 ≤ 3 All goals completed! 🐙) (P1:Partition (Icc 1 1) := ⊥P2:Partition (Ico 1 3) := P1.join ⊥ ⋯⊢ 3 ≤ 5 All goals completed! 🐙) ) set P4 : Partition (Icc 1 5) := P3.join (⊥:Partition (Icc 5 5)) (join_Ico_Icc (P1:Partition (Icc 1 1) := ⊥P2:Partition (Ico 1 3) := P1.join ⊥ ⋯P3:Partition (Ico 1 5) := P2.join ⊥ ⋯⊢ 1 ≤ 5 All goals completed! 🐙) (P1:Partition (Icc 1 1) := ⊥P2:Partition (Ico 1 3) := P1.join ⊥ ⋯P3:Partition (Ico 1 5) := P2.join ⊥ ⋯⊢ 5 ≤ 5 All goals completed! 🐙) ) set P5 : Partition (Icc 1 8) := P4.join (⊥:Partition (Ioc 5 8)) (join_Icc_Ioc (P1:Partition (Icc 1 1) := ⊥P2:Partition (Ico 1 3) := P1.join ⊥ ⋯P3:Partition (Ico 1 5) := P2.join ⊥ ⋯P4:Partition (Icc 1 5) := P3.join ⊥ ⋯⊢ 1 ≤ 5 All goals completed! 🐙) (P1:Partition (Icc 1 1) := ⊥P2:Partition (Ico 1 3) := P1.join ⊥ ⋯P3:Partition (Ico 1 5) := P2.join ⊥ ⋯P4:Partition (Icc 1 5) := P3.join ⊥ ⋯⊢ 5 ≤ 8 All goals completed! 🐙) ) P1:Partition (Icc 1 1) := ⊥P2:Partition (Ico 1 3) := P1.join ⊥ ⋯P3:Partition (Ico 1 5) := P2.join ⊥ ⋯P4:Partition (Icc 1 5) := P3.join ⊥ ⋯P5:Partition (Icc 1 8) := P4.join ⊥ ⋯⊢ P5.add_empty.intervals = {Icc 1 1, Ioo 1 3, Ico 3 5, Icc 5 5, Ioc 5 8, ∅}; P1:Partition (Icc 1 1) := ⊥P2:Partition (Ico 1 3) := P1.join ⊥ ⋯P3:Partition (Ico 1 5) := P2.join ⊥ ⋯P4:Partition (Icc 1 5) := P3.join ⊥ ⋯P5:Partition (Icc 1 8) := P4.join ⊥ ⋯⊢ insert ∅ P5.intervals = {Icc 1 1, Ioo 1 3, Ico 3 5, Icc 5 5, Ioc 5 8, ∅}; All goals completed! 🐙declaration uses `sorry`example : ∃ P:Partition (Icc 1 8), P.intervals = {Icc 1 1, Ioo 1 3, Ico 3 5, Icc 5 5, Ioc 5 8} := ⊢ ∃ P, P.intervals = {Icc 1 1, Ioo 1 3, Ico 3 5, Icc 5 5, Ioc 5 8} All goals completed! 🐙declaration uses `sorry`example : ¬∃ P:Partition (Icc 1 5), P.intervals = {Icc 1 4, Icc 3 5} := ⊢ ¬∃ P, P.intervals = {Icc 1 4, Icc 3 5} All goals completed! 🐙declaration uses `sorry`example : ¬∃ P:Partition (Ioo 1 5), P.intervals = {Ioo 1 3, Ioo 3 5} := ⊢ ¬∃ P, P.intervals = {Ioo 1 3, Ioo 3 5} All goals completed! 🐙declaration uses `sorry`example : ¬∃ P:Partition (Ioo 1 5), P.intervals = {Ioo 0 3, Ico 3 5} := ⊢ ¬∃ P, P.intervals = {Ioo 0 3, Ico 3 5} All goals completed! 🐙

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

theorem declaration uses `sorry`Partition.exist_right {I: BoundedInterval} (hI: I.a < I.b) (hI': I.b ∉ I) {P: Partition I} : ∃ c ∈ Set.Ico I.a I.b, Ioo c I.b ∈ P ∨ Ico c I.b ∈ P := I:BoundedIntervalhI:I.a < I.bhI':I.b ∉ IP:Partition I⊢ ∃ c ∈ Set.Ico I.a I.b, Ioo c I.b ∈ P ∨ Ico c I.b ∈ P All goals completed! 🐙

Theorem 11.1.13 (Length is finitely additive).

theorem declaration uses `sorry`Partition.sum_of_length (I: BoundedInterval) (P: Partition I) : ∑ J ∈ P.intervals, |J|ₗ = |I|ₗ := I:BoundedIntervalP:Partition I⊢ ∑ J ∈ P.intervals, J.length = I.length -- This proof is written to follow the structure of the original text. I:BoundedIntervalP:Partition In:ℕhcard:P.intervals.card = n⊢ ∑ J ∈ P.intervals, J.length = I.length n:ℕ⊢ ∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.length; ⊢ ∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = 0 → ∑ J ∈ P.intervals, J.length = I.lengthn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.length⊢ ∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n + 1 → ∑ J ∈ P.intervals, J.length = I.length ⊢ ∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = 0 → ∑ J ∈ P.intervals, J.length = I.lengthn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.length⊢ ∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n + 1 → ∑ J ∈ P.intervals, J.length = I.length intro I n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition I⊢ P.intervals.card = n + 1 → ∑ J ∈ P.intervals, J.length = I.length n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1⊢ ∑ J ∈ P.intervals, J.length = I.length I:BoundedIntervalP:Partition Ihcard:P.intervals.card = 0⊢ ∑ J ∈ P.intervals, J.length = I.length I:BoundedIntervalP:Partition Ihcard:P.intervals = ∅⊢ ∑ J ∈ P.intervals, J.length = I.length have : (I:Set ℝ) = ∅ := I:BoundedIntervalP:Partition I⊢ ∑ J ∈ P.intervals, J.length = I.length All goals completed! 🐙 All goals completed! 🐙 -- the proof in the book treats the n=1 case separately, but this is unnecessary n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:Subsingleton ↑↑I⊢ ∑ J ∈ P.intervals, J.length = I.lengthn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:¬Subsingleton ↑↑I⊢ ∑ J ∈ P.intervals, J.length = I.length n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:Subsingleton ↑↑I⊢ ∑ J ∈ P.intervals, J.length = I.length have (J: BoundedInterval) (hJ: J ∈ P) : Subsingleton (J:Set ℝ) := I:BoundedIntervalP:Partition I⊢ ∑ J ∈ P.intervals, J.length = I.length All goals completed! 🐙 simp_rw n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:Subsingleton ↑↑Ithis:∀ J ∈ P, Subsingleton ↑↑J⊢ ∑ J ∈ P.intervals, J.length = I.lengthlength_of_subsingleton] at * All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.b⊢ ∑ J ∈ P.intervals, J.length = I.length have : ∃ K L : BoundedInterval, K ∈ P ∧ I.joins L K := I:BoundedIntervalP:Partition I⊢ ∑ J ∈ P.intervals, J.length = I.length n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ I⊢ ∃ K L, K ∈ P ∧ I.joins L Kn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∉ I⊢ ∃ K L, K ∈ P ∧ I.joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ I⊢ ∃ K L, K ∈ P ∧ I.joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ K⊢ ∃ K L, K ∈ P ∧ I.joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ I⊢ ∃ K L, K ∈ P ∧ I.joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:Subsingleton ↑↑K⊢ ∃ K L, K ∈ P ∧ I.joins L Kn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:¬Subsingleton ↑↑K⊢ ∃ K L, K ∈ P ∧ I.joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:Subsingleton ↑↑K⊢ ∃ K L, K ∈ P ∧ I.joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bK:BoundedIntervalhI':I.b ∈ ↑IhK:K ∈ P.intervalshbK:I.b ∈ ↑KhKI:K ⊆ Ihsub:(↑K).Subsingleton⊢ ∃ K ∈ P, ∃ x, I.joins x K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bK:BoundedIntervalhI':I.b ∈ ↑IhK:K ∈ P.intervalshKI:K ⊆ Ihsub:(↑K).SubsingletonhbK:↑K = {I.b}⊢ ∃ K ∈ P, ∃ x, I.joins x K have : K = Icc (I.b) (I.b) := I:BoundedIntervalP:Partition I⊢ ∑ J ∈ P.intervals, J.length = I.length All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ ↑IhK:Icc I.b I.b ∈ P.intervalshKI:Icc I.b I.b ⊆ Ihsub:(↑(Icc I.b I.b)).SubsingletonhbK:↑(Icc I.b I.b) = {I.b}⊢ ∃ K ∈ P, ∃ x, I.joins x K cases I with n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha✝:ℝb✝:ℝP:Partition (Ioo a✝ b✝)hcard:P.intervals.card = n + 1h:(Ioo a✝ b✝).a < (Ioo a✝ b✝).bhI':(Ioo a✝ b✝).b ∈ ↑(Ioo a✝ b✝)hK:Icc (Ioo a✝ b✝).b (Ioo a✝ b✝).b ∈ P.intervalshKI:Icc (Ioo a✝ b✝).b (Ioo a✝ b✝).b ⊆ Ioo a✝ b✝hsub:(↑(Icc (Ioo a✝ b✝).b (Ioo a✝ b✝).b)).SubsingletonhbK:↑(Icc (Ioo a✝ b✝).b (Ioo a✝ b✝).b) = {(Ioo a✝ b✝).b}⊢ ∃ K ∈ P, ∃ x, (Ioo a✝ b✝).joins x K All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha:ℝb:ℝP:Partition (Icc a b)hcard:P.intervals.card = n + 1h:(Icc a b).a < (Icc a b).bhI':(Icc a b).b ∈ ↑(Icc a b)hK:Icc (Icc a b).b (Icc a b).b ∈ P.intervalshKI:Icc (Icc a b).b (Icc a b).b ⊆ Icc a bhsub:(↑(Icc (Icc a b).b (Icc a b).b)).SubsingletonhbK:↑(Icc (Icc a b).b (Icc a b).b) = {(Icc a b).b}⊢ ∃ K ∈ P, ∃ x, (Icc a b).joins x K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha:ℝb:ℝP:Partition (Icc a b)hcard:P.intervals.card = n + 1h:(Icc a b).a < (Icc a b).bhI':(Icc a b).b ∈ ↑(Icc a b)hK:Icc (Icc a b).b (Icc a b).b ∈ P.intervalshKI:Icc (Icc a b).b (Icc a b).b ⊆ Icc a bhsub:(↑(Icc (Icc a b).b (Icc a b).b)).SubsingletonhbK:↑(Icc (Icc a b).b (Icc a b).b) = {(Icc a b).b}⊢ (Icc a b).joins (Ico a b) (Icc b b); n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha:ℝb:ℝP:Partition (Icc a b)hcard:P.intervals.card = n + 1h:(Icc a b).a < (Icc a b).bhI':(Icc a b).b ∈ ↑(Icc a b)hK:Icc (Icc a b).b (Icc a b).b ∈ P.intervalshKI:Icc (Icc a b).b (Icc a b).b ⊆ Icc a bhsub:(↑(Icc (Icc a b).b (Icc a b).b)).SubsingletonhbK:↑(Icc (Icc a b).b (Icc a b).b) = {(Icc a b).b}⊢ a ≤ bn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha:ℝb:ℝP:Partition (Icc a b)hcard:P.intervals.card = n + 1h:(Icc a b).a < (Icc a b).bhI':(Icc a b).b ∈ ↑(Icc a b)hK:Icc (Icc a b).b (Icc a b).b ∈ P.intervalshKI:Icc (Icc a b).b (Icc a b).b ⊆ Icc a bhsub:(↑(Icc (Icc a b).b (Icc a b).b)).SubsingletonhbK:↑(Icc (Icc a b).b (Icc a b).b) = {(Icc a b).b}⊢ b ≤ b n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha:ℝb:ℝP:Partition (Icc a b)hcard:P.intervals.card = n + 1h:(Icc a b).a < (Icc a b).bhI':(Icc a b).b ∈ ↑(Icc a b)hK:Icc (Icc a b).b (Icc a b).b ∈ P.intervalshKI:Icc (Icc a b).b (Icc a b).b ⊆ Icc a bhsub:(↑(Icc (Icc a b).b (Icc a b).b)).SubsingletonhbK:↑(Icc (Icc a b).b (Icc a b).b) = {(Icc a b).b}⊢ a ≤ bn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha:ℝb:ℝP:Partition (Icc a b)hcard:P.intervals.card = n + 1h:(Icc a b).a < (Icc a b).bhI':(Icc a b).b ∈ ↑(Icc a b)hK:Icc (Icc a b).b (Icc a b).b ∈ P.intervalshKI:Icc (Icc a b).b (Icc a b).b ⊆ Icc a bhsub:(↑(Icc (Icc a b).b (Icc a b).b)).SubsingletonhbK:↑(Icc (Icc a b).b (Icc a b).b) = {(Icc a b).b}⊢ b ≤ b All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha:ℝb:ℝP:Partition (Ioc a b)hcard:P.intervals.card = n + 1h:(Ioc a b).a < (Ioc a b).bhI':(Ioc a b).b ∈ ↑(Ioc a b)hK:Icc (Ioc a b).b (Ioc a b).b ∈ P.intervalshKI:Icc (Ioc a b).b (Ioc a b).b ⊆ Ioc a bhsub:(↑(Icc (Ioc a b).b (Ioc a b).b)).SubsingletonhbK:↑(Icc (Ioc a b).b (Ioc a b).b) = {(Ioc a b).b}⊢ ∃ K ∈ P, ∃ x, (Ioc a b).joins x K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha:ℝb:ℝP:Partition (Ioc a b)hcard:P.intervals.card = n + 1h:(Ioc a b).a < (Ioc a b).bhI':(Ioc a b).b ∈ ↑(Ioc a b)hK:Icc (Ioc a b).b (Ioc a b).b ∈ P.intervalshKI:Icc (Ioc a b).b (Ioc a b).b ⊆ Ioc a bhsub:(↑(Icc (Ioc a b).b (Ioc a b).b)).SubsingletonhbK:↑(Icc (Ioc a b).b (Ioc a b).b) = {(Ioc a b).b}⊢ (Ioc a b).joins (Ioo a b) (Icc b b); n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha:ℝb:ℝP:Partition (Ioc a b)hcard:P.intervals.card = n + 1h:(Ioc a b).a < (Ioc a b).bhI':(Ioc a b).b ∈ ↑(Ioc a b)hK:Icc (Ioc a b).b (Ioc a b).b ∈ P.intervalshKI:Icc (Ioc a b).b (Ioc a b).b ⊆ Ioc a bhsub:(↑(Icc (Ioc a b).b (Ioc a b).b)).SubsingletonhbK:↑(Icc (Ioc a b).b (Ioc a b).b) = {(Ioc a b).b}⊢ a < bn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha:ℝb:ℝP:Partition (Ioc a b)hcard:P.intervals.card = n + 1h:(Ioc a b).a < (Ioc a b).bhI':(Ioc a b).b ∈ ↑(Ioc a b)hK:Icc (Ioc a b).b (Ioc a b).b ∈ P.intervalshKI:Icc (Ioc a b).b (Ioc a b).b ⊆ Ioc a bhsub:(↑(Icc (Ioc a b).b (Ioc a b).b)).SubsingletonhbK:↑(Icc (Ioc a b).b (Ioc a b).b) = {(Ioc a b).b}⊢ b ≤ b n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha:ℝb:ℝP:Partition (Ioc a b)hcard:P.intervals.card = n + 1h:(Ioc a b).a < (Ioc a b).bhI':(Ioc a b).b ∈ ↑(Ioc a b)hK:Icc (Ioc a b).b (Ioc a b).b ∈ P.intervalshKI:Icc (Ioc a b).b (Ioc a b).b ⊆ Ioc a bhsub:(↑(Icc (Ioc a b).b (Ioc a b).b)).SubsingletonhbK:↑(Icc (Ioc a b).b (Ioc a b).b) = {(Ioc a b).b}⊢ a < bn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha:ℝb:ℝP:Partition (Ioc a b)hcard:P.intervals.card = n + 1h:(Ioc a b).a < (Ioc a b).bhI':(Ioc a b).b ∈ ↑(Ioc a b)hK:Icc (Ioc a b).b (Ioc a b).b ∈ P.intervalshKI:Icc (Ioc a b).b (Ioc a b).b ⊆ Ioc a bhsub:(↑(Icc (Ioc a b).b (Ioc a b).b)).SubsingletonhbK:↑(Icc (Ioc a b).b (Ioc a b).b) = {(Ioc a b).b}⊢ b ≤ b All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha✝:ℝb✝:ℝP:Partition (Ico a✝ b✝)hcard:P.intervals.card = n + 1h:(Ico a✝ b✝).a < (Ico a✝ b✝).bhI':(Ico a✝ b✝).b ∈ ↑(Ico a✝ b✝)hK:Icc (Ico a✝ b✝).b (Ico a✝ b✝).b ∈ P.intervalshKI:Icc (Ico a✝ b✝).b (Ico a✝ b✝).b ⊆ Ico a✝ b✝hsub:(↑(Icc (Ico a✝ b✝).b (Ico a✝ b✝).b)).SubsingletonhbK:↑(Icc (Ico a✝ b✝).b (Ico a✝ b✝).b) = {(Ico a✝ b✝).b}⊢ ∃ K ∈ P, ∃ x, (Ico a✝ b✝).joins x K All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:K.a < K.b⊢ ∃ K L, K ∈ P ∧ I.joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:K.a < K.bhKI':Ioo K.a K.b ⊆ Icc I.a I.b⊢ ∃ K L, K ∈ P ∧ I.joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:K.a < K.bhKI':↑(Ioo K.a K.b) ⊆ ↑(Icc I.a I.b)⊢ ∃ K L, K ∈ P ∧ I.joins L K have hKb : K.b = I.b := I:BoundedIntervalP:Partition I⊢ ∑ J ∈ P.intervals, J.length = I.length n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:K.a < K.bhKI':↑(Ioo K.a K.b) ⊆ ↑(Icc I.a I.b)⊢ K.b ≤ I.b ∧ I.b ≤ K.b; n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:K.a < K.bhKI':↑(Ioo K.a K.b) ⊆ ↑(Icc I.a I.b)⊢ K.b ≤ I.bn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:K.a < K.bhKI':↑(Ioo K.a K.b) ⊆ ↑(Icc I.a I.b)⊢ I.b ≤ K.b n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:K.a < K.bhKI':↑(Ioo K.a K.b) ⊆ ↑(Icc I.a I.b)⊢ K.b ≤ I.b apply csSup_le_csSup bddAbove_Icc (n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:K.a < K.bhKI':↑(Ioo K.a K.b) ⊆ ↑(Icc I.a I.b)⊢ (↑(Ioo K.a K.b)).Nonempty All goals completed! 🐙) at hKI' All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:K.a < K.bhKI':↑(Ioo K.a K.b) ⊆ ↑(Icc I.a I.b)this:I.b ∈ Icc K.a K.b⊢ I.b ≤ K.b; n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:K.a < K.bhKI':↑(Ioo K.a K.b) ⊆ ↑(Icc I.a I.b)this:K.a ≤ I.b ∧ I.b ≤ K.b⊢ I.b ≤ K.b; All goals completed! 🐙 have hKA : I.a ≤ K.a := I:BoundedIntervalP:Partition I⊢ ∑ J ∈ P.intervals, J.length = I.length apply csInf_le_csInf bddBelow_Icc (n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∈ IK:BoundedIntervalhK:K ∈ P.intervalshbK:I.b ∈ KhKI:K ⊆ Ihsub:K.a < K.bhKI':↑(Ioo K.a K.b) ⊆ ↑(Icc I.a I.b)hKb:K.b = I.b⊢ (↑(Ioo K.a K.b)).Nonempty All goals completed! 🐙) at hKI' All goals completed! 🐙 cases I with n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthK:BoundedIntervalhsub:K.a < K.ba✝:ℝb✝:ℝP:Partition (Ioo a✝ b✝)hcard:P.intervals.card = n + 1h:(Ioo a✝ b✝).a < (Ioo a✝ b✝).bhI':(Ioo a✝ b✝).b ∈ Ioo a✝ b✝hK:K ∈ P.intervalshbK:(Ioo a✝ b✝).b ∈ KhKI:K ⊆ Ioo a✝ b✝hKI':↑(Ioo K.a K.b) ⊆ ↑(Icc (Ioo a✝ b✝).a (Ioo a✝ b✝).b)hKb:K.b = (Ioo a✝ b✝).bhKA:(Ioo a✝ b✝).a ≤ K.a⊢ ∃ K L, K ∈ P ∧ (Ioo a✝ b✝).joins L K All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthK:BoundedIntervalhsub:K.a < K.ba₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁hK:K ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ KhKI:K ⊆ Icc a₁ b₁hKI':↑(Ioo K.a K.b) ⊆ ↑(Icc (Icc a₁ b₁).a (Icc a₁ b₁).b)hKb:K.b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ K.a⊢ ∃ K L, K ∈ P ∧ (Icc a₁ b₁).joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthK:BoundedIntervalhsub:K.a < K.ba₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁hK:K ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ KhKI:K ⊆ Icc a₁ b₁hKI':↑(Ioo K.a K.b) ⊆ ↑(Icc (Icc a₁ b₁).a (Icc a₁ b₁).b)hKb:K.b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ K.a⊢ ∃ L, K ∈ P ∧ (Icc a₁ b₁).joins L K; cases K with n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁a✝:ℝb✝:ℝhsub:(Ioo a✝ b✝).a < (Ioo a✝ b✝).bhK:Ioo a✝ b✝ ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Ioo a✝ b✝hKI:Ioo a✝ b✝ ⊆ Icc a₁ b₁hKI':↑(Ioo (Ioo a✝ b✝).a (Ioo a✝ b✝).b) ⊆ ↑(Icc (Icc a₁ b₁).a (Icc a₁ b₁).b)hKb:(Ioo a✝ b✝).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Ioo a✝ b✝).a⊢ ∃ L, Ioo a✝ b✝ ∈ P ∧ (Icc a₁ b₁).joins L (Ioo a✝ b✝) n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).ba✝:ℝb✝:ℝhsub:(Ioo a✝ b✝).a < (Ioo a✝ b✝).bhK:Ioo a✝ b✝ ∈ P.intervalshKb:(Ioo a✝ b✝).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Ioo a✝ b✝).ahI':a₁ ≤ (Icc a₁ b₁).bhbK:a✝ < (Icc a₁ b₁).b ∧ (Icc a₁ b₁).b < b✝hKI:Set.Ioo a✝ b✝ ⊆ Set.Icc a₁ b₁hKI':Set.Ioo (Ioo a✝ b✝).a (Ioo a✝ b✝).b ⊆ Set.Icc (Icc a₁ b₁).a (Icc a₁ b₁).b⊢ Ioo a✝ b✝ ∈ P ∧ ∃ x, (Icc a₁ b₁).joins x (Ioo a✝ b✝); All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Icc c₂ b₂).a < (Icc c₂ b₂).bhK:Icc c₂ b₂ ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Icc c₂ b₂hKI:Icc c₂ b₂ ⊆ Icc a₁ b₁hKI':↑(Ioo (Icc c₂ b₂).a (Icc c₂ b₂).b) ⊆ ↑(Icc (Icc a₁ b₁).a (Icc a₁ b₁).b)hKb:(Icc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Icc c₂ b₂).a⊢ ∃ L, Icc c₂ b₂ ∈ P ∧ (Icc a₁ b₁).joins L (Icc c₂ b₂) n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Icc c₂ b₂).a < (Icc c₂ b₂).bhK:Icc c₂ b₂ ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Icc c₂ b₂hKI:Icc c₂ b₂ ⊆ Icc a₁ b₁hKI':↑(Ioo (Icc c₂ b₂).a (Icc c₂ b₂).b) ⊆ ↑(Icc (Icc a₁ b₁).a (Icc a₁ b₁).b)hKb:(Icc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Icc c₂ b₂).a⊢ (Icc a₁ b₁).joins (Ico a₁ c₂) (Icc c₂ b₂); n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Icc c₂ (Icc a₁ b₁).b).a < (Icc c₂ (Icc a₁ b₁).b).bhK:Icc c₂ (Icc a₁ b₁).b ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Icc c₂ (Icc a₁ b₁).bhKI:Icc c₂ (Icc a₁ b₁).b ⊆ Icc a₁ b₁hKI':Set.Ioo (Icc c₂ (Icc a₁ b₁).b).a (Icc c₂ (Icc a₁ b₁).b).b ⊆ Set.Icc (Icc a₁ b₁).a (Icc a₁ b₁).bhKb:(Icc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Icc c₂ (Icc a₁ b₁).b).a⊢ (Icc a₁ b₁).joins (Ico a₁ c₂) (Icc c₂ (Icc a₁ b₁).b); n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Icc c₂ (Icc a₁ b₁).b).a < (Icc c₂ (Icc a₁ b₁).b).bhK:Icc c₂ (Icc a₁ b₁).b ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Icc c₂ (Icc a₁ b₁).bhKI:Icc c₂ (Icc a₁ b₁).b ⊆ Icc a₁ b₁hKI':Set.Ioo (Icc c₂ (Icc a₁ b₁).b).a (Icc c₂ (Icc a₁ b₁).b).b ⊆ Set.Icc (Icc a₁ b₁).a (Icc a₁ b₁).bhKb:(Icc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Icc c₂ (Icc a₁ b₁).b).a⊢ a₁ ≤ c₂n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Icc c₂ (Icc a₁ b₁).b).a < (Icc c₂ (Icc a₁ b₁).b).bhK:Icc c₂ (Icc a₁ b₁).b ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Icc c₂ (Icc a₁ b₁).bhKI:Icc c₂ (Icc a₁ b₁).b ⊆ Icc a₁ b₁hKI':Set.Ioo (Icc c₂ (Icc a₁ b₁).b).a (Icc c₂ (Icc a₁ b₁).b).b ⊆ Set.Icc (Icc a₁ b₁).a (Icc a₁ b₁).bhKb:(Icc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Icc c₂ (Icc a₁ b₁).b).a⊢ c₂ ≤ b₁ n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Icc c₂ (Icc a₁ b₁).b).a < (Icc c₂ (Icc a₁ b₁).b).bhK:Icc c₂ (Icc a₁ b₁).b ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Icc c₂ (Icc a₁ b₁).bhKI:Icc c₂ (Icc a₁ b₁).b ⊆ Icc a₁ b₁hKI':Set.Ioo (Icc c₂ (Icc a₁ b₁).b).a (Icc c₂ (Icc a₁ b₁).b).b ⊆ Set.Icc (Icc a₁ b₁).a (Icc a₁ b₁).bhKb:(Icc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Icc c₂ (Icc a₁ b₁).b).a⊢ a₁ ≤ c₂n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Icc c₂ (Icc a₁ b₁).b).a < (Icc c₂ (Icc a₁ b₁).b).bhK:Icc c₂ (Icc a₁ b₁).b ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Icc c₂ (Icc a₁ b₁).bhKI:Icc c₂ (Icc a₁ b₁).b ⊆ Icc a₁ b₁hKI':Set.Ioo (Icc c₂ (Icc a₁ b₁).b).a (Icc c₂ (Icc a₁ b₁).b).b ⊆ Set.Icc (Icc a₁ b₁).a (Icc a₁ b₁).bhKb:(Icc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Icc c₂ (Icc a₁ b₁).b).a⊢ c₂ ≤ b₁ All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ b₂).a < (Ioc c₂ b₂).bhK:Ioc c₂ b₂ ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Ioc c₂ b₂hKI:Ioc c₂ b₂ ⊆ Icc a₁ b₁hKI':↑(Ioo (Ioc c₂ b₂).a (Ioc c₂ b₂).b) ⊆ ↑(Icc (Icc a₁ b₁).a (Icc a₁ b₁).b)hKb:(Ioc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Ioc c₂ b₂).a⊢ ∃ L, Ioc c₂ b₂ ∈ P ∧ (Icc a₁ b₁).joins L (Ioc c₂ b₂) n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ b₂).a < (Ioc c₂ b₂).bhK:Ioc c₂ b₂ ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Ioc c₂ b₂hKI:Ioc c₂ b₂ ⊆ Icc a₁ b₁hKI':↑(Ioo (Ioc c₂ b₂).a (Ioc c₂ b₂).b) ⊆ ↑(Icc (Icc a₁ b₁).a (Icc a₁ b₁).b)hKb:(Ioc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Ioc c₂ b₂).a⊢ (Icc a₁ b₁).joins (Icc a₁ c₂) (Ioc c₂ b₂); n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ (Icc a₁ b₁).b).a < (Ioc c₂ (Icc a₁ b₁).b).bhK:Ioc c₂ (Icc a₁ b₁).b ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Ioc c₂ (Icc a₁ b₁).bhKI:Ioc c₂ (Icc a₁ b₁).b ⊆ Icc a₁ b₁hKI':Set.Ioo (Ioc c₂ (Icc a₁ b₁).b).a (Ioc c₂ (Icc a₁ b₁).b).b ⊆ Set.Icc (Icc a₁ b₁).a (Icc a₁ b₁).bhKb:(Ioc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Ioc c₂ (Icc a₁ b₁).b).a⊢ (Icc a₁ b₁).joins (Icc a₁ c₂) (Ioc c₂ (Icc a₁ b₁).b); n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ (Icc a₁ b₁).b).a < (Ioc c₂ (Icc a₁ b₁).b).bhK:Ioc c₂ (Icc a₁ b₁).b ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Ioc c₂ (Icc a₁ b₁).bhKI:Ioc c₂ (Icc a₁ b₁).b ⊆ Icc a₁ b₁hKI':Set.Ioo (Ioc c₂ (Icc a₁ b₁).b).a (Ioc c₂ (Icc a₁ b₁).b).b ⊆ Set.Icc (Icc a₁ b₁).a (Icc a₁ b₁).bhKb:(Ioc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Ioc c₂ (Icc a₁ b₁).b).a⊢ a₁ ≤ c₂n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ (Icc a₁ b₁).b).a < (Ioc c₂ (Icc a₁ b₁).b).bhK:Ioc c₂ (Icc a₁ b₁).b ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Ioc c₂ (Icc a₁ b₁).bhKI:Ioc c₂ (Icc a₁ b₁).b ⊆ Icc a₁ b₁hKI':Set.Ioo (Ioc c₂ (Icc a₁ b₁).b).a (Ioc c₂ (Icc a₁ b₁).b).b ⊆ Set.Icc (Icc a₁ b₁).a (Icc a₁ b₁).bhKb:(Ioc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Ioc c₂ (Icc a₁ b₁).b).a⊢ c₂ ≤ b₁ n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ (Icc a₁ b₁).b).a < (Ioc c₂ (Icc a₁ b₁).b).bhK:Ioc c₂ (Icc a₁ b₁).b ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Ioc c₂ (Icc a₁ b₁).bhKI:Ioc c₂ (Icc a₁ b₁).b ⊆ Icc a₁ b₁hKI':Set.Ioo (Ioc c₂ (Icc a₁ b₁).b).a (Ioc c₂ (Icc a₁ b₁).b).b ⊆ Set.Icc (Icc a₁ b₁).a (Icc a₁ b₁).bhKb:(Ioc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Ioc c₂ (Icc a₁ b₁).b).a⊢ a₁ ≤ c₂n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ (Icc a₁ b₁).b).a < (Ioc c₂ (Icc a₁ b₁).b).bhK:Ioc c₂ (Icc a₁ b₁).b ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Ioc c₂ (Icc a₁ b₁).bhKI:Ioc c₂ (Icc a₁ b₁).b ⊆ Icc a₁ b₁hKI':Set.Ioo (Ioc c₂ (Icc a₁ b₁).b).a (Ioc c₂ (Icc a₁ b₁).b).b ⊆ Set.Icc (Icc a₁ b₁).a (Icc a₁ b₁).bhKb:(Ioc c₂ b₂).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Ioc c₂ (Icc a₁ b₁).b).a⊢ c₂ ≤ b₁ All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).bhI':(Icc a₁ b₁).b ∈ Icc a₁ b₁a✝:ℝb✝:ℝhsub:(Ico a✝ b✝).a < (Ico a✝ b✝).bhK:Ico a✝ b✝ ∈ P.intervalshbK:(Icc a₁ b₁).b ∈ Ico a✝ b✝hKI:Ico a✝ b✝ ⊆ Icc a₁ b₁hKI':↑(Ioo (Ico a✝ b✝).a (Ico a✝ b✝).b) ⊆ ↑(Icc (Icc a₁ b₁).a (Icc a₁ b₁).b)hKb:(Ico a✝ b✝).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Ico a✝ b✝).a⊢ ∃ L, Ico a✝ b✝ ∈ P ∧ (Icc a₁ b₁).joins L (Ico a✝ b✝) n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Icc a₁ b₁)hcard:P.intervals.card = n + 1h:(Icc a₁ b₁).a < (Icc a₁ b₁).ba✝:ℝb✝:ℝhsub:(Ico a✝ b✝).a < (Ico a✝ b✝).bhK:Ico a✝ b✝ ∈ P.intervalshKI:Ico a✝ b✝ ⊆ Icc a₁ b₁hKb:(Ico a✝ b✝).b = (Icc a₁ b₁).bhKA:(Icc a₁ b₁).a ≤ (Ico a✝ b✝).ahI':a₁ ≤ (Icc a₁ b₁).bhbK:a✝ ≤ (Icc a₁ b₁).b ∧ (Icc a₁ b₁).b < b✝hKI':Set.Ioo (Ico a✝ b✝).a (Ico a✝ b✝).b ⊆ Set.Icc (Icc a₁ b₁).a (Icc a₁ b₁).b⊢ Ico a✝ b✝ ∈ P ∧ ∃ x, (Icc a₁ b₁).joins x (Ico a✝ b✝); All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthK:BoundedIntervalhsub:K.a < K.ba₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁hK:K ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ KhKI:K ⊆ Ioc a₁ b₁hKI':↑(Ioo K.a K.b) ⊆ ↑(Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).b)hKb:K.b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ K.a⊢ ∃ K L, K ∈ P ∧ (Ioc a₁ b₁).joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthK:BoundedIntervalhsub:K.a < K.ba₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁hK:K ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ KhKI:K ⊆ Ioc a₁ b₁hKI':↑(Ioo K.a K.b) ⊆ ↑(Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).b)hKb:K.b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ K.a⊢ ∃ L, K ∈ P ∧ (Ioc a₁ b₁).joins L K; cases K with n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁a✝:ℝb✝:ℝhsub:(Ioo a✝ b✝).a < (Ioo a✝ b✝).bhK:Ioo a✝ b✝ ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ Ioo a✝ b✝hKI:Ioo a✝ b✝ ⊆ Ioc a₁ b₁hKI':↑(Ioo (Ioo a✝ b✝).a (Ioo a✝ b✝).b) ⊆ ↑(Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).b)hKb:(Ioo a✝ b✝).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Ioo a✝ b✝).a⊢ ∃ L, Ioo a✝ b✝ ∈ P ∧ (Ioc a₁ b₁).joins L (Ioo a✝ b✝) All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁c₂:ℝb₂:ℝhsub:(Icc c₂ b₂).a < (Icc c₂ b₂).bhK:Icc c₂ b₂ ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ Icc c₂ b₂hKI:Icc c₂ b₂ ⊆ Ioc a₁ b₁hKI':↑(Ioo (Icc c₂ b₂).a (Icc c₂ b₂).b) ⊆ ↑(Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).b)hKb:(Icc c₂ b₂).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Icc c₂ b₂).a⊢ ∃ L, Icc c₂ b₂ ∈ P ∧ (Ioc a₁ b₁).joins L (Icc c₂ b₂) n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁c₂:ℝb₂:ℝhsub:(Icc c₂ b₂).a < (Icc c₂ b₂).bhK:Icc c₂ b₂ ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ Icc c₂ b₂hKI:Icc c₂ b₂ ⊆ Ioc a₁ b₁hKI':↑(Ioo (Icc c₂ b₂).a (Icc c₂ b₂).b) ⊆ ↑(Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).b)hKb:(Icc c₂ b₂).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Icc c₂ b₂).a⊢ (Ioc a₁ b₁).joins (Ioo a₁ c₂) (Icc c₂ b₂) n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁c₂:ℝb₂:ℝhsub:(Icc c₂ (Ioc a₁ b₁).b).a < (Icc c₂ (Ioc a₁ b₁).b).bhK:Icc c₂ (Ioc a₁ b₁).b ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ Icc c₂ (Ioc a₁ b₁).bhKI:Set.Icc c₂ (Ioc a₁ b₁).b ⊆ Set.Ioc a₁ b₁hKI':Set.Ioo (Icc c₂ (Ioc a₁ b₁).b).a (Icc c₂ (Ioc a₁ b₁).b).b ⊆ Set.Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).bhKb:(Icc c₂ b₂).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Icc c₂ (Ioc a₁ b₁).b).a⊢ (Ioc a₁ b₁).joins (Ioo a₁ c₂) (Icc c₂ (Ioc a₁ b₁).b) have : c₂ ∈ Set.Icc c₂ b₁ := I:BoundedIntervalP:Partition I⊢ ∑ J ∈ P.intervals, J.length = I.length All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁c₂:ℝb₂:ℝhsub:(Icc c₂ (Ioc a₁ b₁).b).a < (Icc c₂ (Ioc a₁ b₁).b).bhK:Icc c₂ (Ioc a₁ b₁).b ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ Icc c₂ (Ioc a₁ b₁).bhKI:Set.Icc c₂ (Ioc a₁ b₁).b ⊆ Set.Ioc a₁ b₁hKI':Set.Ioo (Icc c₂ (Ioc a₁ b₁).b).a (Icc c₂ (Ioc a₁ b₁).b).b ⊆ Set.Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).bhKb:(Icc c₂ b₂).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Icc c₂ (Ioc a₁ b₁).b).athis:c₂ ∈ Set.Ioc a₁ b₁⊢ (Ioc a₁ b₁).joins (Ioo a₁ c₂) (Icc c₂ (Ioc a₁ b₁).b); All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ b₂).a < (Ioc c₂ b₂).bhK:Ioc c₂ b₂ ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ Ioc c₂ b₂hKI:Ioc c₂ b₂ ⊆ Ioc a₁ b₁hKI':↑(Ioo (Ioc c₂ b₂).a (Ioc c₂ b₂).b) ⊆ ↑(Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).b)hKb:(Ioc c₂ b₂).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Ioc c₂ b₂).a⊢ ∃ L, Ioc c₂ b₂ ∈ P ∧ (Ioc a₁ b₁).joins L (Ioc c₂ b₂) n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ b₂).a < (Ioc c₂ b₂).bhK:Ioc c₂ b₂ ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ Ioc c₂ b₂hKI:Ioc c₂ b₂ ⊆ Ioc a₁ b₁hKI':↑(Ioo (Ioc c₂ b₂).a (Ioc c₂ b₂).b) ⊆ ↑(Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).b)hKb:(Ioc c₂ b₂).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Ioc c₂ b₂).a⊢ (Ioc a₁ b₁).joins (Ioc a₁ c₂) (Ioc c₂ b₂); n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ (Ioc a₁ b₁).b).a < (Ioc c₂ (Ioc a₁ b₁).b).bhK:Ioc c₂ (Ioc a₁ b₁).b ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ Ioc c₂ (Ioc a₁ b₁).bhKI:Ioc c₂ (Ioc a₁ b₁).b ⊆ Ioc a₁ b₁hKI':Set.Ioo (Ioc c₂ (Ioc a₁ b₁).b).a (Ioc c₂ (Ioc a₁ b₁).b).b ⊆ Set.Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).bhKb:(Ioc c₂ b₂).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Ioc c₂ (Ioc a₁ b₁).b).a⊢ (Ioc a₁ b₁).joins (Ioc a₁ c₂) (Ioc c₂ (Ioc a₁ b₁).b); n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ (Ioc a₁ b₁).b).a < (Ioc c₂ (Ioc a₁ b₁).b).bhK:Ioc c₂ (Ioc a₁ b₁).b ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ Ioc c₂ (Ioc a₁ b₁).bhKI:Ioc c₂ (Ioc a₁ b₁).b ⊆ Ioc a₁ b₁hKI':Set.Ioo (Ioc c₂ (Ioc a₁ b₁).b).a (Ioc c₂ (Ioc a₁ b₁).b).b ⊆ Set.Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).bhKb:(Ioc c₂ b₂).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Ioc c₂ (Ioc a₁ b₁).b).a⊢ a₁ ≤ c₂n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ (Ioc a₁ b₁).b).a < (Ioc c₂ (Ioc a₁ b₁).b).bhK:Ioc c₂ (Ioc a₁ b₁).b ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ Ioc c₂ (Ioc a₁ b₁).bhKI:Ioc c₂ (Ioc a₁ b₁).b ⊆ Ioc a₁ b₁hKI':Set.Ioo (Ioc c₂ (Ioc a₁ b₁).b).a (Ioc c₂ (Ioc a₁ b₁).b).b ⊆ Set.Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).bhKb:(Ioc c₂ b₂).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Ioc c₂ (Ioc a₁ b₁).b).a⊢ c₂ ≤ b₁ n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ (Ioc a₁ b₁).b).a < (Ioc c₂ (Ioc a₁ b₁).b).bhK:Ioc c₂ (Ioc a₁ b₁).b ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ Ioc c₂ (Ioc a₁ b₁).bhKI:Ioc c₂ (Ioc a₁ b₁).b ⊆ Ioc a₁ b₁hKI':Set.Ioo (Ioc c₂ (Ioc a₁ b₁).b).a (Ioc c₂ (Ioc a₁ b₁).b).b ⊆ Set.Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).bhKb:(Ioc c₂ b₂).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Ioc c₂ (Ioc a₁ b₁).b).a⊢ a₁ ≤ c₂n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁c₂:ℝb₂:ℝhsub:(Ioc c₂ (Ioc a₁ b₁).b).a < (Ioc c₂ (Ioc a₁ b₁).b).bhK:Ioc c₂ (Ioc a₁ b₁).b ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ Ioc c₂ (Ioc a₁ b₁).bhKI:Ioc c₂ (Ioc a₁ b₁).b ⊆ Ioc a₁ b₁hKI':Set.Ioo (Ioc c₂ (Ioc a₁ b₁).b).a (Ioc c₂ (Ioc a₁ b₁).b).b ⊆ Set.Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).bhKb:(Ioc c₂ b₂).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Ioc c₂ (Ioc a₁ b₁).b).a⊢ c₂ ≤ b₁ All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).bhI':(Ioc a₁ b₁).b ∈ Ioc a₁ b₁a✝:ℝb✝:ℝhsub:(Ico a✝ b✝).a < (Ico a✝ b✝).bhK:Ico a✝ b✝ ∈ P.intervalshbK:(Ioc a₁ b₁).b ∈ Ico a✝ b✝hKI:Ico a✝ b✝ ⊆ Ioc a₁ b₁hKI':↑(Ioo (Ico a✝ b✝).a (Ico a✝ b✝).b) ⊆ ↑(Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).b)hKb:(Ico a✝ b✝).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Ico a✝ b✝).a⊢ ∃ L, Ico a✝ b✝ ∈ P ∧ (Ioc a₁ b₁).joins L (Ico a✝ b✝) n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengtha₁:ℝb₁:ℝP:Partition (Ioc a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioc a₁ b₁).a < (Ioc a₁ b₁).ba✝:ℝb✝:ℝhsub:(Ico a✝ b✝).a < (Ico a✝ b✝).bhK:Ico a✝ b✝ ∈ P.intervalshKb:(Ico a✝ b✝).b = (Ioc a₁ b₁).bhKA:(Ioc a₁ b₁).a ≤ (Ico a✝ b✝).ahI':a₁ < (Ioc a₁ b₁).bhbK:a✝ ≤ (Ioc a₁ b₁).b ∧ (Ioc a₁ b₁).b < b✝hKI:Set.Ico a✝ b✝ ⊆ Set.Ioc a₁ b₁hKI':Set.Ioo (Ico a✝ b✝).a (Ico a✝ b✝).b ⊆ Set.Icc (Ioc a₁ b₁).a (Ioc a₁ b₁).b⊢ Ico a✝ b✝ ∈ P ∧ ∃ x, (Ioc a₁ b₁).joins x (Ico a✝ b✝); All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthK:BoundedIntervalhsub:K.a < K.ba✝:ℝb✝:ℝP:Partition (Ico a✝ b✝)hcard:P.intervals.card = n + 1h:(Ico a✝ b✝).a < (Ico a✝ b✝).bhI':(Ico a✝ b✝).b ∈ Ico a✝ b✝hK:K ∈ P.intervalshbK:(Ico a✝ b✝).b ∈ KhKI:K ⊆ Ico a✝ b✝hKI':↑(Ioo K.a K.b) ⊆ ↑(Icc (Ico a✝ b✝).a (Ico a✝ b✝).b)hKb:K.b = (Ico a✝ b✝).bhKA:(Ico a✝ b✝).a ≤ K.a⊢ ∃ K L, K ∈ P ∧ (Ico a✝ b✝).joins L K All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bhI':I.b ∉ Ic:ℝhc:c ∈ Set.Ico I.a I.bhK:Ioo c I.b ∈ P ∨ Ico c I.b ∈ P⊢ ∃ K L, K ∈ P ∧ I.joins L K cases I with n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhI':(Ioo a₁ b₁).b ∉ Ioo a₁ b₁hc:c ∈ Set.Ico (Ioo a₁ b₁).a (Ioo a₁ b₁).bhK:Ioo c (Ioo a₁ b₁).b ∈ P ∨ Ico c (Ioo a₁ b₁).b ∈ P⊢ ∃ K L, K ∈ P ∧ (Ioo a₁ b₁).joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhI':(Ioo a₁ b₁).b ∉ Ioo a₁ b₁hc:c ∈ Set.Ico (Ioo a₁ b₁).a (Ioo a₁ b₁).bhK:Ioo c (Ioo a₁ b₁).b ∈ P⊢ ∃ K L, K ∈ P ∧ (Ioo a₁ b₁).joins L Kn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhI':(Ioo a₁ b₁).b ∉ Ioo a₁ b₁hc:c ∈ Set.Ico (Ioo a₁ b₁).a (Ioo a₁ b₁).bhK:Ico c (Ioo a₁ b₁).b ∈ P⊢ ∃ K L, K ∈ P ∧ (Ioo a₁ b₁).joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhI':(Ioo a₁ b₁).b ∉ Ioo a₁ b₁hc:c ∈ Set.Ico (Ioo a₁ b₁).a (Ioo a₁ b₁).bhK:Ioo c (Ioo a₁ b₁).b ∈ P⊢ ∃ K L, K ∈ P ∧ (Ioo a₁ b₁).joins L Kn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhI':(Ioo a₁ b₁).b ∉ Ioo a₁ b₁hc:c ∈ Set.Ico (Ioo a₁ b₁).a (Ioo a₁ b₁).bhK:Ico c (Ioo a₁ b₁).b ∈ P⊢ ∃ K L, K ∈ P ∧ (Ioo a₁ b₁).joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhc:(Ioo a₁ b₁).a ≤ c ∧ c < (Ioo a₁ b₁).bhK:Ico c (Ioo a₁ b₁).b ∈ P⊢ ∃ K ∈ P, ∃ x, (Ioo a₁ b₁).joins x K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhc:(Ioo a₁ b₁).a ≤ c ∧ c < (Ioo a₁ b₁).bhK:Ioo c (Ioo a₁ b₁).b ∈ P⊢ ∃ K ∈ P, ∃ x, (Ioo a₁ b₁).joins x K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhc:(Ioo a₁ b₁).a ≤ c ∧ c < (Ioo a₁ b₁).bhK:Ioo c (Ioo a₁ b₁).b ∈ P⊢ (Ioo a₁ b₁).joins (Ioc a₁ c) (Ioo c b₁); n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhc:(Ioo a₁ b₁).a ≤ c ∧ c < (Ioo a₁ b₁).bhK:Ioo c (Ioo a₁ b₁).b ∈ P⊢ a₁ ≤ cn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhc:(Ioo a₁ b₁).a ≤ c ∧ c < (Ioo a₁ b₁).bhK:Ioo c (Ioo a₁ b₁).b ∈ P⊢ c < b₁ n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhc:(Ioo a₁ b₁).a ≤ c ∧ c < (Ioo a₁ b₁).bhK:Ioo c (Ioo a₁ b₁).b ∈ P⊢ a₁ ≤ cn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhc:(Ioo a₁ b₁).a ≤ c ∧ c < (Ioo a₁ b₁).bhK:Ioo c (Ioo a₁ b₁).b ∈ P⊢ c < b₁ All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhc:(Ioo a₁ b₁).a ≤ c ∧ c < (Ioo a₁ b₁).bhK:Ico c (Ioo a₁ b₁).b ∈ P⊢ (Ioo a₁ b₁).joins (Ioo a₁ c) (Ico c b₁) n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhc:(Ioo a₁ b₁).a ≤ c ∧ c < (Ioo a₁ b₁).bhK:Ico c (Ioo a₁ b₁).b ⊆ Ioo a₁ b₁⊢ (Ioo a₁ b₁).joins (Ioo a₁ c) (Ico c b₁); n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ioo a₁ b₁)hcard:P.intervals.card = n + 1h:(Ioo a₁ b₁).a < (Ioo a₁ b₁).bhc:(Ioo a₁ b₁).a ≤ c ∧ c < (Ioo a₁ b₁).bhK:Set.Ico c (Ioo a₁ b₁).b ⊆ Set.Ioo a₁ b₁⊢ (Ioo a₁ b₁).joins (Ioo a₁ c) (Ico c b₁) have : c ∈ Set.Ico c b₁ := I:BoundedIntervalP:Partition I⊢ ∑ J ∈ P.intervals, J.length = I.length All goals completed! 🐙 All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa✝:ℝb✝:ℝP:Partition (Icc a✝ b✝)hcard:P.intervals.card = n + 1h:(Icc a✝ b✝).a < (Icc a✝ b✝).bhI':(Icc a✝ b✝).b ∉ Icc a✝ b✝hc:c ∈ Set.Ico (Icc a✝ b✝).a (Icc a✝ b✝).bhK:Ioo c (Icc a✝ b✝).b ∈ P ∨ Ico c (Icc a✝ b✝).b ∈ P⊢ ∃ K L, K ∈ P ∧ (Icc a✝ b✝).joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa✝:ℝb✝:ℝP:Partition (Icc a✝ b✝)hcard:P.intervals.card = n + 1h:(Icc a✝ b✝).a < (Icc a✝ b✝).bhc:c ∈ Set.Ico (Icc a✝ b✝).a (Icc a✝ b✝).bhK:Ioo c (Icc a✝ b✝).b ∈ P ∨ Ico c (Icc a✝ b✝).b ∈ PhI':(Icc a✝ b✝).b < a✝⊢ ∃ K L, K ∈ P ∧ (Icc a✝ b✝).joins L K; All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa✝:ℝb✝:ℝP:Partition (Ioc a✝ b✝)hcard:P.intervals.card = n + 1h:(Ioc a✝ b✝).a < (Ioc a✝ b✝).bhI':(Ioc a✝ b✝).b ∉ Ioc a✝ b✝hc:c ∈ Set.Ico (Ioc a✝ b✝).a (Ioc a✝ b✝).bhK:Ioo c (Ioc a✝ b✝).b ∈ P ∨ Ico c (Ioc a✝ b✝).b ∈ P⊢ ∃ K L, K ∈ P ∧ (Ioc a✝ b✝).joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa✝:ℝb✝:ℝP:Partition (Ioc a✝ b✝)hcard:P.intervals.card = n + 1h:(Ioc a✝ b✝).a < (Ioc a✝ b✝).bhc:c ∈ Set.Ico (Ioc a✝ b✝).a (Ioc a✝ b✝).bhK:Ioo c (Ioc a✝ b✝).b ∈ P ∨ Ico c (Ioc a✝ b✝).b ∈ PhI':(Ioc a✝ b✝).b ≤ a✝⊢ ∃ K L, K ∈ P ∧ (Ioc a✝ b✝).joins L K; All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ico a₁ b₁)hcard:P.intervals.card = n + 1h:(Ico a₁ b₁).a < (Ico a₁ b₁).bhI':(Ico a₁ b₁).b ∉ Ico a₁ b₁hc:c ∈ Set.Ico (Ico a₁ b₁).a (Ico a₁ b₁).bhK:Ioo c (Ico a₁ b₁).b ∈ P ∨ Ico c (Ico a₁ b₁).b ∈ P⊢ ∃ K L, K ∈ P ∧ (Ico a₁ b₁).joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ico a₁ b₁)hcard:P.intervals.card = n + 1h:(Ico a₁ b₁).a < (Ico a₁ b₁).bhI':(Ico a₁ b₁).b ∉ Ico a₁ b₁hc:c ∈ Set.Ico (Ico a₁ b₁).a (Ico a₁ b₁).bhK:Ioo c (Ico a₁ b₁).b ∈ P⊢ ∃ K L, K ∈ P ∧ (Ico a₁ b₁).joins L Kn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ico a₁ b₁)hcard:P.intervals.card = n + 1h:(Ico a₁ b₁).a < (Ico a₁ b₁).bhI':(Ico a₁ b₁).b ∉ Ico a₁ b₁hc:c ∈ Set.Ico (Ico a₁ b₁).a (Ico a₁ b₁).bhK:Ico c (Ico a₁ b₁).b ∈ P⊢ ∃ K L, K ∈ P ∧ (Ico a₁ b₁).joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ico a₁ b₁)hcard:P.intervals.card = n + 1h:(Ico a₁ b₁).a < (Ico a₁ b₁).bhI':(Ico a₁ b₁).b ∉ Ico a₁ b₁hc:c ∈ Set.Ico (Ico a₁ b₁).a (Ico a₁ b₁).bhK:Ioo c (Ico a₁ b₁).b ∈ P⊢ ∃ K L, K ∈ P ∧ (Ico a₁ b₁).joins L Kn:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ico a₁ b₁)hcard:P.intervals.card = n + 1h:(Ico a₁ b₁).a < (Ico a₁ b₁).bhI':(Ico a₁ b₁).b ∉ Ico a₁ b₁hc:c ∈ Set.Ico (Ico a₁ b₁).a (Ico a₁ b₁).bhK:Ico c (Ico a₁ b₁).b ∈ P⊢ ∃ K L, K ∈ P ∧ (Ico a₁ b₁).joins L K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ico a₁ b₁)hcard:P.intervals.card = n + 1h:(Ico a₁ b₁).a < (Ico a₁ b₁).bhc:(Ico a₁ b₁).a ≤ c ∧ c < (Ico a₁ b₁).bhK:Ico c (Ico a₁ b₁).b ∈ P⊢ ∃ K ∈ P, ∃ x, (Ico a₁ b₁).joins x K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ico a₁ b₁)hcard:P.intervals.card = n + 1h:(Ico a₁ b₁).a < (Ico a₁ b₁).bhc:(Ico a₁ b₁).a ≤ c ∧ c < (Ico a₁ b₁).bhK:Ioo c (Ico a₁ b₁).b ∈ P⊢ ∃ K ∈ P, ∃ x, (Ico a₁ b₁).joins x K n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ico a₁ b₁)hcard:P.intervals.card = n + 1h:(Ico a₁ b₁).a < (Ico a₁ b₁).bhc:(Ico a₁ b₁).a ≤ c ∧ c < (Ico a₁ b₁).bhK:Ioo c (Ico a₁ b₁).b ∈ P⊢ (Ico a₁ b₁).joins (Icc a₁ c) (Ioo c b₁); All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthc:ℝa₁:ℝb₁:ℝP:Partition (Ico a₁ b₁)hcard:P.intervals.card = n + 1h:(Ico a₁ b₁).a < (Ico a₁ b₁).bhc:(Ico a₁ b₁).a ≤ c ∧ c < (Ico a₁ b₁).bhK:Ico c (Ico a₁ b₁).b ∈ P⊢ (Ico a₁ b₁).joins (Ico a₁ c) (Ico c b₁); All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bK:BoundedIntervalL:BoundedIntervalhK:K ∈ Ph1:↑L ∩ ↑K = ∅h2:↑I = ↑L ∪ ↑Kh3:I.length = L.length + K.length⊢ ∑ J ∈ P.intervals, J.length = I.length have : ∃ P' : Partition L, P'.intervals = P.intervals.erase K := I:BoundedIntervalP:Partition I⊢ ∑ J ∈ P.intervals, J.length = I.length All goals completed! 🐙 n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bK:BoundedIntervalL:BoundedIntervalhK:K ∈ Ph1:↑L ∩ ↑K = ∅h2:↑I = ↑L ∪ ↑Kh3:I.length = L.length + K.lengthP':Partition LhP':P'.intervals = P.intervals.erase K⊢ ∑ J ∈ P.intervals, J.length = I.length n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bK:BoundedIntervalL:BoundedIntervalhK:K ∈ Ph1:↑L ∩ ↑K = ∅h2:↑I = ↑L ∪ ↑Kh3:I.length = L.length + K.lengthP':Partition LhP':P'.intervals = P.intervals.erase K⊢ ∑ x ∈ P'.intervals, x.length + K.length = L.length + K.length; n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bK:BoundedIntervalL:BoundedIntervalhK:K ∈ Ph1:↑L ∩ ↑K = ∅h2:↑I = ↑L ∪ ↑Kh3:I.length = L.length + K.lengthP':Partition LhP':P'.intervals = P.intervals.erase K⊢ ∑ x ∈ P'.intervals, x.length = L.length n:ℕhn:∀ (I : BoundedInterval) (P : Partition I), P.intervals.card = n → ∑ J ∈ P.intervals, J.length = I.lengthI:BoundedIntervalP:Partition Ihcard:P.intervals.card = n + 1h:I.a < I.bK:BoundedIntervalL:BoundedIntervalhK:K ∈ Ph1:↑L ∩ ↑K = ∅h2:↑I = ↑L ∪ ↑Kh3:I.length = L.length + K.lengthP':Partition LhP':P'.intervals = P.intervals.erase K⊢ P'.intervals.card = n; All goals completed! 🐙

Definition 11.1.14 (Finer and coarser partitions)

instance Partition.instLE (I: BoundedInterval) : LE (Partition I) where le P P' := ∀ J ∈ P'.intervals, ∃ K ∈ P, J ⊆ K
instance declaration uses `sorry`Partition.instPreOrder (I: BoundedInterval) : Preorder (Partition I) where le_refl P := I:BoundedIntervalP:Partition I⊢ P ≤ P All goals completed! 🐙 le_trans P P' P'' hP hP' := I:BoundedIntervalP:Partition IP':Partition IP'':Partition IhP:P ≤ P'hP':P' ≤ P''⊢ P ≤ P'' All goals completed! 🐙instance declaration uses `sorry`Partition.instOrderBot (I: BoundedInterval) : OrderBot (Partition I) where bot_le := I:BoundedInterval⊢ ∀ (a : Partition I), ⊥ ≤ a All goals completed! 🐙/-- Example 11.1.15 -/ declaration uses `sorry`example : ∃ P P' : Partition (Icc 1 4), P.intervals = {Ico 1 2, Icc 2 2, Ioo 2 3, Icc 3 4} ∧ P'.intervals = {Icc 1 2, Ioc 2 4} ∧ P' ≤ P := ⊢ ∃ P P', P.intervals = {Ico 1 2, Icc 2 2, Ioo 2 3, Icc 3 4} ∧ P'.intervals = {Icc 1 2, Ioc 2 4} ∧ P' ≤ P All goals completed! 🐙

Definition 11.1.16 (Common refinement).

noncomputable instance Partition.instMax (I: BoundedInterval) : Max (Partition I) where max P P' := { intervals := Finset.image₂ (fun J K ↦ J ∩ K) P.intervals P'.intervals exists_unique x hx := I:BoundedIntervalP:Partition IP':Partition Ix:ℝhx:x ∈ I⊢ ∃! J, J ∈ Finset.image₂ (fun J K ↦ J ∩ K) P.intervals P'.intervals ∧ x ∈ J I:BoundedIntervalP:Partition IP':Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝:J ∈ P.intervals ∧ x ∈ Ja✝:∀ (y : BoundedInterval), (fun J ↦ J ∈ P.intervals ∧ x ∈ J) y → y = J⊢ ∃! J, J ∈ Finset.image₂ (fun J K ↦ J ∩ K) P.intervals P'.intervals ∧ x ∈ J I:BoundedIntervalP:Partition IP':Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝¹:J ∈ P.intervals ∧ x ∈ Ja✝¹:∀ (y : BoundedInterval), (fun J ↦ J ∈ P.intervals ∧ x ∈ J) y → y = JK:BoundedIntervalh✝:K ∈ P'.intervals ∧ x ∈ Ka✝:∀ (y : BoundedInterval), (fun J ↦ J ∈ P'.intervals ∧ x ∈ J) y → y = K⊢ ∃! J, J ∈ Finset.image₂ (fun J K ↦ J ∩ K) P.intervals P'.intervals ∧ x ∈ J I:BoundedIntervalP:Partition IP':Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝¹:J ∈ P.intervals ∧ x ∈ JK:BoundedIntervalh✝:K ∈ P'.intervals ∧ x ∈ Ka✝¹:∀ y ∈ P.intervals, x ∈ y → y = Ja✝:∀ y ∈ P'.intervals, x ∈ y → y = K⊢ ∃! J, (∃ a ∈ P.intervals, ∃ b ∈ P'.intervals, a ∩ b = J) ∧ x ∈ J I:BoundedIntervalP:Partition IP':Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝¹:J ∈ P.intervals ∧ x ∈ JK:BoundedIntervalh✝:K ∈ P'.intervals ∧ x ∈ Ka✝¹:∀ y ∈ P.intervals, x ∈ y → y = Ja✝:∀ y ∈ P'.intervals, x ∈ y → y = K⊢ (∃ a ∈ P.intervals, ∃ b ∈ P'.intervals, a ∩ b = J ∩ K) ∧ x ∈ J ∩ KI:BoundedIntervalP:Partition IP':Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝¹:J ∈ P.intervals ∧ x ∈ JK:BoundedIntervalh✝:K ∈ P'.intervals ∧ x ∈ Ka✝¹:∀ y ∈ P.intervals, x ∈ y → y = Ja✝:∀ y ∈ P'.intervals, x ∈ y → y = K⊢ ∀ (y : BoundedInterval), (∃ a ∈ P.intervals, ∃ b ∈ P'.intervals, a ∩ b = y) ∧ x ∈ y → y = J ∩ K I:BoundedIntervalP:Partition IP':Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝¹:J ∈ P.intervals ∧ x ∈ JK:BoundedIntervalh✝:K ∈ P'.intervals ∧ x ∈ Ka✝¹:∀ y ∈ P.intervals, x ∈ y → y = Ja✝:∀ y ∈ P'.intervals, x ∈ y → y = K⊢ (∃ a ∈ P.intervals, ∃ b ∈ P'.intervals, a ∩ b = J ∩ K) ∧ x ∈ J ∩ K I:BoundedIntervalP:Partition IP':Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝¹:J ∈ P.intervals ∧ x ∈ JK:BoundedIntervalh✝:K ∈ P'.intervals ∧ x ∈ Ka✝¹:∀ y ∈ P.intervals, x ∈ y → y = Ja✝:∀ y ∈ P'.intervals, x ∈ y → y = K⊢ ∃ a ∈ P.intervals, ∃ b ∈ P'.intervals, a ∩ b = J ∩ K; All goals completed! 🐙 I:BoundedIntervalP:Partition IP':Partition Ix:ℝhx:x ∈ IJ:BoundedIntervalh✝¹:J ∈ P.intervals ∧ x ∈ JK:BoundedIntervalh✝:K ∈ P'.intervals ∧ x ∈ Ka✝¹:∀ y ∈ P.intervals, x ∈ y → y = Ja✝:∀ y ∈ P'.intervals, x ∈ y → y = K⊢ ∀ (y x_1 : BoundedInterval), x_1 ∈ P.intervals → ∀ x_2 ∈ P'.intervals, x_1 ∩ x_2 = y → x ∈ y → y = J ∩ K; All goals completed! 🐙 contains L hL := I:BoundedIntervalP:Partition IP':Partition IL:BoundedIntervalhL:L ∈ Finset.image₂ (fun J K ↦ J ∩ K) P.intervals P'.intervals⊢ L ⊆ I I:BoundedIntervalP:Partition IP':Partition IL:BoundedIntervalhL:∃ a ∈ P.intervals, ∃ b ∈ P'.intervals, a ∩ b = L⊢ L ⊆ I; I:BoundedIntervalP:Partition IP':Partition IJ:BoundedIntervalhJ:J ∈ P.intervalsK:BoundedIntervalhK:K ∈ P'.intervals⊢ J ∩ K ⊆ I I:BoundedIntervalP:Partition IP':Partition IJ:BoundedIntervalK:BoundedIntervalhK:K ∈ P'.intervalshJ:J ⊆ I⊢ J ∩ K ⊆ I; I:BoundedIntervalP:Partition IP':Partition IJ:BoundedIntervalK:BoundedIntervalhJ:J ⊆ IhK:K ⊆ I⊢ J ∩ K ⊆ I I:BoundedIntervalP:Partition IP':Partition IJ:BoundedIntervalK:BoundedIntervalhJ:↑J ⊆ ↑IhK:↑K ⊆ ↑I⊢ ↑J ∩ ↑K ⊆ ↑I; All goals completed! 🐙 }
/-- Example 11.1.17. -/ declaration uses `sorry`example : ∃ P P' : Partition (Icc 1 4), P.intervals = {Ico 1 3, Icc 3 4} ∧ P'.intervals = {Icc 1 2, Ioc 2 4} ∧ (P' ⊔ P).intervals.image toSet = {Set.Icc 1 2, Set.Ioo 2 3, Set.Icc 3 4, ∅} := ⊢ ∃ P P', P.intervals = {Ico 1 3, Icc 3 4} ∧ P'.intervals = {Icc 1 2, Ioc 2 4} ∧ Finset.image toSet (P' ⊔ P).intervals = {Set.Icc 1 2, Set.Ioo 2 3, Set.Icc 3 4, ∅} All goals completed! 🐙

Lemma 11.1.8 / Exercise 11.1.4

theorem declaration uses `sorry`BoundedInterval.le_max {I: BoundedInterval} (P P': Partition I) : P ≤ P ⊔ P' ∧ P' ≤ P ⊔ P' := I:BoundedIntervalP:Partition IP':Partition I⊢ P ≤ P ⊔ P' ∧ P' ≤ P ⊔ P' All goals completed! 🐙

Not from textbook: the reverse inclusion

theorem declaration uses `sorry`BoundedInterval.max_le_iff (I: BoundedInterval) {P P' P'': Partition I} {hP : P ≤ P''} {hP': P' ≤ P''} : P ⊔ P' ≤ P'' := I:BoundedIntervalP:Partition IP':Partition IP'':Partition IhP:P ≤ P''hP':P' ≤ P''⊢ P ⊔ P' ≤ P'' All goals completed! 🐙
end Chapter11