RealIntervals

Supporting results for the classification of compact one-dimensional manifolds.

theorem OneMfld.RealIntervals.ordconn_of_connected {X : Set ℝ} (conn : IsConnected X) (a : ℝ) (aX : a ∈ X) (b : ℝ) (bX : b ∈ X) : Set.Icc a b ⊆ X

theorem OneMfld.RealIntervals.Real.exists_isGLB {S : Set ℝ} (hne : S.Nonempty) (hbdd : BddBelow S) : ∃ (x : ℝ), IsGLB S x

theorem OneMfld.RealIntervals.connected_bddAbove_subset_contains_Ioo {X : Set ℝ} {supX x : ℝ} (conn : IsConnected X) (h_supX : IsLUB X supX) (xX : x ∈ X) : Set.Ioo x supX ⊆ X

theorem OneMfld.RealIntervals.connected_bddBelow_subset_contains_Ioo {X : Set ℝ} {infX x : ℝ} (conn : IsConnected X) (h_infX : IsGLB X infX) (xX : x ∈ X) : Set.Ioo infX x ⊆ X

theorem OneMfld.RealIntervals.connected_bdd_subset_contains_Ioo {X : Set ℝ} {infX supX : ℝ} (conn : IsConnected X) (h_infX : IsGLB X infX) (h_supX : IsLUB X supX) : Set.Ioo infX supX ⊆ X

theorem OneMfld.RealIntervals.bdd_subset_Icc {X : Set ℝ} {infX supX : ℝ} (h_infX : IsGLB X infX) (h_supX : IsLUB X supX) : X ⊆ Set.Icc infX supX

theorem OneMfld.RealIntervals.x_lt_excluded_supX {X : Set ℝ} {x supX : ℝ} (xX : x ∈ X) (h_supX : IsLUB X supX) (supX_X : supX ∉ X) : x < supX

theorem OneMfld.RealIntervals.excluded_infX_lt_x {X : Set ℝ} {x infX : ℝ} (xX : x ∈ X) (h_infX : IsGLB X infX) (infX_X : infX ∉ X) : infX < x

theorem OneMfld.RealIntervals.Ico_Ioo_with_endpoint {a b : ℝ} (hab : a < b) : Set.Ico a b = Set.Ioo a b ∪ {a}

theorem OneMfld.RealIntervals.Ioc_Ioo_with_endpoint {a b : ℝ} (hab : a < b) : Set.Ioc a b = Set.Ioo a b ∪ {b}

theorem OneMfld.RealIntervals.characterize_Ioo {X : Set ℝ} (conn : IsConnected X) {infX supX : ℝ} (h_infX : IsGLB X infX) (h_supX : IsLUB X supX) (infX_X : infX ∉ X) (supX_X : supX ∉ X) : X = Set.Ioo infX supX

theorem OneMfld.RealIntervals.characterize_Ioc {X : Set ℝ} (conn : IsConnected X) {infX supX : ℝ} (inf_lt_sup : infX < supX) (h_infX : IsGLB X infX) (h_supX : IsLUB X supX) (infX_X : infX ∉ X) (supX_X : supX ∈ X) : X = Set.Ioc infX supX

theorem OneMfld.RealIntervals.characterize_Ico {X : Set ℝ} (conn : IsConnected X) {infX supX : ℝ} (inf_lt_sup : infX < supX) (h_infX : IsGLB X infX) (h_supX : IsLUB X supX) (infX_X : infX ∈ X) (supX_X : supX ∉ X) : X = Set.Ico infX supX

theorem OneMfld.RealIntervals.characterize_Icc {X : Set ℝ} (conn : IsConnected X) {infX supX : ℝ} (h_infX : IsGLB X infX) (h_supX : IsLUB X supX) (infX_X : infX ∈ X) (supX_X : supX ∈ X) : X = Set.Icc infX supX

theorem OneMfld.RealIntervals.characterize_singleton {X : Set ℝ} {a : ℝ} (h_infX : IsGLB X a) (h_supX : IsLUB X a) : X = {a}

inductive OneMfld.RealIntervals.BoundedIntervalKind : Type

The four possibilities for including the two endpoints of a bounded interval.

• IooKind : BoundedIntervalKind
• IocKind : BoundedIntervalKind
• IcoKind : BoundedIntervalKind
• IccKind : BoundedIntervalKind

structure OneMfld.RealIntervals.BoundedInterval : Type

Two ordered real endpoints together with their inclusion convention.

• leftEndpoint : ℝ

  The left endpoint of the interval.

