theorem
ContinuousWithinAt.ennreal_mul
{X : Type u_1}
[TopologicalSpace X]
{f g : X → ENNReal}
{s : Set X}
{t : X}
(hf : ContinuousWithinAt f s t)
(hg : ContinuousWithinAt g s t)
(h₁ : f t ≠ 0 ∨ g t ≠ ⊤)
(h₂ : g t ≠ 0 ∨ f t ≠ ⊤)
:
ContinuousWithinAt (fun (x : X) => f x * g x) s t
theorem
ContinuousWithinAt.measure_lt_ne_zero
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
[TopologicalSpace α]
[LinearOrder α]
[DenselyOrdered α]
[OrderTopology α]
[ClosedIicTopology α]
[μ.IsOpenPosMeasure]
{f : α → ENNReal}
{x : α}
(hx : ¬IsMax x)
(hf : ContinuousWithinAt f (Set.Ioi x) x)
{a : ENNReal}
(ha : a < f x)
:
theorem
eLpNormEssSup_eq_iSup'
{f : ENNReal → ENNReal}
(hf : ∀ (a x : ENNReal), a < f x → ContinuousWithinAt f (Set.Ioi x) x)
(f_top : f ⊤ = ⊥)
:
theorem
eLpNormEssSup_nnreal_eq_iSup_nnreal
{f : ENNReal → ENNReal}
(hf : ∀ (a : ENNReal) (x : NNReal), a < f ↑x → ContinuousWithinAt f (Set.Ioi ↑x) ↑x)
: