Topology on extended non-negative reals

theorem ENNReal.isOpen_ne_top : IsOpen {a : ENNReal | a ≠ ⊤}

theorem ENNReal.isOpen_Ico_zero {b : ENNReal} : IsOpen (Set.Ico 0 b)

theorem ENNReal.coe_range_mem_nhds {r : NNReal} : Set.range ofNNReal ∈ nhds ↑r

theorem ENNReal.continuous_coe : Continuous ofNNReal

theorem ENNReal.tendsto_coe_toNNReal {a : ENNReal} (ha : a ≠ ⊤) : Filter.Tendsto ofNNReal (nhds a.toNNReal) (nhds a)

theorem ENNReal.continuous_coe_iff {α : Type u_4} [TopologicalSpace α] {f : α → NNReal} : (Continuous fun (a : α) => ↑(f a)) ↔ Continuous f

theorem ENNReal.nhds_coe {r : NNReal} : nhds ↑r = Filter.map ofNNReal (nhds r)

theorem ENNReal.tendsto_nhds_coe_iff {α : Type u_4} {l : Filter α} {x : NNReal} {f : ENNReal → α} : Filter.Tendsto f (nhds ↑x) l ↔ Filter.Tendsto (f ∘ ofNNReal) (nhds x) l

theorem ENNReal.continuousAt_coe_iff {α : Type u_4} [TopologicalSpace α] {x : NNReal} {f : ENNReal → α} : ContinuousAt f ↑x ↔ ContinuousAt (f ∘ ofNNReal) x

theorem ENNReal.continuous_ofReal : Continuous ENNReal.ofReal

theorem ENNReal.tendsto_ofReal {α : Type u_1} {f : Filter α} {m : α → ℝ} {a : ℝ} (h : Filter.Tendsto m f (nhds a)) : Filter.Tendsto (fun (a : α) => ENNReal.ofReal (m a)) f (nhds (ENNReal.ofReal a))

theorem ENNReal.tendsto_toNNReal {a : ENNReal} (ha : a ≠ ⊤) : Filter.Tendsto ENNReal.toNNReal (nhds a) (nhds a.toNNReal)

theorem ENNReal.tendsto_toNNReal_iff {α : Type u_1} {a : ENNReal} {f : α → ENNReal} {u : Filter α} (ha : a ≠ ⊤) (hf : ∀ (x : α), f x ≠ ⊤) : Filter.Tendsto (ENNReal.toNNReal ∘ f) u (nhds a.toNNReal) ↔ Filter.Tendsto f u (nhds a)

theorem ENNReal.tendsto_toNNReal_iff' {α : Type u_1} {f : α → ENNReal} {u : Filter α} {a : NNReal} (hf : ∀ (x : α), f x ≠ ⊤) : Filter.Tendsto (ENNReal.toNNReal ∘ f) u (nhds a) ↔ Filter.Tendsto f u (nhds ↑a)

theorem ENNReal.eventuallyEq_of_toReal_eventuallyEq {α : Type u_1} {l : Filter α} {f g : α → ENNReal} (hfi : ∀ᶠ (x : α) in l, f x ≠ ⊤) (hgi : ∀ᶠ (x : α) in l, g x ≠ ⊤) (hfg : (fun (x : α) => (f x).toReal) =ᶠ[l] fun (x : α) => (g x).toReal) : f =ᶠ[l] g

theorem ENNReal.continuousOn_toNNReal : ContinuousOn ENNReal.toNNReal {a : ENNReal | a ≠ ⊤}

theorem ENNReal.tendsto_toReal {a : ENNReal} (ha : a ≠ ⊤) : Filter.Tendsto ENNReal.toReal (nhds a) (nhds a.toReal)

theorem ENNReal.continuousOn_toReal : ContinuousOn ENNReal.toReal {a : ENNReal | a ≠ ⊤}

theorem ENNReal.continuousAt_toReal {x : ENNReal} (hx : x ≠ ⊤) : ContinuousAt ENNReal.toReal x

def ENNReal.neTopHomeomorphNNReal : ↑{a : ENNReal | a ≠ ⊤} ≃ₜ NNReal

The set of finite ℝ≥0∞ numbers is homeomorphic to ℝ≥0.

Equations

• ENNReal.neTopHomeomorphNNReal = { toEquiv := ENNReal.neTopEquivNNReal, continuous_toFun := ENNReal.neTopHomeomorphNNReal._proof_1, continuous_invFun := ENNReal.neTopHomeomorphNNReal._proof_2 }

def ENNReal.ltTopHomeomorphNNReal : ↑{a : ENNReal | a < ⊤} ≃ₜ NNReal

The set of finite ℝ≥0∞ numbers is homeomorphic to ℝ≥0.

Equations

• ENNReal.ltTopHomeomorphNNReal = (Homeomorph.setCongr ENNReal.ltTopHomeomorphNNReal._proof_1).trans ENNReal.neTopHomeomorphNNReal

theorem ENNReal.nhds_top : nhds ⊤ = ⨅ (a : ENNReal), ⨅ (_ : a ≠ ⊤), Filter.principal (Set.Ioi a)

theorem ENNReal.nhds_top' : nhds ⊤ = ⨅ (r : NNReal), Filter.principal (Set.Ioi ↑r)

theorem ENNReal.nhds_top_basis : (nhds ⊤).HasBasis (fun (a : ENNReal) => a < ⊤) fun (a : ENNReal) => Set.Ioi a

theorem ENNReal.tendsto_nhds_top_iff_nnreal {α : Type u_1} {m : α → ENNReal} {f : Filter α} : Filter.Tendsto m f (nhds ⊤) ↔ ∀ (x : NNReal), ∀ᶠ (a : α) in f, ↑x < m a

theorem ENNReal.tendsto_nhds_top_iff_nat {α : Type u_1} {m : α → ENNReal} {f : Filter α} : Filter.Tendsto m f (nhds ⊤) ↔ ∀ (n : ℕ), ∀ᶠ (a : α) in f, ↑n < m a

theorem ENNReal.tendsto_nhds_top {α : Type u_1} {m : α → ENNReal} {f : Filter α} (h : ∀ (n : ℕ), ∀ᶠ (a : α) in f, ↑n < m a) : Filter.Tendsto m f (nhds ⊤)

theorem ENNReal.tendsto_nat_nhds_top : Filter.Tendsto (fun (n : ℕ) => ↑n) Filter.atTop (nhds ⊤)

@[simp]

theorem ENNReal.tendsto_coe_nhds_top {α : Type u_1} {f : α → NNReal} {l : Filter α} : Filter.Tendsto (fun (x : α) => ↑(f x)) l (nhds ⊤) ↔ Filter.Tendsto f l Filter.atTop

@[simp]

theorem ENNReal.tendsto_ofReal_nhds_top {α : Type u_1} {f : α → ℝ} {l : Filter α} : Filter.Tendsto (fun (x : α) => ENNReal.ofReal (f x)) l (nhds ⊤) ↔ Filter.Tendsto f l Filter.atTop

theorem ENNReal.tendsto_ofReal_atTop : Filter.Tendsto ENNReal.ofReal Filter.atTop (nhds ⊤)

theorem ENNReal.nhds_zero : nhds 0 = ⨅ (a : ENNReal), ⨅ (_ : a ≠ 0), Filter.principal (Set.Iio a)

theorem ENNReal.nhds_zero_basis : (nhds 0).HasBasis (fun (a : ENNReal) => 0 < a) fun (a : ENNReal) => Set.Iio a

theorem ENNReal.nhds_zero_basis_Iic : (nhds 0).HasBasis (fun (a : ENNReal) => 0 < a) Set.Iic

instance ENNReal.nhdsGT_coe_neBot {r : NNReal} : (nhdsWithin (↑r) (Set.Ioi ↑r)).NeBot

instance ENNReal.nhdsGT_zero_neBot : (nhdsWithin 0 (Set.Ioi 0)).NeBot

instance ENNReal.nhdsGT_one_neBot : (nhdsWithin 1 (Set.Ioi 1)).NeBot

instance ENNReal.nhdsGT_nat_neBot (n : ℕ) : (nhdsWithin (↑n) (Set.Ioi ↑n)).NeBot

instance ENNReal.nhdsGT_ofNat_neBot (n : ℕ) [n.AtLeastTwo] : (nhdsWithin (OfNat.ofNat n) (Set.Ioi (OfNat.ofNat n))).NeBot

instance ENNReal.nhdsLT_neBot {x : ENNReal} [NeZero x] : (nhdsWithin x (Set.Iio x)).NeBot

