theorem
neBot_comap_nhds
{X : Type u_1}
[PseudoEMetricSpace X]
{s : Set X}
(hs : Dense s)
(x : X)
:
(Filter.comap Subtype.val (nhds x)).NeBot
theorem
Dense.holderWith_extend
{X : Type u_1}
{Y : Type u_2}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
[CompleteSpace Y]
{C r : NNReal}
{s : Set X}
{f : ↑s → Y}
(hs : Dense s)
(hf : HolderWith C r f)
(hr : 0 < r)
:
HolderWith C r (hs.extend f)
theorem
PseudoEMetricSpace.boundedSpace_toPseudoMetricSpace
{X : Type u_1}
[PseudoEMetricSpace X]
{C : NNReal}
(hX : ∀ (x y : X), edist x y ≤ ↑C)
:
theorem
MemHolder.mono
{X : Type u_3}
{Y : Type u_4}
[PseudoMetricSpace X]
[hX : BoundedSpace X]
[PseudoEMetricSpace Y]
{f : X → Y}
{r s : NNReal}
(hf : MemHolder r f)
(hs : s ≤ r)
:
MemHolder s f
theorem
MemHolder.mono'
{X : Type u_3}
{Y : Type u_4}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{f : X → Y}
{r s : NNReal}
(hf : MemHolder r f)
(hs : s ≤ r)
{C' : NNReal}
(hX : ∀ (x y : X), edist x y ≤ ↑C')
:
MemHolder s f
theorem
HolderOnWith.mono_right
{X : Type u_3}
{Y : Type u_4}
[PseudoMetricSpace X]
[PseudoEMetricSpace Y]
{f : X → Y}
{C r s : NNReal}
{t : Set X}
(hf : HolderOnWith C r f t)
(hs : s ≤ r)
(ht : Bornology.IsBounded t)
:
∃ (C' : NNReal), HolderOnWith C' s f t
theorem
HolderOnWith.mono_right'
{X : Type u_3}
{Y : Type u_4}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{f : X → Y}
{C r s : NNReal}
{t : Set X}
(hf : HolderOnWith C r f t)
(hs : s ≤ r)
{C' : NNReal}
(ht : ∀ ⦃x : X⦄, x ∈ t → ∀ ⦃y : X⦄, y ∈ t → edist x y ≤ ↑C')
:
∃ (C' : NNReal), HolderOnWith C' s f t
theorem
HolderWith.HolderWith_of_le_of_le
{X : Type u_3}
{Y : Type u_4}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{f : X → Y}
{C₁ C₂ r s t : NNReal}
(hf₁ : HolderWith C₁ r f)
(hf₂ : HolderWith C₂ t f)
(hrs : r ≤ s)
(hst : s ≤ t)
:
HolderWith (max C₁ C₂) s f
theorem
HolderOnWith.holderOnWith_of_le_of_le
{X : Type u_3}
{Y : Type u_4}
[PseudoEMetricSpace X]
[PseudoEMetricSpace Y]
{f : X → Y}
{C₁ C₂ r s t : NNReal}
{u : Set X}
(hf₁ : HolderOnWith C₁ r f u)
(hf₂ : HolderOnWith C₂ t f u)
(hrs : r ≤ s)
(hst : s ≤ t)
:
HolderOnWith (max C₁ C₂) s f u