Loogle!

Result

Found 203 declarations mentioning WeakPseudoEMetricSpace. Of these, only the first 200 are shown.

• WeakPseudoEMetricSpace 📋 Mathlib.Topology.EMetricSpace.Defs
  (α : Type u) [τ : TopologicalSpace α] : Type u
• Metric.edistLtTopSetoid 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] : Setoid α
• WeakPseudoEMetricSpace.toEDist 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {τ : TopologicalSpace α} [self : WeakPseudoEMetricSpace α] : EDist α
• WeakEMetricSpace.toWeakPseudoEMetricSpace 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {inst✝ : TopologicalSpace α} [self : WeakEMetricSpace α] : WeakPseudoEMetricSpace α
• PseudoEMetricSpace.toWeakPseudoEMetricSpace 📋 Mathlib.Topology.EMetricSpace.Defs
  (α : Type u) [inst : PseudoEMetricSpace α] : WeakPseudoEMetricSpace α
• instWeakPseudoEMetricSpaceOrderDual 📋 Mathlib.Topology.EMetricSpace.Defs
  {X : Type u_1} [TopologicalSpace X] [WeakPseudoEMetricSpace X] : WeakPseudoEMetricSpace Xᵒᵈ
• instWeakPseudoEMetricSpaceSubtype 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} {p : α → Prop} [TopologicalSpace α] [WeakPseudoEMetricSpace α] : WeakPseudoEMetricSpace (Subtype p)
• WeakPseudoEMetricSpace.IsInducing 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} {β : Type u_3} [e : TopologicalSpace α] [n : TopologicalSpace β] {f : α → β} (hf : Topology.IsInducing f) (m : WeakPseudoEMetricSpace β) : WeakPseudoEMetricSpace α
• Metric.mem_closedEBall_self 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x : α} {ε : ENNReal} : x ∈ Metric.closedEBall x ε
• WeakPseudoEMetricSpace.edist_self 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {τ : TopologicalSpace α} [self : WeakPseudoEMetricSpace α] (x : α) : edist x x = 0
• WeakPseudoEMetricSpace.edist_comm 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {τ : TopologicalSpace α} [self : WeakPseudoEMetricSpace α] (x y : α) : edist x y = edist y x
• WeakPseudoEMetricSpace.ext 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [TopologicalSpace α] {m m' : WeakPseudoEMetricSpace α} (h : m.toEDist = m'.toEDist) : m = m'
• WeakPseudoEMetricSpace.ext_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_2} [TopologicalSpace α] {m m' : WeakPseudoEMetricSpace α} : m = m' ↔ m.toEDist = m'.toEDist
• Metric.ordConnected_setOfPred_closedEBall_subset 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x : α) (s : Set α) : {r | Metric.closedEBall x r ⊆ s}.OrdConnected
• Metric.ordConnected_setOfPred_eball_subset 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x : α) (s : Set α) : {r | Metric.eball x r ⊆ s}.OrdConnected
• Metric.ordConnected_setOf_closedEBall_subset 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x : α) (s : Set α) : {r | Metric.closedEBall x r ⊆ s}.OrdConnected
• Metric.ordConnected_setOf_eball_subset 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x : α) (s : Set α) : {r | Metric.eball x r ⊆ s}.OrdConnected
• WeakEMetricSpace.mk 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [TopologicalSpace α] [toWeakPseudoEMetricSpace : WeakPseudoEMetricSpace α] (eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y) : WeakEMetricSpace α
• Metric.eball_eq_empty_iff 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x : α} {ε : ENNReal} : Metric.eball x ε = ∅ ↔ ε = 0
• Metric.mem_closedEBall' 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε : ENNReal} : y ∈ Metric.closedEBall x ε ↔ edist x y ≤ ε
• Metric.mem_eball_self 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x : α} {ε : ENNReal} (h : 0 < ε) : x ∈ Metric.eball x ε
• Metric.mem_closedEBall_comm 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε : ENNReal} : x ∈ Metric.closedEBall y ε ↔ y ∈ Metric.closedEBall x ε
• Metric.mem_eball_comm 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε : ENNReal} : x ∈ Metric.eball y ε ↔ y ∈ Metric.eball x ε
• WeakPseudoEMetricSpace.topology_le 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {τ : TopologicalSpace α} [self : WeakPseudoEMetricSpace α] : (uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace ≤ τ
• Metric.mem_eball' 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε : ENNReal} : y ∈ Metric.eball x ε ↔ edist x y < ε
• edist_congr_left 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y z : α} (h : edist x y = 0) : edist z x = edist z y
• edist_congr_right 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y z : α} (h : edist x y = 0) : edist x z = edist y z
• edist_triangle_left 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y z : α) : edist x y ≤ edist z x + edist z y
• edist_triangle_right 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y z : α) : edist x y ≤ edist x z + edist y z
• WeakPseudoEMetricSpace.edist_triangle 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {τ : TopologicalSpace α} [self : WeakPseudoEMetricSpace α] (x y z : α) : edist x z ≤ edist x y + edist y z
• Subtype.edist_eq 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {p : α → Prop} (x y : Subtype p) : edist x y = edist ↑x ↑y
• Subtype.edist_mk_mk 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {p : α → Prop} {x y : α} (hx : p x) (hy : p y) : edist ⟨x, hx⟩ ⟨y, hy⟩ = edist x y
• edist_triangle4 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y z t : α) : edist x t ≤ edist x y + edist y z + edist z t
• edist_congr 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {w x y z : α} (hl : edist w x = 0) (hr : edist y z = 0) : edist w y = edist x z
• Metric.exists_eball_subset_eball 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε : ENNReal} (h : y ∈ Metric.eball x ε) : ∃ ε' > 0, Metric.eball y ε' ⊆ Metric.eball x ε
• Metric.eball_subset 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε₁ ε₂ : ENNReal} (h : edist x y + ε₁ ≤ ε₂) (h' : edist x y ≠ ⊤) : Metric.eball x ε₁ ⊆ Metric.eball y ε₂
• WeakPseudoEMetricSpace.topology_eq_on_restrict 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} {τ : TopologicalSpace α} [self : WeakPseudoEMetricSpace α] (x : α) (r : ENNReal) : IsOpen (Subtype.val ⁻¹' Metric.eball x r)
• Metric.eball_disjoint 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u_3} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {x y : α} {ε₁ ε₂ : ENNReal} (h : ε₁ + ε₂ ≤ edist x y) : Disjoint (Metric.eball x ε₁) (Metric.eball y ε₂)
• WeakPseudoEMetricSpace.mk 📋 Mathlib.Topology.EMetricSpace.Defs
  {α : Type u} [τ : TopologicalSpace α] [toEDist : EDist α] (edist_self : ∀ (x : α), edist x x = 0) (edist_comm : ∀ (x y : α), edist x y = edist y x) (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) (topology_le : (uniformSpaceOfEDist edist edist_self edist_comm edist_triangle).toTopologicalSpace ≤ τ) (topology_eq_on_restrict : ∀ (x : α) (r : ENNReal), IsOpen (Subtype.val ⁻¹' Metric.eball x r)) : WeakPseudoEMetricSpace α
• edist_le_range_sum_edist 📋 Mathlib.Topology.EMetricSpace.Basic
  {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (f : ℕ → α) (n : ℕ) : edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, edist (f i) (f (i + 1))
• edist_le_Ico_sum_edist 📋 Mathlib.Topology.EMetricSpace.Basic
  {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (f : ℕ → α) {m n : ℕ} (h : m ≤ n) : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
• edist_le_range_sum_of_edist_le 📋 Mathlib.Topology.EMetricSpace.Basic
  {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {f : ℕ → α} (n : ℕ) {d : ℕ → ENNReal} (hd : ∀ {k : ℕ}, k < n → edist (f k) (f (k + 1)) ≤ d k) : edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i
• edist_le_Ico_sum_of_edist_le 📋 Mathlib.Topology.EMetricSpace.Basic
  {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] {f : ℕ → α} {m n : ℕ} (hmn : m ≤ n) {d : ℕ → ENNReal} (hd : ∀ {k : ℕ}, m ≤ k → k < n → edist (f k) (f (k + 1)) ≤ d k) : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, d i
• EMetric.subset_countable_closure_of_almost_dense_set 📋 Mathlib.Topology.EMetricSpace.Basic
  {α : Type u} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (s : Set α) (hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, Metric.closedEBall x ε) : ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
• edist_pi_const_le 📋 Mathlib.Topology.EMetricSpace.Pi
  {α : Type u} {β : Type v} [TopologicalSpace α] [WeakPseudoEMetricSpace α] [Fintype β] (a b : α) : (edist (fun x => a) fun x => b) ≤ edist a b
• edist_pi_const 📋 Mathlib.Topology.EMetricSpace.Pi
  {α : Type u} {β : Type v} [TopologicalSpace α] [WeakPseudoEMetricSpace α] [Fintype β] [Nonempty β] (a b : α) : (edist (fun x => a) fun x => b) = edist a b
• Metric.ediam_empty 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} [TopologicalSpace X] [WeakPseudoEMetricSpace X] : Metric.ediam ∅ = 0
• Metric.ediam_subsingleton 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {s : Set X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] (hs : s.Subsingleton) : Metric.ediam s = 0
• Set.Subsingleton.ediam_eq 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {s : Set X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] (hs : s.Subsingleton) : Metric.ediam s = 0
• Metric.ediam_singleton 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {x : X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] : Metric.ediam {x} = 0
• Metric.ediam_one 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} [TopologicalSpace X] [WeakPseudoEMetricSpace X] [One X] : Metric.ediam 1 = 0
• Metric.ediam_zero 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} [TopologicalSpace X] [WeakPseudoEMetricSpace X] [Zero X] : Metric.ediam 0 = 0
• Metric.ediam_mono 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {s t : Set X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] (h : s ⊆ t) : Metric.ediam s ≤ Metric.ediam t
• Metric.ediam_pair 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {x y : X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] : Metric.ediam {x, y} = edist x y
• Metric.ediam_eq_sSup 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} [TopologicalSpace X] [WeakPseudoEMetricSpace X] (s : Set X) : Metric.ediam s = sSup (Set.image2 edist s s)
• Metric.edist_le_ediam_of_mem 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {s : Set X} {x y : X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] (hx : x ∈ s) (hy : y ∈ s) : edist x y ≤ Metric.ediam s
• Metric.ediam_le 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {s : Set X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {d : ENNReal} (h : ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d) : Metric.ediam s ≤ d
• Metric.edist_le_of_ediam_le 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {s : Set X} {x y : X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {d : ENNReal} (hx : x ∈ s) (hy : y ∈ s) (hd : Metric.ediam s ≤ d) : edist x y ≤ d
• Metric.ediam_le_iff 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {s : Set X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {d : ENNReal} : Metric.ediam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d
• Metric.ediam_union_le 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {s t : Set X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] (h : (s ∩ t).Nonempty) : Metric.ediam (s ∪ t) ≤ Metric.ediam s + Metric.ediam t
• Metric.ediam_image_le_iff 📋 Mathlib.Topology.EMetricSpace.Diam
  {α : Type u_1} {X : Type u_2} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {d : ENNReal} {f : α → X} {s : Set α} : Metric.ediam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d
• Metric.ediam_closedEBall_le 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {x : X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {r : ENNReal} : Metric.ediam (Metric.closedEBall x r) ≤ 2 * r
• Metric.ediam_eball_le 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {x : X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {r : ENNReal} : Metric.ediam (Metric.eball x r) ≤ 2 * r
• Metric.ediam_triple 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {x y z : X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] : Metric.ediam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)
• Metric.ediam_union_le_add_edist 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {s t : Set X} {x y : X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] (xs : x ∈ s) (yt : y ∈ t) : Metric.ediam (s ∪ t) ≤ Metric.ediam s + edist x y + Metric.ediam t
• Metric.ediam_insert 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} {s : Set X} {x : X} [TopologicalSpace X] [WeakPseudoEMetricSpace X] : Metric.ediam (insert x s) = max (⨆ y ∈ s, edist x y) (Metric.ediam s)
• Metric.ediam_iUnion_mem_option 📋 Mathlib.Topology.EMetricSpace.Diam
  {X : Type u_2} [TopologicalSpace X] [WeakPseudoEMetricSpace X] {ι : Type u_3} (o : Option ι) (s : ι → Set X) : Metric.ediam (⋃ i ∈ o, s i) = ⨆ i ∈ o, Metric.ediam (s i)
• AddOpposite.instWeakPseudoEMetricSpace 📋 Mathlib.Topology.EMetricSpace.MulOpposite
  {α : Type u_2} [TopologicalSpace α] [WeakPseudoEMetricSpace α] : WeakPseudoEMetricSpace αᵃᵒᵖ
• MulOpposite.instWeakPseudoEMetricSpace 📋 Mathlib.Topology.EMetricSpace.MulOpposite
  {α : Type u_2} [TopologicalSpace α] [WeakPseudoEMetricSpace α] : WeakPseudoEMetricSpace αᵐᵒᵖ
• AddOpposite.edist_op 📋 Mathlib.Topology.EMetricSpace.MulOpposite
  {α : Type u_1} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y : α) : edist (AddOpposite.op x) (AddOpposite.op y) = edist x y
• MulOpposite.edist_op 📋 Mathlib.Topology.EMetricSpace.MulOpposite
  {α : Type u_1} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y : α) : edist (MulOpposite.op x) (MulOpposite.op y) = edist x y
• AddOpposite.edist_unop 📋 Mathlib.Topology.EMetricSpace.MulOpposite
  {α : Type u_1} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y : αᵃᵒᵖ) : edist (AddOpposite.unop x) (AddOpposite.unop y) = edist x y
• MulOpposite.edist_unop 📋 Mathlib.Topology.EMetricSpace.MulOpposite
  {α : Type u_1} [TopologicalSpace α] [WeakPseudoEMetricSpace α] (x y : αᵐᵒᵖ) : edist (MulOpposite.unop x) (MulOpposite.unop y) = edist x y
• BoundedVariationOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) : Prop
• LocallyBoundedVariationOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) : Prop
• eVariationOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) : ENNReal
• BoundedVariationOn.of_subsingleton 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hs : s.Subsingleton) : BoundedVariationOn f s
• BoundedVariationOn.locallyBoundedVariationOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (h : BoundedVariationOn f s) : LocallyBoundedVariationOn f s
• eVariationOn.subsingleton 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {s : Set α} (hs : s.Subsingleton) : eVariationOn f s = 0
• eVariationOn.constant_on 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : (f '' s).Subsingleton) : eVariationOn f s = 0
• BoundedVariationOn.mono 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (h : BoundedVariationOn f s) {t : Set α} (ht : t ⊆ s) : BoundedVariationOn f t
• eVariationOn.congr 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f g : α → E} {s : Set α} (h : Set.EqOn f g s) : eVariationOn f s = eVariationOn g s
• eVariationOn.eq_of_eqOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f f' : α → E} {s : Set α} (h : Set.EqOn f f' s) : eVariationOn f s = eVariationOn f' s
• eVariationOn.mono 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {s t : Set α} (hst : t ⊆ s) : eVariationOn f t ≤ eVariationOn f s
• eVariationOn.pair 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (a b : α) : eVariationOn f {a, b} = edist (f a) (f b)
• eVariationOn.edist_le 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {s : Set α} {x y : α} (hx : x ∈ s) (hy : y ∈ s) : edist (f x) (f y) ≤ eVariationOn f s
• eVariationOn.eq_of_edist_zero_on 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f f' : α → E} {s : Set α} (h : ∀ ⦃x : α⦄, x ∈ s → edist (f x) (f' x) = 0) : eVariationOn f s = eVariationOn f' s
• eVariationOn.eq_zero_iff 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {s : Set α} : eVariationOn f s = 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
• eVariationOn.comp_eq_of_antitoneOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {β : Type u_4} [LinearOrder β] (f : α → E) {t : Set β} (φ : β → α) (hφ : AntitoneOn φ t) : eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t)
• eVariationOn.comp_eq_of_monotoneOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {β : Type u_4} [LinearOrder β] (f : α → E) {t : Set β} (φ : β → α) (hφ : MonotoneOn φ t) : eVariationOn (f ∘ φ) t = eVariationOn f (φ '' t)
• eVariationOn.comp_le_of_antitoneOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {β : Type u_4} [LinearOrder β] (f : α → E) {s : Set α} {t : Set β} (φ : β → α) (hφ : AntitoneOn φ t) (φst : Set.MapsTo φ t s) : eVariationOn (f ∘ φ) t ≤ eVariationOn f s
• eVariationOn.comp_le_of_monotoneOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {β : Type u_4} [LinearOrder β] (f : α → E) {s : Set α} {t : Set β} (φ : β → α) (hφ : MonotoneOn φ t) (φst : Set.MapsTo φ t s) : eVariationOn (f ∘ φ) t ≤ eVariationOn f s
• eVariationOn.image_range_of_monotone 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {u : ℕ → α} (hu : Monotone u) (n : ℕ) : eVariationOn f (u '' Set.Iic n) = ∑ i ∈ Finset.range n, edist (f (u i)) (f (u (i + 1)))
• BoundedVariationOn.tendsto_eVariationOn_Ici_zero 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) : Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Ici y)) (Filter.principal s ⊓ Filter.atTop) (nhds 0)
• BoundedVariationOn.tendsto_eVariationOn_Iic_zero 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) : Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Iic y)) (Filter.principal s ⊓ Filter.atBot) (nhds 0)
• BoundedVariationOn.tendsto_eVariationOn_Ico_zero 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) (x : α) : Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Ico y x)) (nhdsWithin x s) (nhds 0)
• BoundedVariationOn.tendsto_eVariationOn_Ioc_zero 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] [TopologicalSpace α] [OrderTopology α] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) (x : α) : Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Ioc x y)) (nhdsWithin x s) (nhds 0)
• eVariationOn.sum_le 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} {n : ℕ} {u : ℕ → α} (hu : Monotone u) (us : ∀ (i : ℕ), u i ∈ s) : ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
• BoundedVariationOn.ofDual 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) : BoundedVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s)
• LocallyBoundedVariationOn.ofDual 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) : LocallyBoundedVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s)
• eVariationOn.union 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {s t : Set α} {x : α} (hs : IsGreatest s x) (ht : IsLeast t x) : eVariationOn f (s ∪ t) = eVariationOn f s + eVariationOn f t
• eVariationOn.add_le_union 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {s t : Set α} (h : ∀ x ∈ s, ∀ y ∈ t, x ≤ y) : eVariationOn f s + eVariationOn f t ≤ eVariationOn f (s ∪ t)
• eVariationOn.boundedVariation_ofDual 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} : BoundedVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s) ↔ BoundedVariationOn f s
• eVariationOn.locallyBoundedVariation_ofDual 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} : LocallyBoundedVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s) ↔ LocallyBoundedVariationOn f s
• eVariationOn.comp_ofDual 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) : eVariationOn (f ∘ ⇑OrderDual.ofDual) (⇑OrderDual.ofDual ⁻¹' s) = eVariationOn f s
• eVariationOn.sum_le_of_monotoneOn_Iic 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} {n : ℕ} {u : ℕ → α} (hu : MonotoneOn u (Set.Iic n)) (us : ∀ i ≤ n, u i ∈ s) : ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
• BoundedVariationOn.tendsto_eVariationOn_Ici_zero_of_filter 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) (L : Filter α) (hL : ∀ y ∈ s, s ∩ Set.Ici y ∈ L) : Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Ici y)) L (nhds 0)
• eVariationOn.sum' 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {I : ℕ → α} (hI : Monotone I) {n : ℕ} : ∑ i ∈ Finset.range n, eVariationOn f (Set.Icc (I i) (I (i + 1))) = eVariationOn f (Set.Icc (I 0) (I n))
• eVariationOn.sum_le_of_monotoneOn_Icc 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} {m n : ℕ} {u : ℕ → α} (hu : MonotoneOn u (Set.Icc m n)) (us : ∀ i ∈ Set.Icc m n, u i ∈ s) : ∑ i ∈ Finset.Ico m n, edist (f (u (i + 1))) (f (u i)) ≤ eVariationOn f s
• eVariationOn.exists_lt_eVariationOn_inter_Icc 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {ε : ENNReal} {s : Set α} (h : ε < eVariationOn f s) : ∃ a ∈ s, ∃ b ∈ s, a < b ∧ ε < eVariationOn f (s ∩ Set.Icc a b)
• eVariationOn.union' 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {s t : Set α} {x y : α} (hs : IsGreatest s x) (ht : IsLeast t y) (hxy : x ≤ y) : eVariationOn f (s ∪ t) = eVariationOn f s + edist (f x) (f y) + eVariationOn f t
• eVariationOn.comp_inter_Icc_eq_of_monotoneOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {β : Type u_4} [LinearOrder β] (f : α → E) {t : Set β} (φ : β → α) (hφ : MonotoneOn φ t) {x y : β} (hx : x ∈ t) (hy : y ∈ t) : eVariationOn (f ∘ φ) (t ∩ Set.Icc x y) = eVariationOn f (φ '' t ∩ Set.Icc (φ x) (φ y))
• eVariationOn.sum 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {s : Set α} {E✝ : ℕ → α} (hE : Monotone E✝) {n : ℕ} (hn : ∀ (i : ℕ), 0 < i → i < n → E✝ i ∈ s) : ∑ i ∈ Finset.range n, eVariationOn f (s ∩ Set.Icc (E✝ i) (E✝ (i + 1))) = eVariationOn f (s ∩ Set.Icc (E✝ 0) (E✝ n))
• eVariationOn.Icc_add_Icc 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {s : Set α} {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) (hb : b ∈ s) : eVariationOn f (s ∩ Set.Icc a b) + eVariationOn f (s ∩ Set.Icc b c) = eVariationOn f (s ∩ Set.Icc a c)
• eVariationOn.add_point 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {s : Set α} {x : α} (hx : x ∈ s) (u : ℕ → α) (hu : Monotone u) (us : ∀ (i : ℕ), u i ∈ s) (n : ℕ) : ∃ v m, Monotone v ∧ (∀ (i : ℕ), v i ∈ s) ∧ x ∈ v '' Set.Iio m ∧ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))
• eVariationOn.eq_biSup_inter_Icc 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} : eVariationOn f s = ⨆ p ∈ {p | p.1 ∈ s ∧ p.2 ∈ s ∧ p.1 ≤ p.2}, eVariationOn f (s ∩ Set.Icc p.1 p.2)
• eVariationOn.eVariationOn_eq_strictMonoOn 📋 Mathlib.Topology.EMetricSpace.BoundedVariation
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) : eVariationOn f s = ⨆ p, ∑ i ∈ Finset.range p.fst, edist (f (↑p.snd (i + 1))) (f (↑p.snd i))
• variationOnFromTo 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) (a b : α) : ℝ
• variationOnFromTo.self 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) (a : α) : variationOnFromTo f s a a = 0
• variationOnFromTo.eq_neg_swap 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) (a b : α) : variationOnFromTo f s a b = -variationOnFromTo f s b a
• variationOnFromTo.abs_le_eVariationOn 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : BoundedVariationOn f s) {a b : α} : |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal
• variationOnFromTo.nonneg_of_le 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) {a b : α} (h : a ≤ b) : 0 ≤ variationOnFromTo f s a b
• variationOnFromTo.nonpos_of_ge 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) {a b : α} (h : b ≤ a) : variationOnFromTo f s a b ≤ 0
• variationOnFromTo.monotoneOn 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (as : a ∈ s) : MonotoneOn (variationOnFromTo f s a) s
• variationOnFromTo.antitoneOn 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {b : α} (bs : b ∈ s) : AntitoneOn (fun a => variationOnFromTo f s a b) s
• variationOnFromTo.eq_of_le 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) {a b : α} (h : a ≤ b) : variationOnFromTo f s a b = (eVariationOn f (s ∩ Set.Icc a b)).toReal
• variationOnFromTo.edist_zero_of_eq_zero 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : variationOnFromTo f s a b = 0) : edist (f a) (f b) = 0
• variationOnFromTo.eq_of_ge 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) {a b : α} (h : b ≤ a) : variationOnFromTo f s a b = -(eVariationOn f (s ∩ Set.Icc b a)).toReal
• variationOnFromTo.add 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hc : c ∈ s) : variationOnFromTo f s a b + variationOnFromTo f s b c = variationOnFromTo f s a c
• variationOnFromTo.sub_left 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hc : c ∈ s) : variationOnFromTo f s a b - variationOnFromTo f s c b = variationOnFromTo f s a c
• variationOnFromTo.sub_right 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hc : c ∈ s) : variationOnFromTo f s a b - variationOnFromTo f s a c = variationOnFromTo f s c b
• variationOnFromTo.eq_left_iff 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hc : c ∈ s) : variationOnFromTo f s a b = variationOnFromTo f s a c ↔ variationOnFromTo f s b c = 0
• variationOnFromTo.comp_eq_of_monotoneOn 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {β : Type u_4} [LinearOrder β] (f : α → E) {t : Set β} (φ : β → α) (hφ : MonotoneOn φ t) {x y : β} (hx : x ∈ t) (hy : y ∈ t) : variationOnFromTo (f ∘ φ) t x y = variationOnFromTo f (φ '' t) (φ x) (φ y)
• variationOnFromTo.eq_zero_iff 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Set.uIcc a b → ∀ ⦃y : α⦄, y ∈ s ∩ Set.uIcc a b → edist (f x) (f y) = 0
• variationOnFromTo.eq_zero_iff_of_ge 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (ba : b ≤ a) : variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Set.Icc b a → ∀ ⦃y : α⦄, y ∈ s ∩ Set.Icc b a → edist (f x) (f y) = 0
• variationOnFromTo.eq_zero_iff_of_le 📋 Mathlib.Topology.EMetricSpace.VariationOnFromTo
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (ab : a ≤ b) : variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Set.Icc a b → ∀ ⦃y : α⦄, y ∈ s ∩ Set.Icc a b → edist (f x) (f y) = 0
• HasUnitSpeedOn 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : ℝ → E) (s : Set ℝ) : Prop
• HasConstantSpeedOnWith 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : ℝ → E) (s : Set ℝ) (l : NNReal) : Prop
• naturalParameterization 📋 Mathlib.Analysis.ConstantSpeed
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) (s : Set α) (a : α) : ℝ → E
• hasConstantSpeedOnWith_of_subsingleton 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : ℝ → E) {s : Set ℝ} (hs : s.Subsingleton) (l : NNReal) : HasConstantSpeedOnWith f s l
• HasConstantSpeedOnWith.hasLocallyBoundedVariationOn 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal} (h : HasConstantSpeedOnWith f s l) : LocallyBoundedVariationOn f s
• HasUnitSpeedOn.Icc_Icc 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : ℝ → E} {x y z : ℝ} (hfs : HasUnitSpeedOn f (Set.Icc x y)) (hft : HasUnitSpeedOn f (Set.Icc y z)) : HasUnitSpeedOn f (Set.Icc x z)
• HasConstantSpeedOnWith.Icc_Icc 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : ℝ → E} {l : NNReal} {x y z : ℝ} (hfs : HasConstantSpeedOnWith f (Set.Icc x y) l) (hft : HasConstantSpeedOnWith f (Set.Icc y z) l) : HasConstantSpeedOnWith f (Set.Icc x z) l
• HasUnitSpeedOn.union 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : ℝ → E} {s t : Set ℝ} {x : ℝ} (hfs : HasUnitSpeedOn f s) (hft : HasUnitSpeedOn f t) (hs : IsGreatest s x) (ht : IsLeast t x) : HasUnitSpeedOn f (s ∪ t)
• HasConstantSpeedOnWith.union 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal} {t : Set ℝ} (hfs : HasConstantSpeedOnWith f s l) (hft : HasConstantSpeedOnWith f t l) {x : ℝ} (hs : IsGreatest s x) (ht : IsLeast t x) : HasConstantSpeedOnWith f (s ∪ t) l
• has_unit_speed_naturalParameterization 📋 Mathlib.Analysis.ConstantSpeed
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (f : α → E) {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (as : a ∈ s) : HasUnitSpeedOn (naturalParameterization f s a) (variationOnFromTo f s a '' s)
• hasConstantSpeedOnWith_zero_iff 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} : HasConstantSpeedOnWith f s 0 ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
• unique_unit_speed 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {φ : ℝ → ℝ} (φm : MonotoneOn φ s) (hfφ : HasUnitSpeedOn (f ∘ φ) s) (hf : HasUnitSpeedOn f (φ '' s)) ⦃x : ℝ⦄ (xs : x ∈ s) : Set.EqOn φ (fun y => y - x + φ x) s
• edist_naturalParameterization_eq_zero 📋 Mathlib.Analysis.ConstantSpeed
  {α : Type u_1} [LinearOrder α] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : α → E} {s : Set α} (hf : LocallyBoundedVariationOn f s) {a : α} (as : a ∈ s) {b : α} (bs : b ∈ s) : edist (naturalParameterization f s a (variationOnFromTo f s a b)) (f b) = 0