• rightEndpoint : ℝ

  The right endpoint of the interval.

• left_lt_right : self.leftEndpoint < self.rightEndpoint
• kind : BoundedIntervalKind

  Which endpoints belong to the interval.

def OneMfld.RealIntervals.BoundedIntervalAsSet : BoundedInterval → Set ℝ

Interpret the interval's endpoints and inclusion convention as a set of reals.

Equations

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

def OneMfld.RealIntervals.isBoundedInterval (X : Set ℝ) : Prop

The set is a nondegenerate bounded interval with some endpoint convention.

Equations

• OneMfld.RealIntervals.isBoundedInterval X = ∃ (I : OneMfld.RealIntervals.BoundedInterval), X = OneMfld.RealIntervals.BoundedIntervalAsSet I

theorem OneMfld.RealIntervals.isBoundedInterval_Ioo (a b : ℝ) (lt : a < b) : isBoundedInterval (Set.Ioo a b)

theorem OneMfld.RealIntervals.isBoundedInterval_Ioc (a b : ℝ) (lt : a < b) : isBoundedInterval (Set.Ioc a b)

theorem OneMfld.RealIntervals.isBoundedInterval_Ico (a b : ℝ) (lt : a < b) : isBoundedInterval (Set.Ico a b)

theorem OneMfld.RealIntervals.isBoundedInterval_Icc (a b : ℝ) (lt : a < b) : isBoundedInterval (Set.Icc a b)

def OneMfld.RealIntervals.isSingleton (X : Set ℝ) : Prop

The set consists of exactly one real number.

Equations

• OneMfld.RealIntervals.isSingleton X = ∃ (a : ℝ), X = {a}

theorem OneMfld.RealIntervals.classify_connected_reals_with_GLB_lt_LUB {X : Set ℝ} (conn : IsConnected X) {infX supX : ℝ} (h_infX : IsGLB X infX) (h_supX : IsLUB X supX) (lt : infX < supX) : isBoundedInterval X

theorem OneMfld.RealIntervals.classify_connected_bounded_reals {X : Set ℝ} (conn : IsConnected X) (above : BddAbove X) (below : BddBelow X) : isSingleton X ∨ isBoundedInterval X

theorem OneMfld.RealIntervals.classify_connected_bounded_reals_nonempty_interior {X : Set ℝ} (conn : IsConnected X) (above : BddAbove X) (below : BddBelow X) (h : interior X ≠ ∅) : isBoundedInterval X

theorem OneMfld.RealIntervals.isConnected_BoundedInterval (I : BoundedInterval) : IsConnected (BoundedIntervalAsSet I)

theorem OneMfld.RealIntervals.BoundedInterval_subset_Icc (I : BoundedInterval) : BoundedIntervalAsSet I ⊆ Set.Icc I.leftEndpoint I.rightEndpoint

theorem OneMfld.RealIntervals.BoundedInterval_contains_Ioo (I : BoundedInterval) : Set.Ioo I.leftEndpoint I.rightEndpoint ⊆ BoundedIntervalAsSet I

theorem OneMfld.RealIntervals.closure_BoundedInterval (I : BoundedInterval) : closure (BoundedIntervalAsSet I) = Set.Icc I.leftEndpoint I.rightEndpoint

theorem OneMfld.RealIntervals.isBoundedBelow_BoundedInterval (I : BoundedInterval) : BddBelow (BoundedIntervalAsSet I)

theorem OneMfld.RealIntervals.isBoundedAbove_BoundedInterval (I : BoundedInterval) : BddAbove (BoundedIntervalAsSet I)

@[simp]

theorem OneMfld.RealIntervals.interior_BoundedInterval (I : BoundedInterval) : interior (BoundedIntervalAsSet I) = Set.Ioo I.leftEndpoint I.rightEndpoint

@[simp]

theorem OneMfld.RealIntervals.Icc_diff_Ioo {a b : ℝ} (lt : a < b) : Set.Icc a b \ Set.Ioo a b = {a, b}

@[simp]

theorem OneMfld.RealIntervals.frontier_BoundedInterval (I : BoundedInterval) : frontier (BoundedIntervalAsSet I) = {I.leftEndpoint, I.rightEndpoint}

theorem OneMfld.RealIntervals.pair_has_other {a b c : ℝ} (ne : a ≠ b) (h : c ∈ {a, b}) : ∃ d ∈ {a, b}, d ≠ c

