Real-valued functions defined on a subset of \(\R\)

• Continuity
• Limits
• Intermediate value theorem

TheoremImage of a segment#

Mathlib states this as ContinuousOn.image_Icc.

ContinuousOn.image_Icc.{u_2, u_3} {α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α]
  [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] [DenselyOrdered α]
  [ConditionallyCompleteLinearOrder β] [OrderTopology β] {f : α → β} {a b : α} (hab : a ≤ b)
  (h : ContinuousOn f (Set.Icc a b)) :
  f '' Set.Icc a b = Set.Icc (sInf (f '' Set.Icc a b)) (sSup (f '' Set.Icc a b))

Sources

• Mathlib documentation: ContinuousOn.image_Icc
• Source of ContinuousOn.image_Icc in Mathlib/Topology/Order/Compact.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Real-valued functions defined on a subset of \(\R\)

MathlibContinuousOn.image_Icc

Uses 4 · Used by 1

Statement usesLimit of a map with respect to filters · Order topology

Proof usesCompactness in terms of filters · Hausdorff space

Used byChange of variable

TheoremContinuity of monotone functions#

Mathlib states this as OrderIso.continuous.

OrderIso.continuous.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β]
  [TopologicalSpace α] [TopologicalSpace β] [OrderTopology α] [OrderTopology β] (e : α ≃o β) :
  Continuous ⇑e

Sources

• Mathlib documentation: OrderIso.continuous
• Source of OrderIso.continuous in Mathlib/Topology/Order/MonotoneContinuity.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Real-valued functions defined on a subset of \(\R\)

MathlibOrderIso.continuous

Uses 2 · Used by 2

Statement usesContinuous function · Order topology

Used byThe Area of a Circle · Hilbert projection theorem

AbbreviationContinuity of inverse functions#

An order isomorphism between two linear order OrderTopology spaces is a homeomorphism.

OrderIso.toHomeomorph.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β]
  [TopologicalSpace α] [TopologicalSpace β] [OrderTopology α] [OrderTopology β] (e : α ≃o β) :
  α ≃ₜ β

Sources

• Mathlib documentation: OrderIso.toHomeomorph
• Source of OrderIso.toHomeomorph in Mathlib/Topology/Order/MonotoneContinuity.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Real-valued functions defined on a subset of \(\R\)

MathlibOrderIso.toHomeomorph

Uses 2

Statement usesHomeomorphisms · Order topology

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.