mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
⊢ ∃ C' ⊆ A, C = f '' C'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
⊢ coveringNumber ε (f '' A) = coveringNumber ε A

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f < ∞ ↔ MemHolder r f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f ≠ ∞ ↔ MemHolder r f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f = ∞ ↔ ¬MemHolder r f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ eHolderNorm r (Function.const X c) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ nnHolderNorm r (Function.const X c) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
hX : IsEmpty X
⊢ eHolderNorm r f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: Y : Type u_2
inst✝¹ : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst✝ : PseudoMetricSpace X
hX : BoundedSpace X
f : X → Y
s : ℝ≥0
hf : MemHolder r f
hs : s ≤ r
⊢ MemHolder s f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
d : ℝ≥0∞
⊢ d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = 0 ↔ ∀ C > 0, ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < C

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
s : ℝ≥0
hf : MemHolder r f
hs : s ≤ r
hX : ∃ C, ∀ (x y : X), edist x y ≤ ↑C
⊢ MemHolder s f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ 0 < s.einfsep ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = ∞ ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → edist x y = ∞

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: Y : Type u_2
inst✝¹ : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst✝ : PseudoMetricSpace X
f : X → Y
s : ℝ≥0
A : Set X
hf : ∃ C, HolderOnWith C r f A
hs : s ≤ r
hA : Bornology.IsBounded A
⊢ ∃ C, HolderOnWith C s f A

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep < ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < ∞

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep ≠ ∞ ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
d : ℝ≥0∞
⊢ s.einfsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ edist x y < d

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
D s : ℝ≥0
A : Set X
hf : ∃ C, HolderOnWith C r f A
hs : s ≤ r
hA : ∀ ⦃x : X⦄, x ∈ A → ∀ ⦃y : X⦄, y ∈ A → edist x y ≤ ↑D
⊢ ∃ C, HolderOnWith C s f A

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.einfsep < ∞
⊢ s.Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Subsingleton
⊢ s.einfsep = ∞

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
s t : ℝ≥0
A : Set X
hf₁ : ∃ C, HolderOnWith C r f A
hf₂ : ∃ C, HolderOnWith C t f A
hrs : r ≤ s
hst : s ≤ t
⊢ ∃ C, HolderOnWith C s f A

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : EDist α
d : ℝ≥0∞
f : β → α
s : Set β
⊢ d ≤ (f '' s).einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
ι : Type u_3
o : Option ι
s : ι → Set α
⊢ (⋃ i ∈ o, s i).einfsep = ⨅ i ∈ o, (s i).einfsep

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x : α
s : Set α
⊢ (insert x s).einfsep ≤ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
s t : ℝ≥0
hf₁ : MemHolder r f
hf₂ : MemHolder t f
hrs : r ≤ s
hst : s ≤ t
⊢ MemHolder s f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x y : α
⊢ min (edist x y) (edist y x) ≤ {x, y}.einfsep

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ {x, y}.einfsep ≤ edist y x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.einfsep = ⨅ d, uncurry edist ↑d

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Fintype ↑s
⊢ s.einfsep = s.offDiag.toFinset.inf (uncurry edist)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
hs : s.Finite
⊢ s.einfsep = ⋯.toFinset.inf (uncurry edist)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Finset α
⊢ (↑s).einfsep = s.offDiag.inf (uncurry edist)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ s.offDiag.toFinset.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
⊢ edist x₁ x₂ ^ ↑r ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
hxy : x ≠ y
⊢ {x, y}.einfsep = edist x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
⊢ HolderWith (nnHolderNorm r f) r f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
⊢ ↑(nnHolderNorm r f) = eHolderNorm r f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
⊢ nnHolderNorm r f ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
⊢ nnHolderNorm r f = 0 ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
𝕜 : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : Module 𝕜 Y
inst✝ : NormSMulClass 𝕜 Y
c : 𝕜
hc : ‖c‖₊ ≠ 0
⊢ MemHolder r (c • f) ↔ MemHolder r f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
inst✝ : NormedSpace ℝ Y
n : ℕ
hf : MemHolder r f
⊢ MemHolder r (n • f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ (insert x s).einfsep = min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : NormedAddCommGroup Y
r : ℝ≥0
f g : X → Y
⊢ eHolderNorm r (f + g) ≤ eHolderNorm r f + eHolderNorm r g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ {x, y, z}.einfsep = min (min (edist x y) (edist x z)) (edist y z)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
s : (b : β) → Set (X b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
⊢ c ≤ (univ.pi s).einfsep

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
s : (b : β) → Set (X b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
⊢ c ≤ (univ.pi s).einfsep

Tactic:
by
  refine le_einfsep fun x hx y hy hxy => ?_
  rw [mem_univ_pi] at hx hy
  rcases Function.ne_iff.mp hxy with ⟨i, hi⟩
  exact le_trans (le_einfsep_iff.1 (h i) _ (hx _) _ (hy _) hi) (edist_le_pi_edist _ _ i)

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.einfsep = ∞
⊢ s.Subsingleton

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep < ∞

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ 0 < s.einfsep

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ s.infsep = 0 ↔ s.einfsep = 0 ∨ s.einfsep = ∞

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ 0 < s.infsep ↔ 0 < s.einfsep ∧ s.einfsep < ∞

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
hs : 0 < s.infsep
⊢ s.Nontrivial

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ {x, y}.infsep ≤ (min (edist x y) (edist y x)).toReal

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y : α
⊢ {x, y}.infsep = (edist x y).toReal

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ s.infsep < d ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ dist x y < d

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
hd : d ≤ s.infsep
⊢ d ≤ dist x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
x y : α
⊢ {x, y}.infsep = dist x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ {x, y, z}.infsep = min (min (dist x y) (dist x z)) (dist y z)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
⊢ BddBelow (uncurry dist '' s.offDiag)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
hf : MemHolder r f
c : α
⊢ nnHolderNorm r (c • f) = ‖c‖₊ * nnHolderNorm r f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
inst✝ : NormedSpace ℝ Y
n : ℕ
⊢ eHolderNorm r (n • f) = n • eHolderNorm r f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
inst✝ : NormedSpace ℝ Y
n : ℕ
hf : MemHolder r f
⊢ nnHolderNorm r (n • f) = n • nnHolderNorm r f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
⊢ s.infsep = if s.Nontrivial then ⨅ d, uncurry dist ↑d else 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.infsep = ⨅ d, uncurry dist ↑d

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.offDiag.toFinset.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.ShrinkingLemma

Goal state before:
pp: α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite
us : s ⊆ ⋃ i, ball (c i) (r i)
⊢ ∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.ShrinkingLemma

Goal state before:
pp: α : Type u
ι : Type v
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
c : ι → α
s : Set α
r : ι → ℝ
hr : ∀ (i : ι), 0 < r i
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
uf : ∀ x ∈ s, {i | x ∈ ball (c i) (r i)}.Finite
us : s ⊆ ⋃ i, ball (c i) (r i)
⊢ ∃ r', s ⊆ ⋃ i, ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Ioo 0 (r i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.ShrinkingLemma

Goal state before:
pp: α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ i, ball (c i) (r i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.ShrinkingLemma

Goal state before:
pp: α : Type u
inst✝¹ : MetricSpace α
inst✝ : ProperSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
R : α → ℝ
hR : ∀ x ∈ s, 0 < R x
⊢ ∃ ι c r r',
    (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
      (LocallyFinite fun i ↦ ball (c i) (r' i)) ∧ s ⊆ ⋃ i, ball (c i) (r i)

Tactic:
by
  have : ∀ x ∈ s, (𝓝 x).HasBasis (fun r : ℝ => 0 < r ∧ r < R x) fun r => ball x r := fun x hx =>
    nhds_basis_uniformity (uniformity_basis_dist_lt (hR x hx))
  rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs this with
    ⟨ι, c, r', hr', hsub', hfin⟩
  rcases exists_subset_iUnion_ball_radius_pos_lt (fun i => (hr' i).2.1) hs
      (fun x _ => hfin.point_finite x) hsub' with
    ⟨r, hsub, hlt⟩
  exact ⟨ι, c, r, r', fun i => ⟨(hr' i).1, (hlt i).1, (hlt i).2, (hr' i).2.2⟩, hfin, hsub⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
⊢ s.infsep = if hs : s.Nontrivial then s.offDiag.toFinset.inf' ⋯ (uncurry dist) else 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.offDiag.toFinset.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
⊢ ⋯.toFinset.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun n ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = ↑p
f : ↑(range Ψ) ≃ᵢ ↑(range (kuratowskiEmbedding X))
⊢ (↑(range Ψ) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding X)) = (↥p ≃ᵢ ↑(range (kuratowskiEmbedding X)))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝² : MetricSpace X
inst✝¹ : CompactSpace X
inst✝ : Nonempty X
p : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
⊢ ⟦p⟧ = toGHSpace X ↔ ∃ Ψ, Isometry Ψ ∧ range Ψ = ↑p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: p : GHSpace
⊢ toGHSpace p.Rep = p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
⊢ (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)) =
    (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y)))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
⊢ s.infsep = if hs : s.Nontrivial then ⋯.toFinset.inf' ⋯ (uncurry dist) else 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
hsf : s.Finite
hs : s.Nontrivial
⊢ ⋯.toFinset.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ toGHSpace X = toGHSpace Y → Nonempty (X ≃ᵢ Y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hsf : s.Finite
hs : s.Nontrivial
⊢ s.infsep = ⋯.toFinset.inf' ⋯ (uncurry dist)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
⊢ (↑s).Nontrivial ↔ s.offDiag.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
e : X ≃ᵢ Y
f : ↑(range (kuratowskiEmbedding X)) ≃ᵢ X
g : Y ≃ᵢ ↑(range (kuratowskiEmbedding Y))
⊢ (↑(range (kuratowskiEmbedding X)) ≃ᵢ ↑(range (kuratowskiEmbedding Y))) =
    (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
⊢ (↑s).infsep = if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
hs : s.offDiag.Nonempty
⊢ (↑s).infsep = s.offDiag.inf' hs (uncurry dist)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
hs : s.offDiag = ∅
⊢ (↑s).infsep = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ s.offDiag.toFinset.Nonempty

Tactic:
by

Goal state after: