Loogle!

Result

Found 129 declarations mentioning Set.uIoc.

• Set.uIoc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] : α → α → Set α
• Set.uIoc_injective_left 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] (a : α) : Function.Injective (Set.uIoc a)
• Set.uIoc_injective_right 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] (a : α) : Function.Injective fun b => Set.uIoc b a
• Set.nonempty_uIoc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b : α} : (Set.uIoc a b).Nonempty ↔ a ≠ b
• Set.uIoc_comm 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] (a b : α) : Set.uIoc a b = Set.uIoc b a
• Set.uIoc_subset_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b : α} : Set.uIoc a b ⊆ Set.uIcc a b
• Set.Ioc_subset_uIoc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ioc a b ⊆ Set.uIoc a b
• Set.Ioc_subset_uIoc' 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b : α} : Set.Ioc a b ⊆ Set.uIoc b a
• Set.eq_of_mem_uIoc_of_mem_uIoc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b c : α} : a ∈ Set.uIoc b c → b ∈ Set.uIoc a c → a = b
• Set.eq_of_mem_uIoc_of_mem_uIoc' 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b c : α} : b ∈ Set.uIoc a c → c ∈ Set.uIoc a b → b = c
• Set.left_mem_uIoc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b : α} : a ∈ Set.uIoc a b ↔ b < a
• Set.right_mem_uIoc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b : α} : b ∈ Set.uIoc a b ↔ a < b
• Set.uIoc_of_ge 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b : α} (h : b ≤ a) : Set.uIoc a b = Set.Ioc b a
• Set.uIoc_of_le 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b : α} (h : a ≤ b) : Set.uIoc a b = Set.Ioc a b
• Set.uIoc_subset_uIoc_of_uIcc_subset_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b c d : α} (h : Set.uIcc a b ⊆ Set.uIcc c d) : Set.uIoc a b ⊆ Set.uIoc c d
• Set.uIoc_union_uIoc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b c : α} (h : b ∈ Set.uIcc a c) : Set.uIoc a b ∪ Set.uIoc b c = Set.uIoc a c
• Set.uIoc_eq_union 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b : α} : Set.uIoc a b = Set.Ioc a b ∪ Set.Ioc b a
• Set.eq_of_notMem_uIoc_of_notMem_uIoc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b c : α} (ha : a ≤ c) (hb : b ≤ c) : a ∉ Set.uIoc b c → b ∉ Set.uIoc a c → a = b
• Set.forall_uIoc_iff 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b : α} {P : α → Prop} : (∀ x ∈ Set.uIoc a b, P x) ↔ (∀ x ∈ Set.Ioc a b, P x) ∧ ∀ x ∈ Set.Ioc b a, P x
• Set.mem_uIoc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b c : α} : a ∈ Set.uIoc b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
• Set.notMem_uIoc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
  {α : Type u_1} [LinearOrder α] {a b c : α} : a ∉ Set.uIoc b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a