theorem ENNReal.hasBasis_nhds_of_ne_top' {x : ENNReal} (xt : x ≠ ⊤) : (nhds x).HasBasis (fun (x : ENNReal) => x ≠ 0) fun (ε : ENNReal) => Set.Icc (x - ε) (x + ε)

Closed intervals Set.Icc (x - ε) (x + ε), ε ≠ 0, form a basis of neighborhoods of an extended nonnegative real number x ≠ ∞. We use Set.Icc instead of Set.Ioo because this way the statement works for x = 0.

theorem ENNReal.hasBasis_nhds_of_ne_top {x : ENNReal} (xt : x ≠ ⊤) : (nhds x).HasBasis (fun (x : ENNReal) => 0 < x) fun (ε : ENNReal) => Set.Icc (x - ε) (x + ε)

theorem ENNReal.Icc_mem_nhds {x ε : ENNReal} (xt : x ≠ ⊤) (ε0 : ε ≠ 0) : Set.Icc (x - ε) (x + ε) ∈ nhds x

theorem ENNReal.nhds_of_ne_top {x : ENNReal} (xt : x ≠ ⊤) : nhds x = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal (Set.Icc (x - ε) (x + ε))

theorem ENNReal.biInf_le_nhds (x : ENNReal) : ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal (Set.Icc (x - ε) (x + ε)) ≤ nhds x