• hasConstantSpeedOnWith_iff_variationOnFromTo_eq 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal} : HasConstantSpeedOnWith f s l ↔ LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)
• hasConstantSpeedOnWith_iff_ordered 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l : NNReal} : HasConstantSpeedOnWith f s l ↔ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Set.Icc x y) = ENNReal.ofReal (↑l * (y - x))
• HasConstantSpeedOnWith.ratio 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : ℝ → E} {s : Set ℝ} {l l' : NNReal} (hl' : l' ≠ 0) {φ : ℝ → ℝ} (φm : MonotoneOn φ s) (hfφ : HasConstantSpeedOnWith (f ∘ φ) s l) (hf : HasConstantSpeedOnWith f (φ '' s) l') ⦃x : ℝ⦄ (xs : x ∈ s) : Set.EqOn φ (fun y => ↑l / ↑l' * (y - x) + φ x) s
• unique_unit_speed_on_Icc_zero 📋 Mathlib.Analysis.ConstantSpeed
  {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] {f : ℝ → E} {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) {φ : ℝ → ℝ} (φm : MonotoneOn φ (Set.Icc 0 s)) (φst : φ '' Set.Icc 0 s = Set.Icc 0 t) (hfφ : HasUnitSpeedOn (f ∘ φ) (Set.Icc 0 s)) (hf : HasUnitSpeedOn f (Set.Icc 0 t)) : Set.EqOn φ id (Set.Icc 0 s)
• PairReduction.logSizeBallStruct.ball 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] (struct : PairReduction.logSizeBallStruct T) (c : ENNReal) : Finset T
• PairReduction.logSizeBallStruct.smallBall 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] (struct : PairReduction.logSizeBallStruct T) (c : ENNReal) : Finset T
• PairReduction.logSizeRadius 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] (t : T) (V : Finset T) (a c : ENNReal) : ℕ
• PairReduction.pairSet 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] [DecidableEq T] (J : Finset T) (a c : ENNReal) : Finset (T × T)
• PairReduction.pairSetSeq 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] [DecidableEq T] (J : Finset T) (a c : ENNReal) (n : ℕ) : Finset (T × T)
• PairReduction.logSizeBallSeq 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] [DecidableEq T] (J : Finset T) (hJ : J.Nonempty) (a c : ENNReal) : ℕ → PairReduction.logSizeBallStruct T
• PairReduction.finset_logSizeBallSeq_zero 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) : (PairReduction.logSizeBallSeq J hJ a c 0).finset = J
• PairReduction.pairSet_empty_eq_empty 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] [DecidableEq T] (a c : ENNReal) : PairReduction.pairSet ∅ a c = ∅
• PairReduction.antitone_logSizeBallSeq_add_one_subset 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) : Antitone fun i => (PairReduction.logSizeBallSeq J hJ a c i).finset
• PairReduction.card_finset_logSizeBallSeq_card_eq_zero 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) : (PairReduction.logSizeBallSeq J hJ a c J.card).finset.card = 0
• PairReduction.point_mem_logSizeBallSeq_init 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (i : ℕ) : (PairReduction.logSizeBallSeq J hJ a c i).point ∈ J
• PairReduction.finset_logSizeBallSeq_subset_logSizeBallSeq_init 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (i : ℕ) : (PairReduction.logSizeBallSeq J hJ a c i).finset ⊆ J
• PairReduction.one_le_logSizeRadius 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {V : Finset T} {t : T} (ha : 1 < a) : 1 ≤ PairReduction.logSizeRadius t V a c
• PairReduction.card_finset_logSizeBallSeq_le 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (i : ℕ) : (PairReduction.logSizeBallSeq J hJ a c i).finset.card ≤ J.card - i
• PairReduction.point_logSizeBallSeq_zero 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) : (PairReduction.logSizeBallSeq J hJ a c 0).point = Exists.choose hJ
• PairReduction.one_le_radius_logSizeBallSeq 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (ha : 1 < a) (i : ℕ) : 1 ≤ (PairReduction.logSizeBallSeq J hJ a c i).radius
• PairReduction.pairSet_subset 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] : PairReduction.pairSet J a c ⊆ J ×ˢ J
• PairReduction.radius_logSizeBallSeq_zero 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) : (PairReduction.logSizeBallSeq J hJ a c 0).radius = PairReduction.logSizeRadius (Exists.choose hJ) J a c
• PairReduction.disjoint_smallBall_logSizeBallSeq 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) {i j : ℕ} (hij : i ≠ j) : Disjoint ((PairReduction.logSizeBallSeq J hJ a c i).smallBall c) ((PairReduction.logSizeBallSeq J hJ a c j).smallBall c)
• PairReduction.finset_logSizeBallSeq_add_one_subset 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (i : ℕ) : (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset ⊆ (PairReduction.logSizeBallSeq J hJ a c i).finset
• PairReduction.point_notMem_finset_logSizeBallSeq_add_one 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (i : ℕ) : (PairReduction.logSizeBallSeq J hJ a c i).point ∉ (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset
• PairReduction.point_mem_finset_logSizeBallSeq 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (i : ℕ) (h : (PairReduction.logSizeBallSeq J hJ a c i).finset.Nonempty) : (PairReduction.logSizeBallSeq J hJ a c i).point ∈ (PairReduction.logSizeBallSeq J hJ a c i).finset
• PairReduction.card_pairSet_le 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (ha : 1 < a) : ↑(PairReduction.pairSet J a c).card ≤ a * ↑J.card
• PairReduction.card_finset_logSizeBallSeq_add_one_lt 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (i : ℕ) (h : (PairReduction.logSizeBallSeq J hJ a c i).finset.Nonempty) : (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset.card < (PairReduction.logSizeBallSeq J hJ a c i).finset.card
• PairReduction.finset_logSizeBallSeq_add_one 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (i : ℕ) : (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset = (PairReduction.logSizeBallSeq J hJ a c i).finset \ (PairReduction.logSizeBallSeq J hJ a c i).smallBall c
• PairReduction.finset_logSizeBallSeq_add_one_ssubset 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (i : ℕ) (h : (PairReduction.logSizeBallSeq J hJ a c i).finset.Nonempty) : (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset ⊂ (PairReduction.logSizeBallSeq J hJ a c i).finset
• PairReduction.radius_logSizeBallSeq_le 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {n : ℕ} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (ha : 1 < a) (hn : 1 ≤ n) (hJ_card : ↑J.card ≤ a ^ n) (i : ℕ) : (PairReduction.logSizeBallSeq J hJ a c i).radius ≤ n
• PairReduction.radius_logSizeBallSeq_add_one 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (i : ℕ) : (PairReduction.logSizeBallSeq J hJ a c (i + 1)).radius = PairReduction.logSizeRadius (PairReduction.logSizeBallSeq J hJ a c (i + 1)).point (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset a c
• PairReduction.edist_le_of_mem_pairSet 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {n : ℕ} {J : Finset T} [DecidableEq T] (ha : 1 < a) (hJ_card : ↑J.card ≤ a ^ n) {s t : T} (h : (s, t) ∈ PairReduction.pairSet J a c) : edist s t ≤ ↑n * c
• PairReduction.card_pairSetSeq_le_logSizeRadius_mul 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (i : ℕ) (ha : 1 < a) : ↑(PairReduction.pairSetSeq J a c i).card ≤ (if (PairReduction.logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (PairReduction.logSizeBallSeq J hJ a c i).radius
• PairReduction.exists_radius_le 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a : ENNReal} (t : T) (V : Finset T) (ha : 1 < a) (c : ENNReal) : ∃ r, 1 ≤ r ∧ ↑{x ∈ V | edist t x ≤ ↑r * c}.card ≤ a ^ r
• PairReduction.card_le_logSizeRadius_le_pow_logSizeRadius 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {V : Finset T} {t : T} (ha : 1 < a) : ↑{x ∈ V | edist t x ≤ ↑(PairReduction.logSizeRadius t V a c) * c}.card ≤ a ^ PairReduction.logSizeRadius t V a c
• PairReduction.logSizeRadius_le_card_smallBall 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (i : ℕ) (ha : 1 < a) : (if (PairReduction.logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((PairReduction.logSizeBallSeq J hJ a c i).radius - 1) ≤ ↑((PairReduction.logSizeBallSeq J hJ a c i).smallBall c).card
• PairReduction.pow_logSizeRadius_le_card_le_logSizeRadius 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {V : Finset T} {t : T} (ha : 1 < a) (ht : t ∈ V) : a ^ (PairReduction.logSizeRadius t V a c - 1) ≤ ↑{x ∈ V | edist t x ≤ (↑(PairReduction.logSizeRadius t V a c) - 1) * c}.card
• PairReduction.point_logSizeBallSeq_add_one 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] (hJ : J.Nonempty) (i : ℕ) : (PairReduction.logSizeBallSeq J hJ a c (i + 1)).point = if hV' : (PairReduction.logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then Exists.choose hV' else (PairReduction.logSizeBallSeq J hJ a c i).point
• PairReduction.iSup_edist_pairSet 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [DecidableEq T] {E : Type u_2} [TopologicalSpace E] [WeakPseudoEMetricSpace E] (ha : 1 < a) (f : T → E) : ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
• EMetric.pair_reduction 📋 Mathlib.Topology.EMetricSpace.PairReduction
  {T : Type u_1} [TopologicalSpace T] [WeakPseudoEMetricSpace T] {a : ENNReal} {n : ℕ} {J : Finset T} (hJ_card : ↑J.card ≤ a ^ n) (c : ENNReal) (E : Type u_2) [TopologicalSpace E] [WeakPseudoEMetricSpace E] : ∃ K ⊆ J ×ˢ J, ↑K.card ≤ a * ↑J.card ∧ (∀ (s t : T), (s, t) ∈ K → edist s t ≤ ↑n * c) ∧ ∀ (f : T → E), ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
• instWeakPseudoEMetricSpaceOnePoint 📋 Mathlib.Topology.EMetricSpace.Weak
  {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] : WeakPseudoEMetricSpace (OnePoint α)
• Option.edist_none_some 📋 Mathlib.Topology.EMetricSpace.Weak
  {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] {a : α} : edist none (some a) = ⊤
• Option.edist_some_none 📋 Mathlib.Topology.EMetricSpace.Weak
  {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] {a : α} : edist (some a) none = ⊤
• Option.edist_none_none 📋 Mathlib.Topology.EMetricSpace.Weak
  {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] : edist none none = 0
• Option.edist_self' 📋 Mathlib.Topology.EMetricSpace.Weak
  {α : Type u} [TopologicalSpace α] (m : WeakPseudoEMetricSpace α) (x : Option α) : edist x x = 0
• Option.edist_some_some 📋 Mathlib.Topology.EMetricSpace.Weak
  {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] {a b : α} : edist (some a) (some b) = edist a b
• Option.edist_comm' 📋 Mathlib.Topology.EMetricSpace.Weak
  {α : Type u} [TopologicalSpace α] (m : WeakPseudoEMetricSpace α) (x y : Option α) : edist x y = edist y x
• Option.WeakPseudoEMetricSpace.OfIsOpenEmbedding 📋 Mathlib.Topology.EMetricSpace.Weak
  {α : Type u} [t : TopologicalSpace α] [TopologicalSpace (Option α)] [m : WeakPseudoEMetricSpace α] [inst : EDist (Option α)] (h_edist : inst = Option.toEDist) (h : Topology.IsOpenEmbedding some) : WeakPseudoEMetricSpace (Option α)
• Option.some_eball 📋 Mathlib.Topology.EMetricSpace.Weak
  {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] (a : α) (r : ENNReal) : some '' Metric.eball a r = Metric.eball (some a) r
• instWeakPseudoEMetricSpaceWithBot 📋 Mathlib.Topology.EMetricSpace.Weak
  {α : Type u} [t : TopologicalSpace α] [LinearOrder α] [OrderTopology α] [m : WeakPseudoEMetricSpace α] : WeakPseudoEMetricSpace (WithBot α)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c