• OrderEmbedding.preimage_uIoc 📋 Mathlib.Order.Interval.Set.OrderEmbedding
  {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (e : α ↪o β) (x y : α) : ⇑e ⁻¹' Set.uIoc (e x) (e y) = Set.uIoc x y
• Set.ordConnected_uIoc 📋 Mathlib.Order.Interval.Set.OrdConnected
  {α : Type u_1} [LinearOrder α] {a b : α} : (Set.uIoc a b).OrdConnected
• Set.OrdConnected.uIoc_subset 📋 Mathlib.Order.Interval.Set.OrdConnected
  {α : Type u_1} [LinearOrder α] {s : Set α} (hs : s.OrdConnected) ⦃x : α⦄ (hx : x ∈ s) ⦃y : α⦄ (hy : y ∈ s) : Set.uIoc x y ⊆ s
• Set.image_subtype_val_uIoc 📋 Mathlib.Order.Interval.Set.OrdConnected
  {α : Type u_1} [LinearOrder α] {s : Set α} [s.OrdConnected] (a b : ↑s) : Subtype.val '' Set.uIoc a b = Set.uIoc ↑a ↑b
• NNRat.preimage_cast_uIoc 📋 Mathlib.Data.Rat.Cast.Order
  {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0) : NNRat.cast ⁻¹' Set.uIoc ↑p ↑q = Set.uIoc p q
• Rat.preimage_cast_uIoc 📋 Mathlib.Data.Rat.Cast.Order
  {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) : Rat.cast ⁻¹' Set.uIoc ↑p ↑q = Set.uIoc p q
• Fin.image_val_uIoc 📋 Mathlib.Order.Interval.Set.Fin
  {n : ℕ} (i j : Fin n) : Fin.val '' Set.uIoc i j = Set.uIoc ↑i ↑j
• Fin.preimage_val_uIoc_val 📋 Mathlib.Order.Interval.Set.Fin
  {n : ℕ} (i j : Fin n) : Fin.val ⁻¹' Set.uIoc ↑i ↑j = Set.uIoc i j
• Fin.image_castLE_uIoc 📋 Mathlib.Order.Interval.Set.Fin
  {m n : ℕ} (i j : Fin m) (h : m ≤ n) : Fin.castLE h '' Set.uIoc i j = Set.uIoc (Fin.castLE h i) (Fin.castLE h j)
• Fin.preimage_castLE_uIoc_castLE 📋 Mathlib.Order.Interval.Set.Fin
  {m n : ℕ} (i j : Fin m) (h : m ≤ n) : Fin.castLE h ⁻¹' Set.uIoc (Fin.castLE h i) (Fin.castLE h j) = Set.uIoc i j
• Fin.preimage_cast_uIoc 📋 Mathlib.Order.Interval.Set.Fin
  {m n : ℕ} (h : m = n) (i j : Fin n) : Fin.cast h ⁻¹' Set.uIoc i j = Set.uIoc (Fin.cast ⋯ i) (Fin.cast ⋯ j)
• Fin.preimage_castAdd_uIoc_castAdd 📋 Mathlib.Order.Interval.Set.Fin
  {n : ℕ} (m : ℕ) (i j : Fin n) : Fin.castAdd m ⁻¹' Set.uIoc (Fin.castAdd m i) (Fin.castAdd m j) = Set.uIoc i j
• Fin.preimage_natAdd_uIoc_natAdd 📋 Mathlib.Order.Interval.Set.Fin
  {n : ℕ} (m : ℕ) (i j : Fin n) : Fin.natAdd m ⁻¹' Set.uIoc (Fin.natAdd m i) (Fin.natAdd m j) = Set.uIoc i j
• Fin.preimage_addNat_uIoc_addNat 📋 Mathlib.Order.Interval.Set.Fin
  {n : ℕ} (m : ℕ) (i j : Fin n) : (fun x => x.addNat m) ⁻¹' Set.uIoc (i.addNat m) (j.addNat m) = Set.uIoc i j
• Fin.image_castAdd_uIoc 📋 Mathlib.Order.Interval.Set.Fin
  {n : ℕ} (m : ℕ) (i j : Fin n) : Fin.castAdd m '' Set.uIoc i j = Set.uIoc (Fin.castAdd m i) (Fin.castAdd m j)
• Fin.image_natAdd_uIoc 📋 Mathlib.Order.Interval.Set.Fin
  {n : ℕ} (m : ℕ) (i j : Fin n) : Fin.natAdd m '' Set.uIoc i j = Set.uIoc (Fin.natAdd m i) (Fin.natAdd m j)
• Fin.preimage_castSucc_uIoc_castSucc 📋 Mathlib.Order.Interval.Set.Fin
  {n : ℕ} (i j : Fin n) : Fin.castSucc ⁻¹' Set.uIoc i.castSucc j.castSucc = Set.uIoc i j
• Fin.preimage_succ_uIoc_succ 📋 Mathlib.Order.Interval.Set.Fin
  {n : ℕ} (i j : Fin n) : Fin.succ ⁻¹' Set.uIoc i.succ j.succ = Set.uIoc i j
• Fin.image_addNat_uIoc 📋 Mathlib.Order.Interval.Set.Fin
  {n : ℕ} (m : ℕ) (i j : Fin n) : (fun x => x.addNat m) '' Set.uIoc i j = Set.uIoc (i.addNat m) (j.addNat m)
• Fin.image_castSucc_uIoc 📋 Mathlib.Order.Interval.Set.Fin
  {n : ℕ} (i j : Fin n) : Fin.castSucc '' Set.uIoc i j = Set.uIoc i.castSucc j.castSucc
• Fin.image_succ_uIoc 📋 Mathlib.Order.Interval.Set.Fin
  {n : ℕ} (i j : Fin n) : Fin.succ '' Set.uIoc i j = Set.uIoc i.succ j.succ
• ENNReal.image_coe_uIoc 📋 Mathlib.Basic.ENNReal.Operations
  (x y : NNReal) : ENNReal.ofNNReal '' Set.uIoc x y = Set.uIoc ↑x ↑y
• NNReal.image_coe_uIoc 📋 Mathlib.Basic.NNReal.Basic
  (x y : NNReal) : NNReal.toReal '' Set.uIoc x y = Set.uIoc ↑x ↑y
• closure_uIoc 📋 Mathlib.Topology.Order.DenselyOrdered
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} (hab : a ≠ b) : closure (Set.uIoc a b) = Set.uIcc a b
• isPreconnected_uIoc 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} : IsPreconnected (Set.uIoc a b)
• isConnected_uIoc 📋 Mathlib.Topology.Order.IntermediateValue
  {α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} (h : a ≠ b) : IsConnected (Set.uIoc a b)