theorem ENNReal.tendsto_nhds_of_Icc {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (h : ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Set.Icc (a - ε) (a + ε)) : Filter.Tendsto u f (nhds a)

theorem ENNReal.tendsto_nhds {α : Type u_1} {f : Filter α} {u : α → ENNReal} {a : ENNReal} (ha : a ≠ ⊤) : Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ∈ Set.Icc (a - ε) (a + ε)

Characterization of neighborhoods for ℝ≥0∞ numbers. See also tendsto_order for a version with strict inequalities.

theorem ENNReal.tendsto_nhds_zero {α : Type u_1} {f : Filter α} {u : α → ENNReal} : Filter.Tendsto u f (nhds 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ≤ ε

theorem ENNReal.tendsto_const_sub_nhds_zero_iff {α : Type u_1} {l : Filter α} {f : α → ENNReal} {a : ENNReal} (ha : a ≠ ⊤) (hfa : ∀ (n : α), f n ≤ a) : Filter.Tendsto (fun (n : α) => a - f n) l (nhds 0) ↔ Filter.Tendsto (fun (n : α) => f n) l (nhds a)

theorem ENNReal.tendsto_atTop {β : Type u_2} [Nonempty β] [SemilatticeSup β] {f : β → ENNReal} {a : ENNReal} (ha : a ≠ ⊤) : Filter.Tendsto f Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ∈ Set.Icc (a - ε) (a + ε)

theorem ENNReal.tendsto_atTop_zero {β : Type u_2} [Nonempty β] [SemilatticeSup β] {f : β → ENNReal} : Filter.Tendsto f Filter.atTop (nhds 0) ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, f n ≤ ε

theorem ENNReal.tendsto_atTop_zero_iff_le_of_antitone {β : Type u_4} [Nonempty β] [SemilatticeSup β] {f : β → ENNReal} (hf : Antitone f) : Filter.Tendsto f Filter.atTop (nhds 0) ↔ ∀ (ε : ENNReal), 0 < ε → ∃ (n : β), f n ≤ ε

theorem ENNReal.tendsto_atTop_zero_iff_lt_of_antitone {β : Type u_4} [Nonempty β] [SemilatticeSup β] {f : β → ENNReal} (hf : Antitone f) : Filter.Tendsto f Filter.atTop (nhds 0) ↔ ∀ (ε : ENNReal), 0 < ε → ∃ (n : β), f n < ε

theorem ENNReal.tendsto_sub {a b : ENNReal} : a ≠ ⊤ ∨ b ≠ ⊤ → Filter.Tendsto (fun (p : ENNReal × ENNReal) => p.1 - p.2) (nhds (a, b)) (nhds (a - b))

theorem ENNReal.Tendsto.sub {α : Type u_1} {f : Filter α} {ma mb : α → ENNReal} {a b : ENNReal} (hma : Filter.Tendsto ma f (nhds a)) (hmb : Filter.Tendsto mb f (nhds b)) (h : a ≠ ⊤ ∨ b ≠ ⊤) : Filter.Tendsto (fun (a : α) => ma a - mb a) f (nhds (a - b))

theorem ENNReal.tendsto_mul {a b : ENNReal} (ha : a ≠ 0 ∨ b ≠ ⊤) (hb : b ≠ 0 ∨ a ≠ ⊤) : Filter.Tendsto (fun (p : ENNReal × ENNReal) => p.1 * p.2) (nhds (a, b)) (nhds (a * b))

theorem ENNReal.Tendsto.mul {α : Type u_1} {f : Filter α} {ma mb : α → ENNReal} {a b : ENNReal} (hma : Filter.Tendsto ma f (nhds a)) (ha : a ≠ 0 ∨ b ≠ ⊤) (hmb : Filter.Tendsto mb f (nhds b)) (hb : b ≠ 0 ∨ a ≠ ⊤) : Filter.Tendsto (fun (a : α) => ma a * mb a) f (nhds (a * b))

theorem ContinuousOn.ennreal_mul {α : Type u_1} [TopologicalSpace α] {f g : α → ENNReal} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h₁ : ∀ x ∈ s, f x ≠ 0 ∨ g x ≠ ⊤) (h₂ : ∀ x ∈ s, g x ≠ 0 ∨ f x ≠ ⊤) : ContinuousOn (fun (x : α) => f x * g x) s

theorem Continuous.ennreal_mul {α : Type u_1} [TopologicalSpace α] {f g : α → ENNReal} (hf : Continuous f) (hg : Continuous g) (h₁ : ∀ (x : α), f x ≠ 0 ∨ g x ≠ ⊤) (h₂ : ∀ (x : α), g x ≠ 0 ∨ f x ≠ ⊤) : Continuous fun (x : α) => f x * g x

theorem ENNReal.Tendsto.const_mul {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a b : ENNReal} (hm : Filter.Tendsto m f (nhds b)) (hb : b ≠ 0 ∨ a ≠ ⊤) : Filter.Tendsto (fun (b : α) => a * m b) f (nhds (a * b))

theorem ENNReal.Tendsto.mul_const {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a b : ENNReal} (hm : Filter.Tendsto m f (nhds a)) (ha : a ≠ 0 ∨ b ≠ ⊤) : Filter.Tendsto (fun (x : α) => m x * b) f (nhds (a * b))

theorem ENNReal.tendsto_finset_prod_of_ne_top {α : Type u_1} {ι : Type u_4} {f : ι → α → ENNReal} {x : Filter α} {a : ι → ENNReal} (s : Finset ι) (h : ∀ i ∈ s, Filter.Tendsto (f i) x (nhds (a i))) (h' : ∀ i ∈ s, a i ≠ ⊤) : Filter.Tendsto (fun (b : α) => ∏ c ∈ s, f c b) x (nhds (∏ c ∈ s, a c))

theorem ENNReal.continuousAt_const_mul {a b : ENNReal} (h : a ≠ ⊤ ∨ b ≠ 0) : ContinuousAt (fun (x : ENNReal) => a * x) b

theorem ENNReal.continuousAt_mul_const {a b : ENNReal} (h : a ≠ ⊤ ∨ b ≠ 0) : ContinuousAt (fun (x : ENNReal) => x * a) b

theorem ENNReal.continuous_const_mul {a : ENNReal} (ha : a ≠ ⊤) : Continuous fun (x : ENNReal) => a * x

theorem ENNReal.continuous_mul_const {a : ENNReal} (ha : a ≠ ⊤) : Continuous fun (x : ENNReal) => x * a

theorem ENNReal.continuous_div_const (c : ENNReal) (c_ne_zero : c ≠ 0) : Continuous fun (x : ENNReal) => x / c

theorem ENNReal.continuous_pow (n : ℕ) : Continuous fun (a : ENNReal) => a ^ n

theorem ENNReal.continuousOn_sub : ContinuousOn (fun (p : ENNReal × ENNReal) => p.1 - p.2) {p : ENNReal × ENNReal | p ≠ (⊤, ⊤)}

theorem ENNReal.continuous_sub_left {a : ENNReal} (a_ne_top : a ≠ ⊤) : Continuous fun (x : ENNReal) => a - x

theorem ENNReal.continuous_nnreal_sub {a : NNReal} : Continuous fun (x : ENNReal) => ↑a - x

theorem ENNReal.continuousOn_sub_left (a : ENNReal) : ContinuousOn (fun (x : ENNReal) => a - x) {x : ENNReal | x ≠ ⊤}

theorem ENNReal.continuous_sub_right (a : ENNReal) : Continuous fun (x : ENNReal) => x - a

theorem ENNReal.Tendsto.pow {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a : ENNReal} {n : ℕ} (hm : Filter.Tendsto m f (nhds a)) : Filter.Tendsto (fun (x : α) => m x ^ n) f (nhds (a ^ n))

theorem ENNReal.le_of_forall_lt_one_mul_le {x y : ENNReal} (h : ∀ a < 1, a * x ≤ y) : x ≤ y

theorem ENNReal.inv_limsup {ι : Type u_4} {x : ι → ENNReal} {l : Filter ι} : (Filter.limsup x l)⁻¹ = Filter.liminf (fun (i : ι) => (x i)⁻¹) l

theorem ENNReal.inv_liminf {ι : Type u_4} {x : ι → ENNReal} {l : Filter ι} : (Filter.liminf x l)⁻¹ = Filter.limsup (fun (i : ι) => (x i)⁻¹) l

theorem ENNReal.continuous_zpow (n : ℤ) : Continuous fun (x : ENNReal) => x ^ n

@[deprecated tendsto_inv_iff (since := "2026-01-15")]

theorem ENNReal.tendsto_inv_iff {G : Type w} {α : Type u} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] {l : Filter α} {m : α → G} {a : G} : Filter.Tendsto (fun (x : α) => (m x)⁻¹) l (nhds a⁻¹) ↔ Filter.Tendsto m l (nhds a)

Alias of tendsto_inv_iff.

theorem ENNReal.Tendsto.div {α : Type u_1} {f : Filter α} {ma mb : α → ENNReal} {a b : ENNReal} (hma : Filter.Tendsto ma f (nhds a)) (ha : a ≠ 0 ∨ b ≠ 0) (hmb : Filter.Tendsto mb f (nhds b)) (hb : b ≠ ⊤ ∨ a ≠ ⊤) : Filter.Tendsto (fun (a : α) => ma a / mb a) f (nhds (a / b))

theorem ENNReal.Tendsto.const_div {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a b : ENNReal} (hm : Filter.Tendsto m f (nhds b)) (hb : b ≠ ⊤ ∨ a ≠ ⊤) : Filter.Tendsto (fun (b : α) => a / m b) f (nhds (a / b))

theorem ENNReal.Tendsto.div_const {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a b : ENNReal} (hm : Filter.Tendsto m f (nhds a)) (ha : a ≠ 0 ∨ b ≠ 0) : Filter.Tendsto (fun (x : α) => m x / b) f (nhds (a / b))

theorem ENNReal.tendsto_inv_nat_nhds_zero : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹) Filter.atTop (nhds 0)