theorem OneMfld.RealIntervals.other_endpoint {X : Set ℝ} (int : interior X ≠ ∅) (conn : IsConnected X) (above : BddAbove X) (below : BddBelow X) (a : ℝ) (ha : a ∈ frontier X) : ∃ b ∈ frontier X, b ≠ a

theorem OneMfld.RealIntervals.characterize_univ {X : Set ℝ} (conn : IsConnected X) (below : ¬BddBelow X) (above : ¬BddAbove X) : X = Set.univ

theorem OneMfld.RealIntervals.characterize_Ioi {X : Set ℝ} (conn : IsConnected X) {infX : ℝ} (h_infX : IsGLB X infX) (infX_X : infX ∉ X) (above : ¬BddAbove X) : X = Set.Ioi infX

theorem OneMfld.RealIntervals.characterize_Ici {X : Set ℝ} (conn : IsConnected X) {infX : ℝ} (h_infX : IsGLB X infX) (infX_X : infX ∈ X) (above : ¬BddAbove X) : X = Set.Ici infX

theorem OneMfld.RealIntervals.classify_Ixi {X : Set ℝ} (conn : IsConnected X) (below : BddBelow X) (above : ¬BddAbove X) : ∃ (a : ℝ), X = Set.Ioi a ∨ X = Set.Ici a

theorem OneMfld.RealIntervals.characterize_Iio {X : Set ℝ} (conn : IsConnected X) {supX : ℝ} (h_supX : IsLUB X supX) (supX_X : supX ∉ X) (below : ¬BddBelow X) : X = Set.Iio supX

theorem OneMfld.RealIntervals.characterize_Iic {X : Set ℝ} (conn : IsConnected X) {supX : ℝ} (h_supX : IsLUB X supX) (supX_X : supX ∈ X) (below : ¬BddBelow X) : X = Set.Iic supX

theorem OneMfld.RealIntervals.classify_Iix {X : Set ℝ} (conn : IsConnected X) (below : ¬BddBelow X) (above : BddAbove X) : ∃ (a : ℝ), X = Set.Iio a ∨ X = Set.Iic a

inductive OneMfld.RealIntervals.ConnectedRealClassification : Type

The possible forms of a nonempty connected subset of the real line.

• of_univ : ConnectedRealClassification
• of_Iio : ℝ → ConnectedRealClassification
• of_Iic : ℝ → ConnectedRealClassification
• of_Ioi : ℝ → ConnectedRealClassification
• of_Ici : ℝ → ConnectedRealClassification
• of_singleton : ℝ → ConnectedRealClassification
• of_bounded_interval : BoundedInterval → ConnectedRealClassification

def OneMfld.RealIntervals.ConnectedRealClassificationAsSet : ConnectedRealClassification → Set ℝ

Interpret a connected-set classification as a subset of the real line.

Equations

• OneMfld.RealIntervals.ConnectedRealClassificationAsSet OneMfld.RealIntervals.ConnectedRealClassification.of_univ = Set.univ
• OneMfld.RealIntervals.ConnectedRealClassificationAsSet (OneMfld.RealIntervals.ConnectedRealClassification.of_Iio a) = Set.Iio a
• OneMfld.RealIntervals.ConnectedRealClassificationAsSet (OneMfld.RealIntervals.ConnectedRealClassification.of_Iic a) = Set.Iic a
• OneMfld.RealIntervals.ConnectedRealClassificationAsSet (OneMfld.RealIntervals.ConnectedRealClassification.of_Ioi a) = Set.Ioi a
• OneMfld.RealIntervals.ConnectedRealClassificationAsSet (OneMfld.RealIntervals.ConnectedRealClassification.of_Ici a) = Set.Ici a
• OneMfld.RealIntervals.ConnectedRealClassificationAsSet (OneMfld.RealIntervals.ConnectedRealClassification.of_singleton a) = {a}
• OneMfld.RealIntervals.ConnectedRealClassificationAsSet (OneMfld.RealIntervals.ConnectedRealClassification.of_bounded_interval I) = OneMfld.RealIntervals.BoundedIntervalAsSet I

def OneMfld.RealIntervals.isConnectedRealClassification (X : Set ℝ) : Prop

The set is represented by one of the connected real-set forms.

Equations

• OneMfld.RealIntervals.isConnectedRealClassification X = ∃ (I : OneMfld.RealIntervals.ConnectedRealClassification), X = OneMfld.RealIntervals.ConnectedRealClassificationAsSet I

theorem OneMfld.RealIntervals.classify_connected_reals {X : Set ℝ} (conn : IsConnected X) : isConnectedRealClassification X