• MeasureTheory.ae_restrict_uIoc_eq 📋 Mathlib.MeasureTheory.Measure.Restrict
  {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [LinearOrder α] (a b : α) : MeasureTheory.ae (μ.restrict (Set.uIoc a b)) = MeasureTheory.ae (μ.restrict (Set.Ioc a b)) ⊔ MeasureTheory.ae (μ.restrict (Set.Ioc b a))
• MeasureTheory.ae_restrict_uIoc_iff 📋 Mathlib.MeasureTheory.Measure.Restrict
  {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [LinearOrder α] {a b : α} {P : α → Prop} : (∀ᵐ (x : α) ∂μ.restrict (Set.uIoc a b), P x) ↔ (∀ᵐ (x : α) ∂μ.restrict (Set.Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Set.Ioc b a), P x
• MeasureTheory.ae_uIoc_iff 📋 Mathlib.MeasureTheory.Measure.Restrict
  {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [LinearOrder α] {a b : α} {P : α → Prop} : (∀ᵐ (x : α) ∂μ, x ∈ Set.uIoc a b → P x) ↔ (∀ᵐ (x : α) ∂μ, x ∈ Set.Ioc a b → P x) ∧ ∀ᵐ (x : α) ∂μ, x ∈ Set.Ioc b a → P x
• aemeasurable_uIoc_iff 📋 Mathlib.MeasureTheory.Measure.AEMeasurable
  {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [MeasurableSpace β] {μ : MeasureTheory.Measure α} [LinearOrder α] {f : α → β} {a b : α} : AEMeasurable f (μ.restrict (Set.uIoc a b)) ↔ AEMeasurable f (μ.restrict (Set.Ioc a b)) ∧ AEMeasurable f (μ.restrict (Set.Ioc b a))
• measurableSet_uIoc 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
  {α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] {a b : α} [ClosedIicTopology α] : MeasurableSet (Set.uIoc a b)
• MeasureTheory.uIoc_ae_eq_interval 📋 Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
  {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ] [LinearOrder α] {a b : α} : Set.uIoc a b =ᵐ[μ] Set.uIcc a b
• MeasureTheory.AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff 📋 Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
  {α : Type u_1} {β : Type u_2} [TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [LinearOrder α] [TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {a b : α} : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b)) ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc a b)) ∧ MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc b a))
• strictConvex_uIoc 📋 Mathlib.Analysis.Convex.Strict
  {𝕜 : Type u_1} {β : Type u_5} [Semiring 𝕜] [PartialOrder 𝕜] [TopologicalSpace β] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [OrderTopology β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β) : StrictConvex 𝕜 (Set.uIoc r s)
• Continuous.integrableOn_uIoc 📋 Mathlib.MeasureTheory.Function.LocallyIntegrable
  {X : Type u_1} {E : Type u_6} [MeasurableSpace X] [TopologicalSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} {a b : X} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [LinearOrder X] [CompactIccSpace X] [T2Space X] (hf : Continuous f) : MeasureTheory.IntegrableOn f (Set.uIoc a b) μ
• Real.volume_uIoc 📋 Mathlib.MeasureTheory.Measure.Lebesgue.Basic
  {a b : ℝ} : MeasureTheory.volume (Set.uIoc a b) = ENNReal.ofReal |b - a|
• IntervalIntegrable.aestronglyMeasurable_restrict_uIoc 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (h : IntervalIntegrable f μ a b) : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b))
• IntervalIntegrable.def' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (h : IntervalIntegrable f μ a b) : MeasureTheory.IntegrableOn f (Set.uIoc a b) μ
• intervalIntegrable_iff 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} : IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.uIoc a b) μ
• IntervalIntegrable.congr 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ε} (h : Set.EqOn f g (Set.uIoc a b)) : IntervalIntegrable f μ a b → IntervalIntegrable g μ a b
• intervalIntegrable_congr 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ε} (h : Set.EqOn f g (Set.uIoc a b)) : IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b
• IntervalIntegrable.mono_set' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : ℝ → ε} {a b c d : ℝ} {μ : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε] (hf : IntervalIntegrable f μ a b) (hsub : Set.uIoc c d ⊆ Set.uIoc a b) : IntervalIntegrable f μ c d
• IntervalIntegrable.congr_codiscreteWithin 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ε} [MeasureTheory.NullSingletonClass μ] (h : f =ᶠ[Filter.codiscreteWithin (Set.uIoc a b)] g) (hf : IntervalIntegrable f μ a b) : IntervalIntegrable g μ a b
• intervalIntegrable_congr_codiscreteWithin 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ε} [MeasureTheory.NullSingletonClass μ] (h : f =ᶠ[Filter.codiscreteWithin (Set.uIoc a b)] g) : IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b
• intervalIntegral.norm_integral_eq_norm_integral_uIoc 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (f : ℝ → E) : ‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Set.uIoc a b, f x ∂μ‖
• intervalIntegral.norm_intervalIntegral_eq 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (a b : ℝ) (μ : MeasureTheory.Measure ℝ) : ‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Set.uIoc a b, f x ∂μ‖
• IntervalIntegrable.mono_set_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : ℝ → ε} {a b c d : ℝ} {μ : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε] (hf : IntervalIntegrable f μ a b) (h : Set.uIoc c d ≤ᵐ[μ] Set.uIoc a b) : IntervalIntegrable f μ c d
• IntervalIntegrable.congr_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ε} (hf : IntervalIntegrable f μ a b) (h : f =ᵐ[μ.restrict (Set.uIoc a b)] g) : IntervalIntegrable g μ a b
• intervalIntegrable_congr_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ε} (h : f =ᵐ[μ.restrict (Set.uIoc a b)] g) : IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b
• intervalIntegral.abs_integral_eq_abs_integral_uIoc 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (f : ℝ → ℝ) : |∫ (x : ℝ) in a..b, f x ∂μ| = |∫ (x : ℝ) in Set.uIoc a b, f x ∂μ|
• intervalIntegral.abs_intervalIntegral_eq 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  (f : ℝ → ℝ) (a b : ℝ) (μ : MeasureTheory.Measure ℝ) : |∫ (x : ℝ) in a..b, f x ∂μ| = |∫ (x : ℝ) in Set.uIoc a b, f x ∂μ|
• IntervalIntegrable.intervalIntegrable_enorm_iff 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : ℝ → ε} [TopologicalSpace.PseudoMetrizableSpace ε] {μ : MeasureTheory.Measure ℝ} {a b : ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b))) : IntervalIntegrable (fun t => ‖f t‖ₑ) μ a b ↔ IntervalIntegrable f μ a b
• intervalIntegral.integral_congr_ae_restrict 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f g : ℝ → E} {μ : MeasureTheory.Measure ℝ} (h : f =ᵐ[μ.restrict (Set.uIoc a b)] g) : ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
• intervalIntegral.integral_congr_codiscreteWithin 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {a b : ℝ} {f₁ f₂ : ℝ → ℝ} (hf : f₁ =ᶠ[Filter.codiscreteWithin (Set.uIoc a b)] f₂) : ∫ (x : ℝ) in a..b, f₁ x = ∫ (x : ℝ) in a..b, f₂ x
• intervalIntegral.norm_integral_le_integral_norm_uIoc 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} : ‖∫ (x : ℝ) in a..b, f x ∂μ‖ ≤ ∫ (x : ℝ) in Set.uIoc a b, ‖f x‖ ∂μ
• intervalIntegral.integral_non_aestronglyMeasurable 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} (hf : ¬MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b))) : ∫ (x : ℝ) in a..b, f x ∂μ = 0
• intervalIntegral.integral_congr_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f g : ℝ → E} {μ : MeasureTheory.Measure ℝ} (h : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.uIoc a b → f x = g x) : ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
• IntervalIntegrable.intervalIntegrable_norm_iff 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {a b : ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b))) : IntervalIntegrable (fun t => ‖f t‖) μ a b ↔ IntervalIntegrable f μ a b
• intervalIntegral.norm_integral_le_of_norm_le_const 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b C : ℝ} {f : ℝ → E} (h : ∀ x ∈ Set.uIoc a b, ‖f x‖ ≤ C) : ‖∫ (x : ℝ) in a..b, f x‖ ≤ C * |b - a|
• IntervalIntegrable.mono_fun_enorm' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε] {f : ℝ → ε} {g : ℝ → ENNReal} (hg : IntervalIntegrable g μ a b) (hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b))) (hle : (fun x => ‖f x‖ₑ) ≤ᵐ[μ.restrict (Set.uIoc a b)] g) : IntervalIntegrable f μ a b
• intervalIntegrable_const_iff 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {c : ε} (hc : ‖c‖ₑ ≠ ⊤ := by finiteness) : IntervalIntegrable (fun x => c) μ a b ↔ c = 0 ∨ μ (Set.uIoc a b) < ⊤
• intervalIntegral.integral_cases 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} (f : ℝ → E) (a b : ℝ) : ∫ (x : ℝ) in a..b, f x ∂μ ∈ {∫ (x : ℝ) in Set.uIoc a b, f x ∂μ, -∫ (x : ℝ) in Set.uIoc a b, f x ∂μ}
• intervalIntegral.integral_zero_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} (h : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.uIoc a b → f x = 0) : ∫ (x : ℝ) in a..b, f x ∂μ = 0
• intervalIntegral.norm_integral_le_of_norm_le_const_ae 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b C : ℝ} {f : ℝ → E} (h : ∀ᵐ (x : ℝ), x ∈ Set.uIoc a b → ‖f x‖ ≤ C) : ‖∫ (x : ℝ) in a..b, f x‖ ≤ C * |b - a|
• IntervalIntegrable.mono_fun' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} {g : ℝ → ℝ} (hg : IntervalIntegrable g μ a b) (hfm : MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b))) (hle : (fun x => ‖f x‖) ≤ᵐ[μ.restrict (Set.uIoc a b)] g) : IntervalIntegrable f μ a b
• intervalIntegral.norm_integral_le_abs_of_norm_le 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {g : ℝ → ℝ} (h : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ‖f t‖ ≤ g t) (hbound : IntervalIntegrable g μ a b) : ‖∫ (t : ℝ) in a..b, f t ∂μ‖ ≤ |∫ (t : ℝ) in a..b, g t ∂μ|
• IntervalIntegrable.mono_fun_enorm 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {ε : Type u_3} {ε' : Type u_4} [TopologicalSpace ε] [ENormedAddMonoid ε] [TopologicalSpace ε'] [ENormedAddMonoid ε'] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε] [TopologicalSpace.PseudoMetrizableSpace ε'] {g : ℝ → ε'} (hf : IntervalIntegrable f μ a b) (hgm : MeasureTheory.AEStronglyMeasurable g (μ.restrict (Set.uIoc a b))) (hle : (fun x => ‖g x‖ₑ) ≤ᵐ[μ.restrict (Set.uIoc a b)] fun x => ‖f x‖ₑ) : IntervalIntegrable g μ a b
• IntervalIntegrable.mono_fun 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [NormedAddCommGroup F] {g : ℝ → F} (hf : IntervalIntegrable f μ a b) (hgm : MeasureTheory.AEStronglyMeasurable g (μ.restrict (Set.uIoc a b))) (hle : (fun x => ‖g x‖) ≤ᵐ[μ.restrict (Set.uIoc a b)] fun x => ‖f x‖) : IntervalIntegrable g μ a b
• intervalIntegral.abs_integral_mono_interval 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {c d : ℝ} (h : Set.uIoc a b ⊆ Set.uIoc c d) (hf : 0 ≤ᵐ[μ.restrict (Set.uIoc c d)] f) (hfi : IntervalIntegrable f μ c d) : |∫ (x : ℝ) in a..b, f x ∂μ| ≤ |∫ (x : ℝ) in c..d, f x ∂μ|
• intervalIntegral.integral_pos_iff_support_of_nonneg_ae' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : 0 ≤ᵐ[μ.restrict (Set.uIoc a b)] f) (hfi : IntervalIntegrable f μ a b) : 0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (Function.support f ∩ Set.Ioc a b)
• intervalIntegral.intervalIntegral_eq_integral_uIoc 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
  {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (a b : ℝ) (μ : MeasureTheory.Measure ℝ) : ∫ (x : ℝ) in a..b, f x ∂μ = (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Set.uIoc a b, f x ∂μ
• intervalIntegral.continuous_of_dominated_interval 📋 Mathlib.MeasureTheory.Integral.DominatedConvergence
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {X : Type u_3} [TopologicalSpace X] [FirstCountableTopology X] {F : X → ℝ → E} {bound : ℝ → ℝ} {a b : ℝ} (hF_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (h_bound : ∀ (x : X), ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ‖F x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → Continuous fun x => F x t) : Continuous fun x => ∫ (t : ℝ) in a..b, F x t ∂μ
• intervalIntegral.continuousAt_of_dominated_interval 📋 Mathlib.MeasureTheory.Integral.DominatedConvergence
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {X : Type u_3} [TopologicalSpace X] [FirstCountableTopology X] {F : X → ℝ → E} {x₀ : X} {bound : ℝ → ℝ} {a b : ℝ} (hF_meas : ∀ᶠ (x : X) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ‖F x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ContinuousAt (fun x => F x t) x₀) : ContinuousAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) x₀
• intervalIntegral.continuousWithinAt_of_dominated_interval 📋 Mathlib.MeasureTheory.Integral.DominatedConvergence
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ} {X : Type u_3} [TopologicalSpace X] [FirstCountableTopology X] {F : X → ℝ → E} {x₀ : X} {bound : ℝ → ℝ} {a b : ℝ} {s : Set X} (hF_meas : ∀ᶠ (x : X) in nhdsWithin x₀ s, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (h_bound : ∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ‖F x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ContinuousWithinAt (fun x => F x t) s x₀) : ContinuousWithinAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) s x₀
• intervalIntegral.tendsto_integral_filter_of_dominated_convergence 📋 Mathlib.MeasureTheory.Integral.DominatedConvergence
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {ι : Type u_3} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → ℝ → E} (bound : ℝ → ℝ) (hF_meas : ∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F n) (μ.restrict (Set.uIoc a b))) (h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.uIoc a b → ‖F n x‖ ≤ bound x) (bound_integrable : IntervalIntegrable bound μ a b) (h_lim : ∀ᵐ (x : ℝ) ∂μ, x ∈ Set.uIoc a b → Filter.Tendsto (fun n => F n x) l (nhds (f x))) : Filter.Tendsto (fun n => ∫ (x : ℝ) in a..b, F n x ∂μ) l (nhds (∫ (x : ℝ) in a..b, f x ∂μ))
• intervalIntegral.continuousAt_parametric_primitive_of_dominated 📋 Mathlib.MeasureTheory.Integral.DominatedConvergence
  {E : Type u_1} {X : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace X] {μ : MeasureTheory.Measure ℝ} [FirstCountableTopology X] {F : X → ℝ → E} (bound : ℝ → ℝ) (a b : ℝ) {a₀ b₀ : ℝ} {x₀ : X} (hF_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (h_bound : ∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ‖F x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_cont : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ContinuousAt (fun x => F x t) x₀) (ha₀ : a₀ ∈ Set.Ioo a b) (hb₀ : b₀ ∈ Set.Ioo a b) (hμb₀ : μ {b₀} = 0) : ContinuousAt (fun p => ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
• intervalIntegral.hasSum_integral_of_dominated_convergence 📋 Mathlib.MeasureTheory.Integral.DominatedConvergence
  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {ι : Type u_3} [Countable ι] {F : ι → ℝ → E} (bound : ι → ℝ → ℝ) (hF_meas : ∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F n) (μ.restrict (Set.uIoc a b))) (h_bound : ∀ (n : ι), ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ‖F n t‖ ≤ bound n t) (bound_summable : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → Summable fun n => bound n t) (bound_integrable : IntervalIntegrable (fun t => ∑' (n : ι), bound n t) μ a b) (h_lim : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → HasSum (fun n => F n t) (f t)) : HasSum (fun n => ∫ (t : ℝ) in a..b, F n t ∂μ) (∫ (t : ℝ) in a..b, f t ∂μ)
• hasFDerivAt_integral_of_dominated_of_fderiv_le'' 📋 Mathlib.Analysis.Calculus.ParametricIntegral
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_4} [NormedAddCommGroup H] {x₀ : H} {s : Set H} [NormedSpace ℝ H] {μ : MeasureTheory.Measure ℝ} {F : H → ℝ → E} {F' : H → ℝ → H →L[ℝ] E} {a b : ℝ} {bound : ℝ → ℝ} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Set.uIoc a b))) (h_bound : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ∀ x ∈ s, ‖F' x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ∀ x ∈ s, HasFDerivAt (fun x => F x t) (F' x t) x) : HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
• hasFDerivAt_integral_of_dominated_loc_of_lip_interval 📋 Mathlib.Analysis.Calculus.ParametricIntegral
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_4} [NormedAddCommGroup H] {x₀ : H} {s : Set H} [NormedSpace ℝ H] {μ : MeasureTheory.Measure ℝ} {F : H → ℝ → E} {F' : ℝ → H →L[ℝ] E} {a b : ℝ} {bound : ℝ → ℝ} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Set.uIoc a b))) (h_lip : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) s) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), HasFDerivAt (fun x => F x t) (F' t) x₀) : IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
• intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_deriv_le 📋 Mathlib.Analysis.Calculus.ParametricIntervalIntegral
  {𝕜 : Type u_1} [RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {a b : ℝ} {bound : ℝ → ℝ} {F F' : 𝕜 → ℝ → E} {x₀ : 𝕜} {s : Set 𝕜} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Set.uIoc a b))) (h_bound : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ∀ x ∈ s, ‖F' x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ∀ x ∈ s, HasDerivAt (fun x => F x t) (F' x t) x) : IntervalIntegrable (F' x₀) μ a b ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
• intervalIntegral.hasDerivAt_integral_of_dominated_loc_of_lip 📋 Mathlib.Analysis.Calculus.ParametricIntervalIntegral
  {𝕜 : Type u_1} [RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {a b : ℝ} {bound : ℝ → ℝ} {F : 𝕜 → ℝ → E} {F' : ℝ → E} {x₀ : 𝕜} {s : Set 𝕜} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : 𝕜) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Set.uIoc a b))) (h_lipsch : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) s) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → HasDerivAt (fun x => F x t) (F' t) x₀) : IntervalIntegrable F' μ a b ∧ HasDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
• intervalIntegral.hasFDerivAt_integral_of_dominated_of_fderiv_le 📋 Mathlib.Analysis.Calculus.ParametricIntervalIntegral
  {𝕜 : Type u_1} [RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {H : Type u_3} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {s : Set H} {a b : ℝ} {bound : ℝ → ℝ} {F : H → ℝ → E} {F' : H → ℝ → H →L[𝕜] E} {x₀ : H} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable (F' x₀) (μ.restrict (Set.uIoc a b))) (h_bound : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ∀ x ∈ s, ‖F' x t‖ ≤ bound t) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → ∀ x ∈ s, HasFDerivAt (fun x => F x t) (F' x t) x) : HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
• intervalIntegral.hasFDerivAt_integral_of_dominated_loc_of_lip 📋 Mathlib.Analysis.Calculus.ParametricIntervalIntegral
  {𝕜 : Type u_1} [RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace 𝕜 E] {H : Type u_3} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {s : Set H} {a b : ℝ} {bound : ℝ → ℝ} {F : H → ℝ → E} {F' : ℝ → H →L[𝕜] E} {x₀ : H} (hs : s ∈ nhds x₀) (hF_meas : ∀ᶠ (x : H) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) (hF_int : IntervalIntegrable (F x₀) μ a b) (hF'_meas : MeasureTheory.AEStronglyMeasurable F' (μ.restrict (Set.uIoc a b))) (h_lip : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) s) (bound_integrable : IntervalIntegrable bound μ a b) (h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Set.uIoc a b → HasFDerivAt (fun x => F x t) (F' t) x₀) : IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
• injOn_circleMap_of_abs_sub_le 📋 Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
  {a b R : ℝ} {c : ℂ} (h_R : R ≠ 0) : |a - b| ≤ 2 * Real.pi → Set.InjOn (circleMap c R) (Set.uIoc a b)
• MeasureTheory.intervalIntegral_integral_swap 📋 Mathlib.MeasureTheory.Integral.Prod
  {α : Type u_1} {E : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasureTheory.SFinite μ] {a b : ℝ} {f : ℝ → α → E} (h_int : MeasureTheory.Integrable (Function.uncurry f) ((MeasureTheory.volume.restrict (Set.uIoc a b)).prod μ)) : ∫ (x : ℝ) in a..b, ∫ (y : α), f x y ∂μ = ∫ (y : α), ∫ (x : ℝ) in a..b, f x y ∂μ
• MeasureTheory.intervalIntegral_intervalIntegral_swap 📋 Mathlib.MeasureTheory.Integral.Prod
  {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ → ℝ → E} {a b c d : ℝ} (h : MeasureTheory.IntegrableOn (Function.uncurry F) (Set.uIoc a b ×ˢ Set.uIoc c d) MeasureTheory.volume) : ∫ (x : ℝ) in a..b, ∫ (y : ℝ) in c..d, F x y = ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, F x y
• AbsolutelyContinuousOnInterval.uIoc_subset_of_mem_disjWithin 📋 Mathlib.MeasureTheory.Function.AbsolutelyContinuous
  {a b : ℝ} {n : ℕ} {I : ℕ → ℝ × ℝ} (hnI : (n, I) ∈ AbsolutelyContinuousOnInterval.disjWithin a b) {i : ℕ} (hi : i < n) : Set.uIoc (I i).1 (I i).2 ⊆ Set.uIoc a b
• AbsolutelyContinuousOnInterval.biUnion_uIoc_subset_of_mem_disjWithin 📋 Mathlib.MeasureTheory.Function.AbsolutelyContinuous
  {a b : ℝ} {n : ℕ} {I : ℕ → ℝ × ℝ} (hnI : (n, I) ∈ AbsolutelyContinuousOnInterval.disjWithin a b) : ⋃ i ∈ Finset.range n, Set.uIoc (I i).1 (I i).2 ⊆ Set.uIoc a b
• AbsolutelyContinuousOnInterval.tendsto_volume_totalLengthFilter_nhds_zero 📋 Mathlib.MeasureTheory.Function.AbsolutelyContinuous
  : Filter.Tendsto (fun E => MeasureTheory.volume (⋃ i ∈ Finset.range E.1, Set.uIoc (E.2 i).1 (E.2 i).2)) AbsolutelyContinuousOnInterval.totalLengthFilter (nhds 0)
• AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero 📋 Mathlib.MeasureTheory.Function.AbsolutelyContinuous
  (a b : ℝ) : Filter.Tendsto (fun E => (MeasureTheory.volume.restrict (Set.uIoc a b)) (⋃ i ∈ Finset.range E.1, Set.uIoc (E.2 i).1 (E.2 i).2)) (AbsolutelyContinuousOnInterval.totalLengthFilter ⊓ Filter.principal (AbsolutelyContinuousOnInterval.disjWithin a b)) (nhds 0)
• interval_average_symm 📋 Mathlib.MeasureTheory.Integral.IntervalAverage
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (a b : ℝ) : ⨍ (x : ℝ) in a..b, f x = ⨍ (x : ℝ) in b..a, f x
• interval_average_eq_div 📋 Mathlib.MeasureTheory.Integral.IntervalAverage
  (f : ℝ → ℝ) (a b : ℝ) : ⨍ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)
• exists_eq_interval_average 📋 Mathlib.MeasureTheory.Integral.IntervalAverage
  {f : ℝ → ℝ} {a b : ℝ} (hab : a ≠ b) (hf : ContinuousOn f (Set.uIcc a b)) : ∃ c ∈ Set.uIoo a b, f c = ⨍ (x : ℝ) in a..b, f x
• intervalAverage_congr_codiscreteWithin 📋 Mathlib.MeasureTheory.Integral.IntervalAverage
  {a b : ℝ} {f₁ f₂ : ℝ → ℝ} (hf : f₁ =ᶠ[Filter.codiscreteWithin (Set.uIoc a b)] f₂) : ⨍ (x : ℝ) in a..b, f₁ x = ⨍ (x : ℝ) in a..b, f₂ x
• exists_eq_interval_average_of_measure 📋 Mathlib.MeasureTheory.Integral.IntervalAverage
  {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : ContinuousOn f (Set.uIcc a b)) (hμfin : μ (Set.uIoc a b) ≠ ⊤) (hμ0 : μ (Set.uIoc a b) ≠ 0) : ∃ c ∈ Set.uIoc a b, f c = ⨍ (x : ℝ) in Set.uIoc a b, f x ∂μ
• exists_eq_interval_average_of_noAtoms 📋 Mathlib.MeasureTheory.Integral.IntervalAverage
  {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] (hf : ContinuousOn f (Set.uIcc a b)) (hμfin : μ (Set.uIoc a b) ≠ ⊤) (hμ0 : μ (Set.uIoc a b) ≠ 0) : ∃ c ∈ Set.uIoo a b, f c = ⨍ (x : ℝ) in Set.uIoc a b, f x ∂μ
• exists_eq_interval_average_of_nullSingletonClass 📋 Mathlib.MeasureTheory.Integral.IntervalAverage
  {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] (hf : ContinuousOn f (Set.uIcc a b)) (hμfin : μ (Set.uIoc a b) ≠ ⊤) (hμ0 : μ (Set.uIoc a b) ≠ 0) : ∃ c ∈ Set.uIoo a b, f c = ⨍ (x : ℝ) in Set.uIoc a b, f x ∂μ
• interval_average_eq 📋 Mathlib.MeasureTheory.Integral.IntervalAverage
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (a b : ℝ) : ⨍ (x : ℝ) in a..b, f x = (b - a)⁻¹ • ∫ (x : ℝ) in a..b, f x
• Real.circleAverage_eq_intervalAverage 📋 Mathlib.MeasureTheory.Integral.CircleAverage
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ} : Real.circleAverage f c R = ⨍ (θ : ℝ) in 0..2 * Real.pi, f (circleMap c R θ)
• integral_pow_abs_sub_uIoc 📋 Mathlib.Analysis.SpecialFunctions.Integrals.Basic
  {a b : ℝ} (n : ℕ) : ∫ (x : ℝ) in Set.uIoc a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)