theorem ENNReal.tendsto_coe_sub {r : NNReal} {b : ENNReal} : Filter.Tendsto (fun (b : ENNReal) => ↑r - b) (nhds b) (nhds (↑r - b))

theorem ENNReal.exists_countable_dense_no_zero_top : ∃ (s : Set ENNReal), s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ⊤ ∉ s

theorem ENNReal.exists_frequently_lt_of_liminf_ne_top {ι : Type u_4} {l : Filter ι} {x : ι → ℝ} (hx : Filter.liminf (fun (n : ι) => ↑(Real.nnabs (x n))) l ≠ ⊤) : ∃ (R : ℝ), ∃ᶠ (n : ι) in l, x n < R

theorem ENNReal.exists_frequently_lt_of_liminf_ne_top' {ι : Type u_4} {l : Filter ι} {x : ι → ℝ} (hx : Filter.liminf (fun (n : ι) => ↑(Real.nnabs (x n))) l ≠ ⊤) : ∃ (R : ℝ), ∃ᶠ (n : ι) in l, R < x n

theorem ENNReal.exists_upcrossings_of_not_bounded_under {ι : Type u_4} {l : Filter ι} {x : ι → ℝ} (hf : Filter.liminf (fun (i : ι) => ↑(Real.nnabs (x i))) l ≠ ⊤) (hbdd : ¬Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (i : ι) => |x i|) : ∃ (a : ℚ) (b : ℚ), a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

theorem ENNReal.tendsto_toReal_iff {ι : Type u_4} {fi : Filter ι} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤) {x : ENNReal} (hx : x ≠ ⊤) : Filter.Tendsto (fun (n : ι) => (f n).toReal) fi (nhds x.toReal) ↔ Filter.Tendsto f fi (nhds x)

theorem ENNReal.tendsto_toReal_zero_iff {ι : Type u_4} {fi : Filter ι} {f : ι → ENNReal} (hf : ∀ (i : ι), f i ≠ ⊤ := by finiteness) : Filter.Tendsto (fun (n : ι) => (f n).toReal) fi (nhds 0) ↔ Filter.Tendsto f fi (nhds 0)

theorem edist_ne_top_of_mem_ball {β : Type u_2} [EMetricSpace β] {a : β} {r : ENNReal} (x y : ↑(EMetric.ball a r)) : edist ↑x ↑y ≠ ⊤

In an emetric ball, the distance between points is everywhere finite

def metricSpaceEMetricBall {β : Type u_2} [EMetricSpace β] (a : β) (r : ENNReal) : MetricSpace ↑(EMetric.ball a r)

Each ball in an extended metric space gives us a metric space, as the edist is everywhere finite.

Equations

• metricSpaceEMetricBall a r = EMetricSpace.toMetricSpace ⋯

theorem nhds_eq_nhds_emetric_ball {β : Type u_2} [EMetricSpace β] (a x : β) (r : ENNReal) (h : x ∈ EMetric.ball a r) : nhds x = Filter.map Subtype.val (nhds ⟨x, h⟩)

theorem tendsto_iff_edist_tendsto_0 {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] {l : Filter β} {f : β → α} {y : α} : Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (fun (x : β) => edist (f x) y) l (nhds 0)

