Loogle!

Result

Found 306 declarations mentioning Set.uIcc. Of these, only the first 200 are shown.

Set.uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] (a b : α) : Set α
Set.nonempty_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a b : α} : (Set.uIcc a b).Nonempty
Set.uIcc_injective_left 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [DistribLattice α] (a : α) : Function.Injective (Set.uIcc a)
Set.uIcc_injective_right 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [DistribLattice α] (a : α) : Function.Injective fun b => Set.uIcc b a
Set.left_mem_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a b : α} : a ∈ Set.uIcc a b
Set.right_mem_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a b : α} : b ∈ Set.uIcc a b
Set.uIcc_comm 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] (a b : α) : Set.uIcc a b = Set.uIcc b a
Set.uIcc_self 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a : α} : Set.uIcc a a = {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.uIoo_subset_uIcc_self 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [LinearOrder α] {a b : α} : Set.uIoo a b ⊆ Set.uIcc a b
Set.Icc_subset_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a b : α} : Set.Icc a b ⊆ Set.uIcc a b
Set.Icc_subset_uIcc' 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a b : α} : Set.Icc b a ⊆ Set.uIcc a b
Set.uIcc_subset_uIcc_left 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a b x : α} (h : x ∈ Set.uIcc a b) : Set.uIcc a x ⊆ Set.uIcc a b
Set.uIcc_subset_uIcc_right 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a b x : α} (h : x ∈ Set.uIcc a b) : Set.uIcc x b ⊆ Set.uIcc a b
Set.uIcc_of_ge 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a b : α} (h : b ≤ a) : Set.uIcc a b = Set.Icc b a
Set.uIcc_of_gt 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a b : α} (h : b < a) : Set.uIcc a b = Set.Icc b a
Set.uIcc_of_le 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a b : α} (h : a ≤ b) : Set.uIcc a b = Set.Icc a b
Set.uIcc_of_lt 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a b : α} (h : a < b) : Set.uIcc a b = Set.Icc a b
Set.eq_of_mem_uIcc_of_mem_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [DistribLattice α] {a b c : α} (ha : a ∈ Set.uIcc b c) (hb : b ∈ Set.uIcc a c) : a = b
Set.eq_of_mem_uIcc_of_mem_uIcc' 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [DistribLattice α] {a b c : α} : b ∈ Set.uIcc a c → c ∈ Set.uIcc a b → b = c
Set.uIcc_subset_uIcc_union_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [LinearOrder α] {a b c : α} : Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c
Set.mem_uIcc_of_ge 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a b x : α} (hb : b ≤ x) (ha : x ≤ a) : x ∈ Set.uIcc a b
Set.mem_uIcc_of_le 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a b x : α} (ha : a ≤ x) (hb : x ≤ b) : x ∈ Set.uIcc 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.uIcc_subset_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ ∈ Set.uIcc a₂ b₂) (h₂ : b₁ ∈ Set.uIcc a₂ b₂) : Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂
Set.bdd_below_bdd_above_iff_subset_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] (s : Set α) : BddBelow s ∧ BddAbove s ↔ ∃ a b, s ⊆ Set.uIcc a b
Set.uIcc_subset_uIcc_iff_mem 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a₁ a₂ b₁ b₂ : α} : Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂ ↔ a₁ ∈ Set.uIcc a₂ b₂ ∧ b₁ ∈ Set.uIcc a₂ b₂
Set.uIcc_of_not_ge 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [LinearOrder α] {a b : α} (h : ¬b ≤ a) : Set.uIcc a b = Set.Icc a b
Set.uIcc_of_not_le 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [LinearOrder α] {a b : α} (h : ¬a ≤ b) : Set.uIcc a b = Set.Icc b a
Antitone.mapsTo_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : Antitone f) : Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
Monotone.mapsTo_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : Monotone f) : Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
Set.uIcc_eq_union 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [LinearOrder α] {a b : α} : Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a
Set.Icc_min_max 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [LinearOrder α] {a b : α} : Set.Icc (min a b) (max a b) = Set.uIcc a b
Set.uIcc_prod_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (a₁ a₂ : α) (b₁ b₂ : β) : Set.uIcc a₁ a₂ ×ˢ Set.uIcc b₁ b₂ = Set.uIcc (a₁, b₁) (a₂, b₂)
Antitone.image_uIcc_subset 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : Antitone f) : f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
Monotone.image_uIcc_subset 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : Monotone f) : f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
Set.notMem_uIcc_of_gt 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [LinearOrder α] {a b c : α} (ha : a < c) (hb : b < c) : c ∉ Set.uIcc a b
Set.notMem_uIcc_of_lt 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [LinearOrder α] {a b c : α} (ha : c < a) (hb : c < b) : c ∉ Set.uIcc a b
AntitoneOn.mapsTo_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : AntitoneOn f (Set.uIcc a b)) : Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
MonotoneOn.mapsTo_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : MonotoneOn f (Set.uIcc a b)) : Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
Set.uIcc_prod_eq 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (a b : α × β) : Set.uIcc a b = Set.uIcc a.1 b.1 ×ˢ Set.uIcc a.2 b.2
Set.uIcc_subset_Icc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ∈ Set.Icc a₂ b₂) (hb : b₁ ∈ Set.Icc a₂ b₂) : Set.uIcc a₁ b₁ ⊆ Set.Icc a₂ b₂
AntitoneOn.image_uIcc_subset 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : AntitoneOn f (Set.uIcc a b)) : f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
MonotoneOn.image_uIcc_subset 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] {f : α → β} {a b : α} (hf : MonotoneOn f (Set.uIcc a b)) : f '' Set.uIcc a b ⊆ Set.uIcc (f a) (f b)
Set.uIcc_subset_uIcc_iff_le' 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] {a₁ a₂ b₁ b₂ : α} : Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂ ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂
Set.mem_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [LinearOrder α] {a b c : α} : a ∈ Set.uIcc b c ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b
Set.uIcc_toDual 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] (a b : α) : Set.uIcc (OrderDual.toDual a) (OrderDual.toDual b) = ⇑OrderDual.ofDual ⁻¹' Set.uIcc a b
Set.uIcc_ofDual 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [Lattice α] (a b : αᵒᵈ) : Set.uIcc (OrderDual.ofDual a) (OrderDual.ofDual b) = ⇑OrderDual.toDual ⁻¹' Set.uIcc a b
Set.monotone_or_antitone_iff_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} : Monotone f ∨ Antitone f ↔ ∀ (a b c : α), c ∈ Set.uIcc a b → f c ∈ Set.uIcc (f a) (f b)
Set.uIcc_subset_uIcc_iff_le 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} [LinearOrder α] {a₁ a₂ b₁ b₂ : α} : Set.uIcc a₁ b₁ ⊆ Set.uIcc a₂ b₂ ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂
Set.monotoneOn_or_antitoneOn_iff_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} : MonotoneOn f s ∨ AntitoneOn f s ↔ ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ Set.uIcc a b → f c ∈ Set.uIcc (f a) (f b)
OrderEmbedding.preimage_uIcc 📋 Mathlib.Order.Interval.Set.OrderEmbedding
{α : Type u_1} {β : Type u_2} [LinearOrder α] [Lattice β] (e : α ↪o β) (x y : α) : ⇑e ⁻¹' Set.uIcc (e x) (e y) = Set.uIcc x y
Set.ordConnected_uIcc 📋 Mathlib.Order.Interval.Set.OrdConnected
{α : Type u_1} [LinearOrder α] {a b : α} : (Set.uIcc a b).OrdConnected
Set.ordConnected_of_uIcc_subset_left 📋 Mathlib.Order.Interval.Set.OrdConnected
{α : Type u_1} [LinearOrder α] {s : Set α} {x : α} (h : ∀ y ∈ s, Set.uIcc x y ⊆ s) : s.OrdConnected
Set.OrdConnected.uIcc_subset 📋 Mathlib.Order.Interval.Set.OrdConnected
{α : Type u_1} [LinearOrder α] {s : Set α} (hs : s.OrdConnected) ⦃x : α⦄ (hx : x ∈ s) ⦃y : α⦄ (hy : y ∈ s) : Set.uIcc x y ⊆ s
Set.ordConnected_iff_uIcc_subset 📋 Mathlib.Order.Interval.Set.OrdConnected
{α : Type u_1} [LinearOrder α] {s : Set α} : s.OrdConnected ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.uIcc x y ⊆ s
Set.ordConnected_iff_uIcc_subset_left 📋 Mathlib.Order.Interval.Set.OrdConnected
{α : Type u_1} [LinearOrder α] {s : Set α} {x : α} (hx : x ∈ s) : s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → Set.uIcc x y ⊆ s
Set.ordConnected_iff_uIcc_subset_right 📋 Mathlib.Order.Interval.Set.OrdConnected
{α : Type u_1} [LinearOrder α] {s : Set α} {x : α} (hx : x ∈ s) : s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → Set.uIcc y x ⊆ s
Set.image_subtype_val_uIcc 📋 Mathlib.Order.Interval.Set.OrdConnected
{α : Type u_1} [LinearOrder α] {s : Set α} [s.OrdConnected] (a b : ↑s) : Subtype.val '' Set.uIcc a b = Set.uIcc ↑a ↑b
Rat.preimage_cast_uIcc 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) : Rat.cast ⁻¹' Set.uIcc ↑p ↑q = Set.uIcc p q
NNRat.preimage_cast_uIcc 📋 Mathlib.Data.Rat.Cast.Order
{K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0) : NNRat.cast ⁻¹' Set.uIcc ↑p ↑q = Set.uIcc p q
Set.finite_uIcc 📋 Mathlib.Order.Interval.Finset.Defs
{α : Type u_1} [Lattice α] [LocallyFiniteOrder α] (a b : α) : (Set.uIcc a b).Finite
Set.fintypeUIcc 📋 Mathlib.Order.Interval.Finset.Defs
{α : Type u_1} [Lattice α] [LocallyFiniteOrder α] (a b : α) : Fintype ↑(Set.uIcc a b)
Finset.coe_uIcc 📋 Mathlib.Order.Interval.Finset.Defs
{α : Type u_1} [Lattice α] [LocallyFiniteOrder α] (a b : α) : ↑(Finset.uIcc a b) = Set.uIcc a b
Fintype.card_uIcc 📋 Mathlib.Order.Interval.Finset.Defs
{α : Type u_1} [Lattice α] [LocallyFiniteOrder α] (a b : α) [Fintype ↑(Set.uIcc a b)] : Fintype.card ↑(Set.uIcc a b) = (Finset.uIcc a b).card
Fin.image_val_uIcc 📋 Mathlib.Order.Interval.Set.Fin
{n : ℕ} (i j : Fin n) : Fin.val '' Set.uIcc i j = Set.uIcc ↑i ↑j
Fin.preimage_val_uIcc_val 📋 Mathlib.Order.Interval.Set.Fin
{n : ℕ} (i j : Fin n) : Fin.val ⁻¹' Set.uIcc ↑i ↑j = Set.uIcc i j
Fin.preimage_rev_uIcc 📋 Mathlib.Order.Interval.Set.Fin
{n : ℕ} (i j : Fin n) : Fin.rev ⁻¹' Set.uIcc i j = Set.uIcc i.rev j.rev
Fin.image_castLE_uIcc 📋 Mathlib.Order.Interval.Set.Fin
{m n : ℕ} (i j : Fin m) (h : m ≤ n) : Fin.castLE h '' Set.uIcc i j = Set.uIcc (Fin.castLE h i) (Fin.castLE h j)
Fin.preimage_castLE_uIcc_castLE 📋 Mathlib.Order.Interval.Set.Fin
{m n : ℕ} (i j : Fin m) (h : m ≤ n) : Fin.castLE h ⁻¹' Set.uIcc (Fin.castLE h i) (Fin.castLE h j) = Set.uIcc i j
Fin.preimage_cast_uIcc 📋 Mathlib.Order.Interval.Set.Fin
{m n : ℕ} (h : m = n) (i j : Fin n) : Fin.cast h ⁻¹' Set.uIcc i j = Set.uIcc (Fin.cast ⋯ i) (Fin.cast ⋯ j)
Fin.preimage_castAdd_uIcc_castAdd 📋 Mathlib.Order.Interval.Set.Fin
{n : ℕ} (m : ℕ) (i j : Fin n) : Fin.castAdd m ⁻¹' Set.uIcc (Fin.castAdd m i) (Fin.castAdd m j) = Set.uIcc i j
Fin.preimage_natAdd_uIcc_natAdd 📋 Mathlib.Order.Interval.Set.Fin
{n : ℕ} (m : ℕ) (i j : Fin n) : Fin.natAdd m ⁻¹' Set.uIcc (Fin.natAdd m i) (Fin.natAdd m j) = Set.uIcc i j
Fin.preimage_addNat_uIcc_addNat 📋 Mathlib.Order.Interval.Set.Fin
{n : ℕ} (m : ℕ) (i j : Fin n) : (fun x => x.addNat m) ⁻¹' Set.uIcc (i.addNat m) (j.addNat m) = Set.uIcc i j
Fin.image_castAdd_uIcc 📋 Mathlib.Order.Interval.Set.Fin
{n : ℕ} (m : ℕ) (i j : Fin n) : Fin.castAdd m '' Set.uIcc i j = Set.uIcc (Fin.castAdd m i) (Fin.castAdd m j)
Fin.image_natAdd_uIcc 📋 Mathlib.Order.Interval.Set.Fin
{n : ℕ} (m : ℕ) (i j : Fin n) : Fin.natAdd m '' Set.uIcc i j = Set.uIcc (Fin.natAdd m i) (Fin.natAdd m j)
Fin.preimage_castSucc_uIcc_castSucc 📋 Mathlib.Order.Interval.Set.Fin
{n : ℕ} (i j : Fin n) : Fin.castSucc ⁻¹' Set.uIcc i.castSucc j.castSucc = Set.uIcc i j
Fin.preimage_succ_uIcc_succ 📋 Mathlib.Order.Interval.Set.Fin
{n : ℕ} (i j : Fin n) : Fin.succ ⁻¹' Set.uIcc i.succ j.succ = Set.uIcc i j
Fin.image_addNat_uIcc 📋 Mathlib.Order.Interval.Set.Fin
{n : ℕ} (m : ℕ) (i j : Fin n) : (fun x => x.addNat m) '' Set.uIcc i j = Set.uIcc (i.addNat m) (j.addNat m)
Fin.image_castSucc_uIcc 📋 Mathlib.Order.Interval.Set.Fin
{n : ℕ} (i j : Fin n) : Fin.castSucc '' Set.uIcc i j = Set.uIcc i.castSucc j.castSucc
Fin.image_succ_uIcc 📋 Mathlib.Order.Interval.Set.Fin
{n : ℕ} (i j : Fin n) : Fin.succ '' Set.uIcc i j = Set.uIcc i.succ j.succ
Set.image_neg_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b : α) : Neg.neg '' Set.uIcc a b = Set.uIcc (-a) (-b)
Set.inv_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] (a b : α) : (Set.uIcc a b)⁻¹ = Set.uIcc a⁻¹ b⁻¹
Set.neg_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b : α) : -Set.uIcc a b = Set.uIcc (-a) (-b)
Set.image_const_sub_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b c : α) : (fun x => a - x) '' Set.uIcc b c = Set.uIcc (a - b) (a - c)
Set.image_sub_const_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b c : α) : (fun x => x - a) '' Set.uIcc b c = Set.uIcc (b - a) (c - a)
Set.preimage_const_sub_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b c : α) : (fun x => a - x) ⁻¹' Set.uIcc b c = Set.uIcc (a - b) (a - c)
Set.image_div_const_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a b c : α) : (fun x => x / a) '' Set.uIcc b c = Set.uIcc (b / a) (c / a)
Set.preimage_add_const_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b c : α) : (fun x => x + a) ⁻¹' Set.uIcc b c = Set.uIcc (b - a) (c - a)
Set.preimage_const_add_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b c : α) : (fun x => a + x) ⁻¹' Set.uIcc b c = Set.uIcc (b - a) (c - a)
Set.preimage_sub_const_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b c : α) : (fun x => x - a) ⁻¹' Set.uIcc b c = Set.uIcc (b + a) (c + a)
Set.image_add_const_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b c : α) : (fun x => x + a) '' Set.uIcc b c = Set.uIcc (b + a) (c + a)
Set.image_const_add_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b c : α) : (fun x => a + x) '' Set.uIcc b c = Set.uIcc (a + b) (a + c)
Set.abs_sub_left_of_mem_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b c : α} (h : c ∈ Set.uIcc a b) : |c - a| ≤ |b - a|
Set.abs_sub_right_of_mem_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b c : α} (h : c ∈ Set.uIcc a b) : |b - c| ≤ |b - a|
Set.image_const_mul_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a b c : α) : (fun x => a * x) '' Set.uIcc b c = Set.uIcc (a * b) (a * c)
Set.image_mul_const_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a b c : α) : (fun x => x * a) '' Set.uIcc b c = Set.uIcc (b * a) (c * a)
Set.abs_sub_le_of_uIcc_subset_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b c d : α} (h : Set.uIcc c d ⊆ Set.uIcc a b) : |d - c| ≤ |b - a|
Set.preimage_const_mul_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (ha : a ≠ 0) (b c : α) : (fun x => a * x) ⁻¹' Set.uIcc b c = Set.uIcc (b / a) (c / a)
Set.preimage_mul_const_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (ha : a ≠ 0) (b c : α) : (fun x => x * a) ⁻¹' Set.uIcc b c = Set.uIcc (b / a) (c / a)
Set.preimage_div_const_uIcc 📋 Mathlib.Algebra.Order.Group.Pointwise.Interval
{α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {a : α} (ha : a ≠ 0) (b c : α) : (fun x => x / a) ⁻¹' Set.uIcc b c = Set.uIcc (b * a) (c * a)
Filter.tendsto_uIcc_of_Icc 📋 Mathlib.Order.Filter.Interval
{α : Type u_1} [LinearOrder α] {l : Filter α} [Filter.TendstoIxxClass Set.Icc l l] : Filter.TendstoIxxClass Set.uIcc l l
Filter.tendsto_Icc_uIcc_uIcc 📋 Mathlib.Order.Filter.Interval
{α : Type u_1} [LinearOrder α] {a b : α} : Filter.TendstoIxxClass Set.Icc (Filter.principal (Set.uIcc a b)) (Filter.principal (Set.uIcc a b))
Filter.tendsto_Ioc_uIcc_uIcc 📋 Mathlib.Order.Filter.Interval
{α : Type u_1} [LinearOrder α] {a b : α} : Filter.TendstoIxxClass Set.Ioc (Filter.principal (Set.uIcc a b)) (Filter.principal (Set.uIcc a b))
Filter.Tendsto.uIcc 📋 Mathlib.Order.Filter.Interval
{α : Type u_1} {β : Type u_2} [LinearOrder α] {l : Filter α} [Filter.TendstoIxxClass Set.Icc l l] {f g : β → α} {lb : Filter β} (hf : Filter.Tendsto f lb l) (hg : Filter.Tendsto g lb l) : Filter.Tendsto (fun x => Set.uIcc (f x) (g x)) lb l.smallSets
Set.pi_univ_uIcc 📋 Mathlib.Order.Interval.Set.Pi
{ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] (a b : (i : ι) → α i) : (Set.univ.pi fun i => Set.uIcc (a i) (b i)) = Set.uIcc a b
Set.image_update_uIcc_left 📋 Mathlib.Order.Interval.Set.Pi
{ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] (f : (i : ι) → α i) (i : ι) (a : α i) : Function.update f i '' Set.uIcc a (f i) = Set.uIcc (Function.update f i a) f
Set.image_update_uIcc_right 📋 Mathlib.Order.Interval.Set.Pi
{ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] (f : (i : ι) → α i) (i : ι) (b : α i) : Function.update f i '' Set.uIcc (f i) b = Set.uIcc f (Function.update f i b)
Set.image_update_uIcc 📋 Mathlib.Order.Interval.Set.Pi
{ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] (f : (i : ι) → α i) (i : ι) (a b : α i) : Function.update f i '' Set.uIcc a b = Set.uIcc (Function.update f i a) (Function.update f i b)
Set.image_mulSingle_uIcc 📋 Mathlib.Order.Interval.Set.Pi
{ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] [(i : ι) → One (α i)] (i : ι) (a b : α i) : Pi.mulSingle i '' Set.uIcc a b = Set.uIcc (Pi.mulSingle i a) (Pi.mulSingle i b)
Set.image_single_uIcc 📋 Mathlib.Order.Interval.Set.Pi
{ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] [(i : ι) → Zero (α i)] (i : ι) (a b : α i) : Pi.single i '' Set.uIcc a b = Set.uIcc (Pi.single i a) (Pi.single i b)
Set.image_mulSingle_uIcc_left 📋 Mathlib.Order.Interval.Set.Pi
{ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] [(i : ι) → One (α i)] (i : ι) (a : α i) : Pi.mulSingle i '' Set.uIcc a 1 = Set.uIcc (Pi.mulSingle i a) 1
Set.image_mulSingle_uIcc_right 📋 Mathlib.Order.Interval.Set.Pi
{ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] [(i : ι) → One (α i)] (i : ι) (b : α i) : Pi.mulSingle i '' Set.uIcc 1 b = Set.uIcc 1 (Pi.mulSingle i b)
Set.image_single_uIcc_left 📋 Mathlib.Order.Interval.Set.Pi
{ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] [(i : ι) → Zero (α i)] (i : ι) (a : α i) : Pi.single i '' Set.uIcc a 0 = Set.uIcc (Pi.single i a) 0
Set.image_single_uIcc_right 📋 Mathlib.Order.Interval.Set.Pi
{ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Lattice (α i)] [DecidableEq ι] [(i : ι) → Zero (α i)] (i : ι) (b : α i) : Pi.single i '' Set.uIcc 0 b = Set.uIcc 0 (Pi.single i b)
Function.Periodic.image_uIcc 📋 Mathlib.Algebra.Field.Periodic
{α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] (h : Function.Periodic f c) (hc : c ≠ 0) (a : α) : f '' Set.uIcc a (a + c) = Set.range f
ENNReal.image_coe_uIcc 📋 Mathlib.Basic.ENNReal.Operations
(x y : NNReal) : ENNReal.ofNNReal '' Set.uIcc x y = Set.uIcc ↑x ↑y
Set.mem_ordConnectedComponent 📋 Mathlib.Order.Interval.Set.OrdConnectedComponent
{α : Type u_1} [LinearOrder α] {s : Set α} {x y : α} : y ∈ s.ordConnectedComponent x ↔ Set.uIcc x y ⊆ s
Set.ordConnectedComponent_eq 📋 Mathlib.Order.Interval.Set.OrdConnectedComponent
{α : Type u_1} [LinearOrder α] {s : Set α} {x y : α} (h : Set.uIcc x y ⊆ s) : s.ordConnectedComponent x = s.ordConnectedComponent y
Set.eq_of_mem_ordConnectedSection_of_uIcc_subset 📋 Mathlib.Order.Interval.Set.OrdConnectedComponent
{α : Type u_1} [LinearOrder α] {s : Set α} {x y : α} (hx : x ∈ s.ordConnectedSection) (hy : y ∈ s.ordConnectedSection) (h : Set.uIcc x y ⊆ s) : x = y
Set.ordConnectedProj_eq 📋 Mathlib.Order.Interval.Set.OrdConnectedComponent
{α : Type u_1} [LinearOrder α] {s : Set α} {x y : ↑s} : s.ordConnectedProj x = s.ordConnectedProj y ↔ Set.uIcc ↑x ↑y ⊆ s
NNReal.image_coe_uIcc 📋 Mathlib.Basic.NNReal.Basic
(x y : NNReal) : NNReal.toReal '' Set.uIcc x y = Set.uIcc ↑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
closure_uIoo 📋 Mathlib.Topology.Order.DenselyOrdered
{α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} (hab : a ≠ b) : closure (Set.uIoo a b) = Set.uIcc a b
isPreconnected_uIcc 📋 Mathlib.Topology.Order.IntermediateValue
{α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} : IsPreconnected (Set.uIcc a b)
exists_mem_uIcc_isFixedPt_of_mapsTo 📋 Mathlib.Topology.Order.IntermediateValue
{α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} {f : α → α} (hf : ContinuousOn f (Set.uIcc a b)) (hmaps : Set.MapsTo f (Set.uIcc a b) (Set.uIcc a b)) : ∃ c ∈ Set.uIcc a b, Function.IsFixedPt f c
exists_mem_uIcc_isFixedPt_of_surjOn 📋 Mathlib.Topology.Order.IntermediateValue
{α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} {f : α → α} (hf : ContinuousOn f (Set.uIcc a b)) (h_surj : Set.SurjOn f (Set.uIcc a b) (Set.uIcc a b)) : ∃ c ∈ Set.uIcc a b, Function.IsFixedPt f c
intermediate_value_uIcc 📋 Mathlib.Topology.Order.IntermediateValue
{α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hf : ContinuousOn f (Set.uIcc a b)) : Set.uIcc (f a) (f b) ⊆ f '' Set.uIcc a b
ContinuousOn.surjOn_uIcc 📋 Mathlib.Topology.Order.IntermediateValue
{α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {s : Set α} [hs : s.OrdConnected] {f : α → δ} (hf : ContinuousOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : Set.SurjOn f s (Set.uIcc (f a) (f b))
exists_mem_uIcc_isFixedPt 📋 Mathlib.Topology.Order.IntermediateValue
{α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α} {f : α → α} (hf : ContinuousOn f (Set.uIcc a b)) (ha : a ≤ f a) (hb : f b ≤ b) : ∃ c ∈ Set.uIcc a b, Function.IsFixedPt f c
ContinuousOn.image_uIcc_of_antitoneOn 📋 Mathlib.Topology.Order.IntermediateValue
{α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hf : ContinuousOn f (Set.uIcc a b)) (hmono : AntitoneOn f (Set.uIcc a b)) : f '' Set.uIcc a b = Set.uIcc (f a) (f b)
ContinuousOn.image_uIcc_of_monotoneOn 📋 Mathlib.Topology.Order.IntermediateValue
{α : Type u} [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} {f : α → δ} (hf : ContinuousOn f (Set.uIcc a b)) (hmono : MonotoneOn f (Set.uIcc a b)) : f '' Set.uIcc a b = Set.uIcc (f a) (f b)
isCompact_uIcc 📋 Mathlib.Topology.Order.Compact
{α : Type u_2} [LinearOrder α] [TopologicalSpace α] [CompactIccSpace α] {a b : α} : IsCompact (Set.uIcc a b)
ContinuousOn.image_uIcc 📋 Mathlib.Topology.Order.Compact
{α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] [DenselyOrdered α] [ConditionallyCompleteLinearOrder β] [OrderTopology β] {f : α → β} {a b : α} (h : ContinuousOn f (Set.uIcc a b)) : f '' Set.uIcc a b = Set.uIcc (sInf (f '' Set.uIcc a b)) (sSup (f '' Set.uIcc a b))
ContinuousOn.image_uIcc_eq_Icc 📋 Mathlib.Topology.Order.Compact
{α : Type u_2} {β : Type u_3} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β] [DenselyOrdered α] [ConditionallyCompleteLinearOrder β] [OrderTopology β] {f : α → β} {a b : α} (h : ContinuousOn f (Set.uIcc a b)) : f '' Set.uIcc a b = Set.Icc (sInf (f '' Set.uIcc a b)) (sSup (f '' Set.uIcc a b))
Real.dist_left_le_of_mem_uIcc 📋 Mathlib.Topology.MetricSpace.Pseudo.Real
{x y z : ℝ} (h : y ∈ Set.uIcc x z) : dist x y ≤ dist x z
Real.dist_right_le_of_mem_uIcc 📋 Mathlib.Topology.MetricSpace.Pseudo.Real
{x y z : ℝ} (h : y ∈ Set.uIcc x z) : dist y z ≤ dist x z
Real.dist_le_of_mem_uIcc 📋 Mathlib.Topology.MetricSpace.Pseudo.Real
{x y x' y' : ℝ} (hx : x ∈ Set.uIcc x' y') (hy : y ∈ Set.uIcc x' y') : dist x y ≤ dist x' y'
measurableSet_uIcc 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
{α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] {a b : α} [OrderClosedTopology α] : MeasurableSet (Set.uIcc a b)
nhdsWithin_uIcc_isMeasurablyGenerated 📋 Mathlib.MeasureTheory.Constructions.BorelSpace.Order
{α : Type u_1} [TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [LinearOrder α] {a b x : α} [OrderClosedTopology α] : (nhdsWithin x (Set.uIcc a b)).IsMeasurablyGenerated
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
Complex.horizontalSegment_eq 📋 Mathlib.Basic.Complex.Basic
(a₁ a₂ b : ℝ) : (fun x => ↑x + ↑b * Complex.I) '' Set.uIcc a₁ a₂ = Set.uIcc a₁ a₂ ×ℂ {b}
Complex.verticalSegment_eq 📋 Mathlib.Basic.Complex.Basic
(a b₁ b₂ : ℝ) : (fun y => ↑a + ↑y * Complex.I) '' Set.uIcc b₁ b₂ = {a} ×ℂ Set.uIcc b₁ b₂
Real.image_exp_uIcc 📋 Mathlib.Analysis.SpecialFunctions.Exp
(a b : ℝ) : Real.exp '' Set.uIcc a b = Set.uIcc (Real.exp a) (Real.exp b)
Real.image_log_uIcc 📋 Mathlib.Analysis.SpecialFunctions.Log.Basic
{a b : ℝ} (ha : 0 < a) (hb : 0 < b) : Real.log '' Set.uIcc a b = Set.uIcc (Real.log a) (Real.log b)
AffineMap.image_uIcc 📋 Mathlib.LinearAlgebra.AffineSpace.AffineMap
{k : Type u_10} [Field k] [LinearOrder k] [IsStrictOrderedRing k] (f : k →ᵃ[k] k) (a b : k) : ⇑f '' Set.uIcc a b = Set.uIcc (f a) (f b)
segment_eq_uIcc 📋 Mathlib.Analysis.Convex.Segment
{𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (x y : 𝕜) : segment 𝕜 x y = Set.uIcc x y
segment_subset_uIcc 📋 Mathlib.Analysis.Convex.Segment
{𝕜 : Type u_1} {E : Type u_2} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [LinearOrder E] [IsOrderedAddMonoid E] [Module 𝕜 E] [PosSMulMono 𝕜 E] (x y : E) : segment 𝕜 x y ⊆ Set.uIcc x y
Nonneg.segment_eq_uIcc 📋 Mathlib.Analysis.Convex.Segment
{𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : Nonneg 𝕜} : segment (Nonneg 𝕜) x y = Set.uIcc x y
convex_uIcc 📋 Mathlib.Analysis.Convex.Basic
{𝕜 : Type u_1} {β : Type u_4} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid β] [LinearOrder β] [IsOrderedAddMonoid β] [Module 𝕜 β] [PosSMulMono 𝕜 β] (r s : β) : Convex 𝕜 (Set.uIcc r s)
strictConvex_uIcc 📋 Mathlib.Analysis.Convex.Strict
{𝕜 : Type u_1} {β : Type u_5} [Semiring 𝕜] [PartialOrder 𝕜] [TopologicalSpace β] [AddCommMonoid β] [LinearOrder β] [IsOrderedCancelAddMonoid β] [OrderTopology β] [Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β) : StrictConvex 𝕜 (Set.uIcc r s)
Continuous.integrableOn_uIcc 📋 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.uIcc a b) μ
ContinuousOn.integrableOn_uIcc 📋 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 : ContinuousOn f (Set.uIcc a b)) : MeasureTheory.IntegrableOn f (Set.uIcc a b) μ
parallelepiped_single 📋 Mathlib.MeasureTheory.Measure.Haar.OfBasis
{ι : Type u_1} [Fintype ι] [DecidableEq ι] (a : ι → ℝ) : (parallelepiped fun i => Pi.single i (a i)) = Set.uIcc 0 a
Real.volume_real_interval 📋 Mathlib.MeasureTheory.Measure.Lebesgue.Basic
{a b : ℝ} : MeasureTheory.volume.real (Set.uIcc a b) = |b - a|
Real.volume_interval 📋 Mathlib.MeasureTheory.Measure.Lebesgue.Basic
{a b : ℝ} : MeasureTheory.volume (Set.uIcc a b) = ENNReal.ofReal |b - a|
uniqueDiffOn_uIcc 📋 Mathlib.Analysis.Calculus.TangentCone.Real
{a b : ℝ} (hab : a ≠ b) : UniqueDiffOn ℝ (Set.uIcc a b)
MeasureTheory.IntegrableOn.intervalIntegrable 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
{ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} (hf : MeasureTheory.IntegrableOn f (Set.uIcc a b) μ) : IntervalIntegrable f μ 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) (h : Set.uIcc c d ⊆ Set.uIcc a b) : IntervalIntegrable f μ c d
intervalIntegral.integral_congr 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
{E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} {μ : MeasureTheory.Measure ℝ} {a b : ℝ} (h : Set.EqOn f g (Set.uIcc a b)) : ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
IntervalIntegrable.trans_iff 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
{ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : ℝ → ε} {a b c : ℝ} {μ : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε] (h : b ∈ Set.uIcc a c) : IntervalIntegrable f μ a c ↔ IntervalIntegrable f μ a b ∧ IntervalIntegrable f μ b c
ContinuousOn.intervalIntegrable 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
{E : Type u_5} [NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {u : ℝ → E} {a b : ℝ} (hu : ContinuousOn u (Set.uIcc a b)) : IntervalIntegrable u μ a b
IntervalIntegrable.mono 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
{ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] {f : ℝ → ε} {a b c d : ℝ} {μ ν : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε] (hf : IntervalIntegrable f ν a b) (h1 : Set.uIcc c d ⊆ Set.uIcc a b) (h2 : μ ≤ ν) : IntervalIntegrable f μ c d
intervalIntegrable_iff' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
{ε : Type u_3} [TopologicalSpace ε] [ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] (h : ‖f (min a b)‖ₑ ≠ ⊤ := by finiteness) : IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.uIcc a b) μ
AntitoneOn.intervalIntegrable 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
{E : Type u_5} [NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] [ConditionallyCompleteLinearOrder E] [OrderTopology E] [SecondCountableTopology E] {u : ℝ → E} {a b : ℝ} (hu : AntitoneOn u (Set.uIcc a b)) : IntervalIntegrable u μ a b
MonotoneOn.intervalIntegrable 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
{E : Type u_5} [NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] [ConditionallyCompleteLinearOrder E] [OrderTopology E] [SecondCountableTopology E] {u : ℝ → E} {a b : ℝ} (hu : MonotoneOn u (Set.uIcc a b)) : IntervalIntegrable u μ a b
IntervalIntegrable.continuousOn_mul 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
{A : Type u_7} [NormedRing A] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f g : ℝ → A} (hf : IntervalIntegrable f μ a b) (hg : ContinuousOn g (Set.uIcc a b)) : IntervalIntegrable (fun x => g x * f x) μ a b
IntervalIntegrable.mul_continuousOn 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
{A : Type u_7} [NormedRing A] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f g : ℝ → A} (hf : IntervalIntegrable f μ a b) (hg : ContinuousOn g (Set.uIcc a b)) : IntervalIntegrable (fun x => f x * g x) μ a b
IntervalIntegrable.continuousOn_smul 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
{𝕜 : Type u_2} {E : Type u_5} [NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → 𝕜} {g : ℝ → E} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (hg : IntervalIntegrable g μ a b) (hf : ContinuousOn f (Set.uIcc a b)) : IntervalIntegrable (fun x => f x • g x) μ a b
IntervalIntegrable.smul_continuousOn 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
{𝕜 : Type u_2} {E : Type u_5} [NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → 𝕜} {g : ℝ → E} [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] (hf : IntervalIntegrable f μ a b) (hg : ContinuousOn g (Set.uIcc a b)) : IntervalIntegrable (fun x => f x • g x) μ a b
intervalIntegral.continuousOn_primitive_interval 📋 Mathlib.MeasureTheory.Integral.DominatedConvergence
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [MeasureTheory.NullSingletonClass μ] (h_int : MeasureTheory.IntegrableOn f (Set.uIcc a b) μ) : ContinuousOn (fun x => ∫ (t : ℝ) in a..x, f t ∂μ) (Set.uIcc a b)
intervalIntegral.continuousOn_primitive_interval_left 📋 Mathlib.MeasureTheory.Integral.DominatedConvergence
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [MeasureTheory.NullSingletonClass μ] (h_int : MeasureTheory.IntegrableOn f (Set.uIcc a b) μ) : ContinuousOn (fun x => ∫ (t : ℝ) in x..b, f t ∂μ) (Set.uIcc a b)
intervalIntegral.continuousOn_primitive_interval' 📋 Mathlib.MeasureTheory.Integral.DominatedConvergence
{E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b₁ b₂ : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [MeasureTheory.NullSingletonClass μ] (h_int : IntervalIntegrable f μ b₁ b₂) (ha : a ∈ Set.uIcc b₁ b₂) : ContinuousOn (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Set.uIcc b₁ b₂)
TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn 📋 Mathlib.MeasureTheory.Integral.DominatedConvergence
{ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated] {F : ι → ℝ → E} [MeasureTheory.IsLocallyFiniteMeasure μ] (hF : ∀ᶠ (i : ι) in l, ContinuousOn (F i) (Set.uIcc a b)) (h_lim : TendstoUniformlyOn F f l (Set.uIcc a b)) : Filter.Tendsto (fun n => ∫ (x : ℝ) in a..b, F n x ∂μ) l (nhds (∫ (x : ℝ) in a..b, f x ∂μ))
intervalIntegral.hasSum_intervalIntegral_of_summable_norm 📋 Mathlib.MeasureTheory.Integral.DominatedConvergence
{ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [Countable ι] {f : ι → C(ℝ, E)} (hf_sum : Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := Set.uIcc a b, isCompact' := ⋯ }) (f i)‖) : HasSum (fun i => ∫ (x : ℝ) in a..b, (f i) x) (∫ (x : ℝ) in a..b, ∑' (i : ι), (f i) x)
intervalIntegral.tsum_intervalIntegral_eq_of_summable_norm 📋 Mathlib.MeasureTheory.Integral.DominatedConvergence
{ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [Countable ι] {f : ι → C(ℝ, E)} (hf_sum : Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := Set.uIcc a b, isCompact' := ⋯ }) (f i)‖) : ∑' (i : ι), ∫ (x : ℝ) in a..b, (f i) x = ∫ (x : ℝ) in a..b, ∑' (i : ι), (f i) x
continuousOn_uIcc_extendFrom_uIoo 📋 Mathlib.Topology.Order.ExtendFrom
{α : Type u_1} {β : Type u_2} [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α] [OrderTopology α] [TopologicalSpace β] {f : α → β} {a b : α} {la lb : β} [RegularSpace β] (hf : ContinuousOn f (Set.uIoo a b)) (ha : Filter.Tendsto f (nhdsWithin a (Set.uIoo a b)) (nhds la)) (hb : Filter.Tendsto f (nhdsWithin b (Set.uIoo a b)) (nhds lb)) : ContinuousOn (extendFrom (Set.uIoo a b) f) (Set.uIcc a b)
exists_isLocalExtr_uIoo 📋 Mathlib.Topology.Order.Rolle
{X : Type u_1} {Y : Type u_2} [ConditionallyCompleteLinearOrder X] [DenselyOrdered X] [TopologicalSpace X] [OrderTopology X] [LinearOrder Y] [TopologicalSpace Y] [OrderTopology Y] {f : X → Y} {a b : X} (hab : a ≠ b) (hfc : ContinuousOn f (Set.uIcc a b)) (hfI : f a = f b) : ∃ c ∈ Set.uIoo a b, IsLocalExtr f c
exists_uIoo_isExtrOn_uIcc 📋 Mathlib.Topology.Order.Rolle
{X : Type u_1} {Y : Type u_2} [ConditionallyCompleteLinearOrder X] [DenselyOrdered X] [TopologicalSpace X] [OrderTopology X] [LinearOrder Y] [TopologicalSpace Y] [OrderTopology Y] {f : X → Y} {a b : X} (hab : a ≠ b) (hfc : ContinuousOn f (Set.uIcc a b)) (hfI : f a = f b) : ∃ c ∈ Set.uIoo a b, IsExtrOn f (Set.uIcc a b) c
intervalIntegral.FTCFilter.nhdsUIcc 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
{x a b : ℝ} [h : Fact (x ∈ Set.uIcc a b)] : intervalIntegral.FTCFilter x (nhdsWithin x (Set.uIcc a b)) (nhdsWithin x (Set.uIcc a b))
intervalIntegral.integral_eq_sub_of_hasDerivAt 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
{E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E} (hderiv : ∀ x ∈ Set.uIcc a b, HasDerivAt f (f' x) x) (hint : IntervalIntegrable f' MeasureTheory.volume a b) : ∫ (y : ℝ) in a..b, f' y = f b - f a
intervalIntegral.integral_deriv_eq_sub' 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
{E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f' : ℝ → E} (f : ℝ → E) (hderiv : deriv f = f') (hdiff : ∀ x ∈ Set.uIcc a b, DifferentiableAt ℝ f x) (hcont : ContinuousOn f' (Set.uIcc a b)) : ∫ (y : ℝ) in a..b, f' y = f b - f a
intervalIntegral.integral_eq_sub_of_hasDeriv_right 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
{E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E} (hcont : ContinuousOn f (Set.uIcc a b)) (hderiv : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) (hint : IntervalIntegrable f' MeasureTheory.volume a b) : ∫ (y : ℝ) in a..b, f' y = f b - f a
intervalIntegral.integral_deriv_eq_sub 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
{E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f : ℝ → E} (hderiv : ∀ x ∈ Set.uIcc a b, DifferentiableAt ℝ f x) (hint : IntervalIntegrable (deriv f) MeasureTheory.volume a b) : ∫ (y : ℝ) in a..b, deriv f y = f b - f a
intervalIntegral.integral_deriv_eq_sub_uIoo 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
{E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f : ℝ → E} (hcont : ContinuousOn f (Set.uIcc a b)) (hderiv : ∀ x ∈ Set.uIoo a b, DifferentiableAt ℝ f x) (hint : IntervalIntegrable (deriv f) MeasureTheory.volume a b) : ∫ (y : ℝ) in a..b, deriv f y = f b - f a
intervalIntegral.intervalIntegrable_deriv_of_nonneg 📋 Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
{g' g : ℝ → ℝ} {a b : ℝ} (hcont : ContinuousOn g (Set.uIcc a b)) (hderiv : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt g (g' x) x) (hpos : ∀ x ∈ Set.Ioo (min a b) (max a b), 0 ≤ g' x) : IntervalIntegrable g' MeasureTheory.volume a b
intervalIntegrable_inv_iff 📋 Mathlib.Analysis.SpecialFunctions.NonIntegrable
{a b : ℝ} : IntervalIntegrable (fun x => x⁻¹) MeasureTheory.volume a b ↔ a = b ∨ 0 ∉ Set.uIcc a b
intervalIntegrable_sub_inv_iff 📋 Mathlib.Analysis.SpecialFunctions.NonIntegrable
{a b c : ℝ} : IntervalIntegrable (fun x => (x - c)⁻¹) MeasureTheory.volume a b ↔ a = b ∨ c ∉ Set.uIcc a b
not_intervalIntegrable_of_sub_inv_isBigO_punctured 📋 Mathlib.Analysis.SpecialFunctions.NonIntegrable
{F : Type u_2} [NormedAddCommGroup F] {f : ℝ → F} {a b c : ℝ} (hf : (fun x => (x - c)⁻¹) =O[nhdsWithin c {c}ᶜ] f) (hne : a ≠ b) (hc : c ∈ Set.uIcc a b) : ¬IntervalIntegrable f MeasureTheory.volume a b
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter 📋 Mathlib.Analysis.SpecialFunctions.NonIntegrable
{E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] {f : ℝ → E} {g : ℝ → F} {a b : ℝ} (l : Filter ℝ) [l.NeBot] [Filter.TendstoIxxClass Set.Icc l l] (hl : Set.uIcc a b ∈ l) (hd : ∀ᶠ (x : ℝ) in l, DifferentiableAt ℝ f x) (hf : Filter.Tendsto (fun x => ‖f x‖) l Filter.atTop) (hfg : deriv f =O[l] g) : ¬IntervalIntegrable g MeasureTheory.volume a b
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured 📋 Mathlib.Analysis.SpecialFunctions.NonIntegrable
{E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] {f : ℝ → E} {g : ℝ → F} {a b c : ℝ} (h_deriv : ∀ᶠ (x : ℝ) in nhdsWithin c {c}ᶜ, DifferentiableAt ℝ f x) (h_infty : Filter.Tendsto (fun x => ‖f x‖) (nhdsWithin c {c}ᶜ) Filter.atTop) (hg : deriv f =O[nhdsWithin c {c}ᶜ] g) (hne : a ≠ b) (hc : c ∈ Set.uIcc a b) : ¬IntervalIntegrable g MeasureTheory.volume a b
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_within_sdiff_singleton 📋 Mathlib.Analysis.SpecialFunctions.NonIntegrable
{E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] {f : ℝ → E} {g : ℝ → F} {a b c : ℝ} (hne : a ≠ b) (hc : c ∈ Set.uIcc a b) (h_deriv : ∀ᶠ (x : ℝ) in nhdsWithin c (Set.uIcc a b \ {c}), DifferentiableAt ℝ f x) (h_infty : Filter.Tendsto (fun x => ‖f x‖) (nhdsWithin c (Set.uIcc a b \ {c})) Filter.atTop) (hg : deriv f =O[nhdsWithin c (Set.uIcc a b \ {c})] g) : ¬IntervalIntegrable g MeasureTheory.volume a b
MeasureTheory.integral_eq_of_hasDerivAt_off_countable 📋 Mathlib.MeasureTheory.Integral.DivergenceTheorem
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f f' : ℝ → E) {a b : ℝ} {s : Set ℝ} (hs : s.Countable) (Hc : ContinuousOn f (Set.uIcc a b)) (Hd : ∀ x ∈ Set.Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x) (Hi : IntervalIntegrable f' MeasureTheory.volume a b) : ∫ (x : ℝ) in a..b, f' x = f b - f a
MeasureTheory.integral2_divergence_prod_of_hasFDerivAt 📋 Mathlib.MeasureTheory.Integral.DivergenceTheorem
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f g : ℝ × ℝ → E) (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a₁ a₂ b₁ b₂ : ℝ) (Hcf : ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂)) (Hcg : ContinuousOn g (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂)) (Hdf : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂), HasFDerivAt f (f' x) x) (Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂), HasFDerivAt g (g' x) x) (Hi : MeasureTheory.IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) MeasureTheory.volume) : ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) = (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) - ∫ (y : ℝ) in a₂..b₂, f (a₁, y)
MeasureTheory.integral2_divergence_prod_of_hasFDerivAt_off_countable 📋 Mathlib.MeasureTheory.Integral.DivergenceTheorem
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f g : ℝ × ℝ → E) (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a₁ a₂ b₁ b₂ : ℝ) (s : Set (ℝ × ℝ)) (hs : s.Countable) (Hcf : ContinuousOn f (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂)) (Hcg : ContinuousOn g (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂)) (Hdf : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt f (f' x) x) (Hdg : ∀ x ∈ Set.Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Set.Ioo (min a₂ b₂) (max a₂ b₂) \ s, HasFDerivAt g (g' x) x) (Hi : MeasureTheory.IntegrableOn (fun x => (f' x) (1, 0) + (g' x) (0, 1)) (Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂) MeasureTheory.volume) : ∫ (x : ℝ) in a₁..b₁, ∫ (y : ℝ) in a₂..b₂, (f' (x, y)) (1, 0) + (g' (x, y)) (0, 1) = (((∫ (x : ℝ) in a₁..b₁, g (x, b₂)) - ∫ (x : ℝ) in a₁..b₁, g (x, a₂)) + ∫ (y : ℝ) in a₂..b₂, f (b₁, y)) - ∫ (y : ℝ) in a₂..b₂, f (a₁, y)
Complex.integral_boundary_rect_eq_zero_of_differentiableOn 📋 Mathlib.Analysis.Complex.CauchyIntegral
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) (H : DifferentiableOn ℂ f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im)) : (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) + Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) = 0
Complex.integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn 📋 Mathlib.Analysis.Complex.CauchyIntegral
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) (Hc : ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im)) (Hd : DifferentiableOn ℂ f (Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im))) : (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) + Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) = 0
Complex.integral_boundary_rect_eq_zero_of_differentiable_on_off_countable 📋 Mathlib.Analysis.Complex.CauchyIntegral
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ) (s : Set ℂ) (hs : s.Countable) (Hc : ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im)) (Hd : ∀ x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im) \ s, DifferentiableAt ℂ f x) : (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) + Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) = 0
Complex.integral_boundary_rect_of_continuousOn_of_hasFDerivAt_real 📋 Mathlib.Analysis.Complex.CauchyIntegral
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℂ → E) (f' : ℂ → ℂ →L[ℝ] E) (z w : ℂ) (Hc : ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im)) (Hd : ∀ x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im), HasFDerivAt f (f' x) x) (Hi : MeasureTheory.IntegrableOn (fun z => Complex.I • (f' z) 1 - (f' z) Complex.I) (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) MeasureTheory.volume) : (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) + Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) - Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) = ∫ (x : ℝ) in z.re..w.re, ∫ (y : ℝ) in z.im..w.im, Complex.I • (f' (↑x + ↑y * Complex.I)) 1 - (f' (↑x + ↑y * Complex.I)) Complex.I

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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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.
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 69fae59