• ValueDistribution.Cartan.integrableOn_cartanKernel 📋 Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation
  {f : ℂ → ℂ} {R : ℝ} (h : Meromorphic f) : MeasureTheory.IntegrableOn (fun p => ValueDistribution.Cartan.cartanKernel f R p.1 p.2) (Set.uIoc 0 (2 * Real.pi) ×ˢ Set.uIoc 0 (2 * Real.pi)) MeasureTheory.volume
• Frullani.norm_integral_inv_smul_sub_le 📋 Mathlib.Analysis.SpecialFunctions.FrullaniIntegral
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E] (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (ha : 0 < a) (hb : 0 < b) {V : E} {δ : ℝ} (hδ : 0 ≤ δ) (h : ∀ x ∈ Set.uIoc a b, ‖f x - V‖ ≤ δ) : ‖(∫ (x : ℝ) in a..b, x⁻¹ • f x) - Real.log (b / a) • V‖ ≤ δ * |Real.log (b / a)|
• Frullani.tendsto_integral_inv_smul_of_tendsto_uniform 📋 Mathlib.Analysis.SpecialFunctions.FrullaniIntegral
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E] (hf : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume) (ha : 0 < a) (hb : 0 < b) {F : Filter ℝ} (hpos : ∀ᶠ (t : ℝ) in F, 0 < t) {V : E} (huni : ∀ δ > 0, ∀ᶠ (t : ℝ) in F, ∀ x ∈ Set.uIoc (a * t) (b * t), ‖f x - V‖ ≤ δ) : Filter.Tendsto (fun t => ∫ (x : ℝ) in a * t..b * t, x⁻¹ • f x) F (nhds (Real.log (b / a) • V))
• unitInterval.volume_uIoc 📋 Mathlib.MeasureTheory.Constructions.UnitInterval
  (x y : ↑unitInterval) : MeasureTheory.volume (Set.uIoc x y) = edist y x