theorem EMetric.cauchySeq_iff_le_tendsto_0 {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [Nonempty β] [SemilatticeSup β] {s : β → α} : CauchySeq s ↔ ∃ (b : β → ENNReal), (∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N) ∧ Filter.Tendsto b Filter.atTop (nhds 0)

Yet another metric characterization of Cauchy sequences on integers. This one is often the most efficient.

theorem continuous_of_le_add_edist {α : Type u_1} [PseudoEMetricSpace α] {f : α → ENNReal} (C : ENNReal) (hC : C ≠ ⊤) (h : ∀ (x y : α), f x ≤ f y + C * edist x y) : Continuous f

theorem continuous_edist {α : Type u_1} [PseudoEMetricSpace α] : Continuous fun (p : α × α) => edist p.1 p.2

theorem Continuous.edist {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : Continuous fun (b : β) => EDist.edist (f b) (g b)

theorem Filter.Tendsto.edist {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] {f g : β → α} {x : Filter β} {a b : α} (hf : Tendsto f x (nhds a)) (hg : Tendsto g x (nhds b)) : Tendsto (fun (x : β) => EDist.edist (f x) (g x)) x (nhds (EDist.edist a b))

theorem EMetric.isClosed_closedBall {α : Type u_1} [PseudoEMetricSpace α] {a : α} {r : ENNReal} : IsClosed (closedBall a r)

@[simp]

theorem Metric.ediam_closure {α : Type u_1} [PseudoEMetricSpace α] (s : Set α) : ediam (closure s) = ediam s

@[deprecated Metric.ediam_closure (since := "2026-01-04")]

theorem EMetric.diam_closure {α : Type u_1} [PseudoEMetricSpace α] (s : Set α) : Metric.ediam (closure s) = Metric.ediam s

Alias of Metric.ediam_closure.

@[simp]

theorem Metric.diam_closure {α : Type u_4} [PseudoMetricSpace α] (s : Set α) : diam (closure s) = diam s

theorem isClosed_setOf_lipschitzOnWith {α : Type u_4} {β : Type u_5} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (s : Set α) : IsClosed {f : α → β | LipschitzOnWith K f s}

theorem isClosed_setOf_lipschitzWith {α : Type u_4} {β : Type u_5} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) : IsClosed {f : α → β | LipschitzWith K f}

theorem LipschitzOnWith.closure {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {s : Set α} {K : NNReal} (hcont : ContinuousOn f (closure s)) (hf : LipschitzOnWith K f s) : LipschitzOnWith K f (closure s)

theorem lipschitzOnWith_closure_iff {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {s : Set α} {K : NNReal} (hcont : ContinuousOn f (closure s)) : LipschitzOnWith K f (closure s) ↔ LipschitzOnWith K f s

theorem Real.ediam_eq {s : Set ℝ} (h : Bornology.IsBounded s) : Metric.ediam s = ENNReal.ofReal (sSup s - sInf s)

For a bounded set s : Set ℝ, its ediam is equal to sSup s - sInf s reinterpreted as ℝ≥0∞.

theorem Real.diam_eq {s : Set ℝ} (h : Bornology.IsBounded s) : Metric.diam s = sSup s - sInf s

For a bounded set s : Set ℝ, its Metric.diam is equal to sSup s - sInf s.

@[simp]

theorem Real.ediam_Ioo (a b : ℝ) : Metric.ediam (Set.Ioo a b) = ENNReal.ofReal (b - a)

@[simp]

theorem Real.ediam_Icc (a b : ℝ) : Metric.ediam (Set.Icc a b) = ENNReal.ofReal (b - a)

@[simp]

theorem Real.ediam_Ico (a b : ℝ) : Metric.ediam (Set.Ico a b) = ENNReal.ofReal (b - a)

@[simp]

theorem Real.ediam_Ioc (a b : ℝ) : Metric.ediam (Set.Ioc a b) = ENNReal.ofReal (b - a)

theorem Real.diam_Icc {a b : ℝ} (h : a ≤ b) : Metric.diam (Set.Icc a b) = b - a

theorem Real.diam_Ico {a b : ℝ} (h : a ≤ b) : Metric.diam (Set.Ico a b) = b - a

theorem Real.diam_Ioc {a b : ℝ} (h : a ≤ b) : Metric.diam (Set.Ioc a b) = b - a

theorem Real.diam_Ioo {a b : ℝ} (h : a ≤ b) : Metric.diam (Set.Ioo a b) = b - a

noncomputable def ENNReal.truncateToReal (t x : ENNReal) : ℝ

With truncation level t, the truncated cast ℝ≥0∞ → ℝ is given by x ↦ (min t x).toReal. Unlike ENNReal.toReal, this cast is continuous and monotone when t ≠ ∞.

Equations

• t.truncateToReal x = (min t x).toReal

theorem ENNReal.truncateToReal_eq_toReal {t x : ENNReal} (t_ne_top : t ≠ ⊤) (x_le : x ≤ t) : t.truncateToReal x = x.toReal

theorem ENNReal.truncateToReal_le {t : ENNReal} (t_ne_top : t ≠ ⊤) {x : ENNReal} : t.truncateToReal x ≤ t.toReal

theorem ENNReal.truncateToReal_nonneg {t x : ENNReal} : 0 ≤ t.truncateToReal x

theorem ENNReal.monotone_truncateToReal {t : ENNReal} (t_ne_top : t ≠ ⊤) : Monotone t.truncateToReal

The truncated cast ENNReal.truncateToReal t : ℝ≥0∞ → ℝ is monotone when t ≠ ∞.

theorem ENNReal.continuous_truncateToReal {t : ENNReal} (t_ne_top : t ≠ ⊤) : Continuous t.truncateToReal

The truncated cast ENNReal.truncateToReal t : ℝ≥0∞ → ℝ is continuous when t ≠ ∞.

theorem ENNReal.limsup_sub_const {ι : Type u_4} (F : Filter ι) (f : ι → ENNReal) (c : ENNReal) : Filter.limsup (fun (i : ι) => f i - c) F = Filter.limsup f F - c

theorem ENNReal.liminf_sub_const {ι : Type u_4} (F : Filter ι) [F.NeBot] (f : ι → ENNReal) (c : ENNReal) : Filter.liminf (fun (i : ι) => f i - c) F = Filter.liminf f F - c

theorem ENNReal.limsup_const_sub {ι : Type u_4} (F : Filter ι) (f : ι → ENNReal) {c : ENNReal} (c_ne_top : c ≠ ⊤) : Filter.limsup (fun (i : ι) => c - f i) F = c - Filter.liminf f F

theorem ENNReal.liminf_const_sub {ι : Type u_4} (F : Filter ι) [F.NeBot] (f : ι → ENNReal) {c : ENNReal} (c_ne_top : c ≠ ⊤) : Filter.liminf (fun (i : ι) => c - f i) F = c - Filter.limsup f F

theorem ENNReal.le_limsup_mul {ι : Type u_4} {f : Filter ι} {u v : ι → ENNReal} : Filter.limsup u f * Filter.liminf v f ≤ Filter.limsup (u * v) f

theorem ENNReal.limsup_mul_le' {ι : Type u_4} {f : Filter ι} {u v : ι → ENNReal} (h : Filter.limsup u f ≠ 0 ∨ Filter.limsup v f ≠ ⊤) (h' : Filter.limsup u f ≠ ⊤ ∨ Filter.limsup v f ≠ 0) : Filter.limsup (u * v) f ≤ Filter.limsup u f * Filter.limsup v f

See also ENNReal.limsup_mul_le.

theorem ENNReal.le_liminf_mul {ι : Type u_4} {f : Filter ι} {u v : ι → ENNReal} : Filter.liminf u f * Filter.liminf v f ≤ Filter.liminf (u * v) f

theorem ENNReal.liminf_mul_le {ι : Type u_4} {f : Filter ι} {u v : ι → ENNReal} (h : Filter.limsup u f ≠ 0 ∨ Filter.liminf v f ≠ ⊤) (h' : Filter.limsup u f ≠ ⊤ ∨ Filter.liminf v f ≠ 0) : Filter.liminf (u * v) f ≤ Filter.limsup u f * Filter.liminf v f

theorem ENNReal.liminf_toReal_eq {ι : Type u_4} {f : Filter ι} {u : ι → ENNReal} [f.NeBot] {b : ENNReal} (b_ne_top : b ≠ ⊤) (le_b : ∀ᶠ (i : ι) in f, u i ≤ b) : Filter.liminf (fun (i : ι) => (u i).toReal) f = (Filter.liminf u f).toReal

If u : ι → ℝ≥0∞ is bounded, then we have liminf (toReal ∘ u) = toReal (liminf u).

theorem ENNReal.limsup_toReal_eq {ι : Type u_4} {f : Filter ι} {u : ι → ENNReal} [f.NeBot] {b : ENNReal} (b_ne_top : b ≠ ⊤) (le_b : ∀ᶠ (i : ι) in f, u i ≤ b) : Filter.limsup (fun (i : ι) => (u i).toReal) f = (Filter.limsup u f).toReal

If u : ι → ℝ≥0∞ is bounded, then we have liminf (toReal ∘ u) = toReal (liminf u).

@[simp]

theorem ENNReal.ofNNReal_limsup {ι : Type u_4} {f : Filter ι} {u : ι → NNReal} (hf : Filter.IsBoundedUnder (fun (x1 x2 : NNReal) => x1 ≤ x2) f u) : ↑(Filter.limsup u f) = Filter.limsup (fun (i : ι) => ↑(u i)) f

@[simp]

theorem ENNReal.ofNNReal_liminf {ι : Type u_4} {f : Filter ι} {u : ι → NNReal} (hf : Filter.IsCoboundedUnder (fun (x1 x2 : NNReal) => x1 ≥ x2) f u) : ↑(Filter.liminf u f) = Filter.liminf (fun (i : ι) => ↑(u i)) f

theorem ENNReal.liminf_add_of_right_tendsto_zero {ι : Type u_4} {u : Filter ι} {g : ι → ENNReal} (hg : Filter.Tendsto g u (nhds 0)) (f : ι → ENNReal) : Filter.liminf (f + g) u = Filter.liminf f u

theorem ENNReal.liminf_add_of_left_tendsto_zero {ι : Type u_4} {u : Filter ι} {f : ι → ENNReal} (hf : Filter.Tendsto f u (nhds 0)) (g : ι → ENNReal) : Filter.liminf (f + g) u = Filter.liminf g u

theorem ENNReal.limsup_add_of_right_tendsto_zero {ι : Type u_4} {u : Filter ι} {g : ι → ENNReal} (hg : Filter.Tendsto g u (nhds 0)) (f : ι → ENNReal) : Filter.limsup (f + g) u = Filter.limsup f u

theorem ENNReal.limsup_add_of_left_tendsto_zero {ι : Type u_4} {u : Filter ι} {f : ι → ENNReal} (hf : Filter.Tendsto f u (nhds 0)) (g : ι → ENNReal) : Filter.limsup (f + g) u = Filter.limsup g u

theorem Dense.lipschitzWith_extend {α : Type u_4} {β : Type u_5} [PseudoEMetricSpace α] [EMetricSpace β] [CompleteSpace β] {s : Set α} (hs : Dense s) {f : ↑s → β} {K : NNReal} (hf : LipschitzWith K f) : LipschitzWith K (hs.extend f)