• curveIntegralFun_trans_aeeq_left 📋 Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c : E} (ω : E → E →L[𝕜] F) (γab : Path a b) (γbc : Path b c) : curveIntegralFun ω (γab.trans γbc) =ᵐ[MeasureTheory.volume.restrict (Set.uIoc 0 (1 / 2))] fun t => 2 • curveIntegralFun ω γab (2 * t)
• curveIntegralFun_trans_aeeq_right 📋 Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c : E} (ω : E → E →L[𝕜] F) (γab : Path a b) (γbc : Path b c) : curveIntegralFun ω (γab.trans γbc) =ᵐ[MeasureTheory.volume.restrict (Set.uIoc (1 / 2) 1)] fun t => 2 • curveIntegralFun ω γbc (2 * t - 1)
• exists_eq_const_mul_intervalIntegral_of_nonneg 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
  {a b : ℝ} {f g : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} (hf : ContinuousOn f (Set.uIcc a b)) (hg : IntervalIntegrable g μ a b) (hg0 : ∀ x ∈ Set.uIoc a b, 0 ≤ g x) : ∃ c ∈ Set.uIcc a b, ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ
• exists_eq_const_mul_intervalIntegral_of_ae_nonneg 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue
  {a b : ℝ} {f g : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} (hf : ContinuousOn f (Set.uIcc a b)) (hg : IntervalIntegrable g μ a b) (hg0 : ∀ᵐ (x : ℝ) ∂μ.restrict (Set.uIoc a b), 0 ≤ g x) : ∃ c ∈ Set.uIcc a b, ∫ (x : ℝ) in a..b, f x * g x ∂μ = f c * ∫ (x : ℝ) in a..b, g x ∂μ

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