Loogle!

Result

Found 278 declarations mentioning Monotone and Set. Of these, 94 match your pattern(s).

Set.monotone_powerset 📋 Mathlib.Data.Set.Basic
{α : Type u} : Monotone Set.powerset
Set.monotone_image 📋 Mathlib.Data.Set.Image
{α : Type u_1} {β : Type u_2} {f : α → β} : Monotone (Set.image f)
Set.offDiag_mono 📋 Mathlib.Data.Set.Prod
{α : Type u_1} : Monotone Set.offDiag
Monotone.set_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] {f : α → Set β} {g : α → Set γ} (hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x ×ˢ g x
Monotone.iUnion_nat_add 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {f : ℕ → Set α} (hf : Monotone f) (k : ℕ) : ⋃ n, f (n + k) = ⋃ n, f n
Set.iUnion_inter_of_monotone 📋 Mathlib.Data.Set.Lattice
{ι : Type u_12} {α : Type u_13} [Preorder ι] [IsDirected ι fun x1 x2 => x1 ≤ x2] {s t : ι → Set α} (hs : Monotone s) (ht : Monotone t) : ⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i
Set.iInter_union_of_monotone 📋 Mathlib.Data.Set.Lattice
{ι : Type u_12} {α : Type u_13} [Preorder ι] [IsDirected ι (Function.swap fun x1 x2 => x1 ≤ x2)] {s t : ι → Set α} (hs : Monotone s) (ht : Monotone t) : ⋂ i, s i ∪ t i = (⋂ i, s i) ∪ ⋂ i, t i
Set.monotone_setOf 📋 Mathlib.Data.Set.Order
{α : Type u_1} {β : Type u_2} [Preorder α] {p : α → β → Prop} (hp : ∀ (b : β), Monotone fun a => p a b) : Monotone fun a => {b | p a b}
Monotone.inter 📋 Mathlib.Data.Set.Order
{α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} (hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x ∩ g x
Monotone.union 📋 Mathlib.Data.Set.Order
{α : Type u_1} {β : Type u_2} [Preorder β] {f g : β → Set α} (hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x ∪ g x
SetLike.coe_mono 📋 Mathlib.Data.SetLike.Basic
{A : Type u_1} {B : Type u_2} [i : SetLike A B] : Monotone SetLike.coe
Set.nsmul_right_monotone 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [AddMonoid α] {s : Set α} (hs : 0 ∈ s) : Monotone fun x => x • s
Set.pow_right_monotone 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [Monoid α] {s : Set α} (hs : 1 ∈ s) : Monotone fun x => s ^ x
Set.kernImage_mono 📋 Mathlib.Data.Set.Lattice.Image
{α : Type u_1} {β : Type u_2} {f : α → β} : Monotone (Set.kernImage f)
Set.monotone_preimage 📋 Mathlib.Data.Set.Lattice.Image
{α : Type u_1} {β : Type u_2} {f : α → β} : Monotone (Set.preimage f)
Set.iUnion_prod_of_monotone 📋 Mathlib.Data.Set.Lattice.Image
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] {s : α → Set β} {t : α → Set γ} (hs : Monotone s) (ht : Monotone t) : ⋃ x, s x ×ˢ t x = (⋃ x, s x) ×ˢ ⋃ x, t x
Set.monotone_accumulate 📋 Mathlib.Data.Set.Accumulate
{α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] : Monotone (Set.Accumulate s)
Set.iUnion_iInter_of_monotone 📋 Mathlib.Data.Set.Finite.Lattice
{ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [Preorder ι'] [IsDirected ι' fun x1 x2 => x1 ≤ x2] [Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ (i : ι), Monotone (s i)) : ⋃ j, ⋂ i, s i j = ⋂ i, ⋃ j, s i j
Set.iInter_iUnion_of_monotone 📋 Mathlib.Data.Set.Finite.Lattice
{ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [Preorder ι'] [IsDirected ι' (Function.swap fun x1 x2 => x1 ≤ x2)] [Nonempty ι'] {s : ι → ι' → Set α} (hs : ∀ (i : ι), Monotone (s i)) : ⋂ j, ⋃ i, s i j = ⋃ i, ⋂ j, s i j
Set.iUnion_univ_pi_of_monotone 📋 Mathlib.Data.Set.Finite.Lattice
{ι : Type u_1} {ι' : Type u_2} [LinearOrder ι'] [Nonempty ι'] [Finite ι] {α : ι → Type u_3} {s : (i : ι) → ι' → Set (α i)} (hs : ∀ (i : ι), Monotone (s i)) : (⋃ j, Set.univ.pi fun i => s i j) = Set.univ.pi fun i => ⋃ j, s i j
Set.iUnion_pi_of_monotone 📋 Mathlib.Data.Set.Finite.Lattice
{ι : Type u_1} {ι' : Type u_2} [LinearOrder ι'] [Nonempty ι'] {α : ι → Type u_3} {I : Set ι} {s : (i : ι) → ι' → Set (α i)} (hI : I.Finite) (hs : ∀ i ∈ I, Monotone (s i)) : (⋃ j, I.pi fun i => s i j) = I.pi fun i => ⋃ j, s i j
infClosure_mono 📋 Mathlib.Order.SupClosed
{α : Type u_3} [SemilatticeInf α] : Monotone ⇑infClosure
latticeClosure_mono 📋 Mathlib.Order.SupClosed
{α : Type u_3} [Lattice α] : Monotone ⇑latticeClosure
supClosure_mono 📋 Mathlib.Order.SupClosed
{α : Type u_3} [SemilatticeSup α] : Monotone ⇑supClosure
Filter.HasBasis.biInter_mem 📋 Mathlib.Order.Filter.Bases.Basic
{α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {f : Set α → Set β} (h : l.HasBasis p s) (hf : Monotone f) : ⋂ t ∈ l, f t = ⋂ i, ⋂ (_ : p i), f (s i)
Monotone.piecewise_eventually_eq_iUnion 📋 Mathlib.Order.Filter.AtTopBot.Defs
{ι : Type u_1} {α : Type u_3} {β : α → Type u_6} [Preorder ι] {s : ι → Set α} [(i : ι) → DecidablePred fun x => x ∈ s i] [DecidablePred fun x => x ∈ ⋃ i, s i] (hs : Monotone s) (f g : (a : α) → β a) (a : α) : ∀ᶠ (i : ι) in Filter.atTop, (s i).piecewise f g a = (⋃ i, s i).piecewise f g a
Filter.lift'_principal 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {h : Set α → Set β} {s : Set α} (hh : Monotone h) : (Filter.principal s).lift' h = Filter.principal (h s)
Filter.lift'_bot 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {h : Set α → Set β} (hh : Monotone h) : ⊥.lift' h = Filter.principal (h ∅)
Filter.lift'_pure 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {h : Set α → Set β} {a : α} (hh : Monotone h) : (pure a).lift' h = Filter.principal (h {a})
Filter.lift'_neBot_iff 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} (hh : Monotone h) : (f.lift' h).NeBot ↔ ∀ s ∈ f, (h s).Nonempty
Filter.HasBasis.lift' 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} {ι : Sort u_5} {p : ι → Prop} {s : ι → Set α} (hf : f.HasBasis p s) (hh : Monotone h) : (f.lift' h).HasBasis p (h ∘ s)
Filter.comap_lift'_eq2 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : β → α} {g : Set β → Set γ} (hg : Monotone g) : (Filter.comap m f).lift' g = f.lift' (g ∘ Set.preimage m)
Filter.map_lift'_eq 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {h : Set α → Set β} {m : β → γ} (hh : Monotone h) : Filter.map m (f.lift' h) = f.lift' (Set.image m ∘ h)
Filter.map_lift'_eq2 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set β → Set γ} {m : α → β} (hg : Monotone g) : (Filter.map m f).lift' g = f.lift' (g ∘ Set.image m)
Filter.mem_lift'_sets 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} (hh : Monotone h) {s : Set β} : s ∈ f.lift' h ↔ ∃ t ∈ f, h t ⊆ s
Filter.eventually_lift'_iff 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} (hh : Monotone h) {p : β → Prop} : (∀ᶠ (y : β) in f.lift' h, p y) ↔ ∃ t ∈ f, ∀ y ∈ h t, p y
Filter.lift_lift'_assoc 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set α → Set β} {h : Set β → Filter γ} (hg : Monotone g) (hh : Monotone h) : (f.lift' g).lift h = f.lift fun s => h (g s)
Filter.sInter_lift'_sets 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} (hh : Monotone h) : ⋂₀ {s | s ∈ f.lift' h} = ⋂ s ∈ f, h s
Filter.lift'_lift'_assoc 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set α → Set β} {h : Set β → Set γ} (hg : Monotone g) (hh : Monotone h) : (f.lift' g).lift' h = f.lift' fun s => h (g s)
Filter.lift_lift'_same_eq_lift' 📋 Mathlib.Order.Filter.Lift
{α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Set α → Set β} (hg₁ : ∀ (s : Set α), Monotone fun t => g s t) (hg₂ : ∀ (t : Set α), Monotone fun s => g s t) : (f.lift fun s => f.lift' (g s)) = f.lift' fun s => g s s
Filter.prod_lift'_lift' 📋 Mathlib.Order.Filter.Lift
{α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} {f₁ : Filter α₁} {f₂ : Filter α₂} {g₁ : Set α₁ → Set β₁} {g₂ : Set α₂ → Set β₂} (hg₁ : Monotone g₁) (hg₂ : Monotone g₂) : f₁.lift' g₁ ×ˢ f₂.lift' g₂ = f₁.lift fun s => f₂.lift' fun t => g₁ s ×ˢ g₂ t
Filter.ker_mono 📋 Mathlib.Order.Filter.Ker
{α : Type u_2} : Monotone Filter.ker
monotone_closure 📋 Mathlib.Topology.Closure
(X : Type u_1) [TopologicalSpace X] : Monotone closure
Monotone.iInter_comp_tendsto_atBot 📋 Mathlib.Order.Filter.AtTopBot.CompleteLattice
{α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder β] {l : Filter α} [l.NeBot] {s : β → Set γ} (hs : Monotone s) {f : α → β} (hf : Filter.Tendsto f l Filter.atBot) : ⋂ a, s (f a) = ⋂ b, s b
Monotone.iUnion_comp_tendsto_atTop 📋 Mathlib.Order.Filter.AtTopBot.CompleteLattice
{α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder β] {l : Filter α} [l.NeBot] {s : β → Set γ} (hs : Monotone s) {f : α → β} (hf : Filter.Tendsto f l Filter.atTop) : ⋃ a, s (f a) = ⋃ b, s b
Monotone.compRel 📋 Mathlib.Topology.UniformSpace.Defs
{α : Type ua} {β : Type ub} [Preorder β] {f g : β → Set (α × α)} (hf : Monotone f) (hg : Monotone g) : Monotone fun x => compRel (f x) (g x)
UniformOnFun.isCountablyGenerated_uniformity 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
{α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) [(uniformity β).IsCountablyGenerated] {t : ℕ → Set α} (ht : ∀ (n : ℕ), t n ∈ 𝔖) (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n) : (uniformity (UniformOnFun α β 𝔖)).IsCountablyGenerated
UniformOnFun.hasAntitoneBasis_uniformity 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
{α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) {ι : Type u_5} [Preorder ι] [IsDirected ι fun x1 x2 => x1 ≤ x2] {t : ι → Set α} {V : ι → Set (β × β)} (ht : ∀ (n : ι), t n ∈ 𝔖) (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n) (hb : (uniformity β).HasAntitoneBasis V) : (uniformity (UniformOnFun α β 𝔖)).HasAntitoneBasis fun n => UniformOnFun.gen 𝔖 (t n) (V n)
Rel.core_mono 📋 Mathlib.Data.Rel
{α : Type u_1} {β : Type u_2} (r : Rel α β) : Monotone r.core
Rel.image_mono 📋 Mathlib.Data.Rel
{α : Type u_1} {β : Type u_2} (r : Rel α β) : Monotone r.image
monotone_Iic 📋 Mathlib.Order.Interval.Set.Monotone
{α : Type u_1} [Preorder α] : Monotone Set.Iic
monotone_Iio 📋 Mathlib.Order.Interval.Set.Monotone
{α : Type u_1} [Preorder α] : Monotone Set.Iio
Antitone.Ici 📋 Mathlib.Order.Interval.Set.Monotone
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) : Monotone fun x => Set.Ici (f x)
Antitone.Ioi 📋 Mathlib.Order.Interval.Set.Monotone
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Antitone f) : Monotone fun x => Set.Ioi (f x)
Monotone.Iic 📋 Mathlib.Order.Interval.Set.Monotone
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) : Monotone fun x => Set.Iic (f x)
Monotone.Iio 📋 Mathlib.Order.Interval.Set.Monotone
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β} (hf : Monotone f) : Monotone fun x => Set.Iio (f x)
Antitone.Icc 📋 Mathlib.Order.Interval.Set.Monotone
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} (hf : Antitone f) (hg : Monotone g) : Monotone fun x => Set.Icc (f x) (g x)
Antitone.Ico 📋 Mathlib.Order.Interval.Set.Monotone
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} (hf : Antitone f) (hg : Monotone g) : Monotone fun x => Set.Ico (f x) (g x)
Antitone.Ioc 📋 Mathlib.Order.Interval.Set.Monotone
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} (hf : Antitone f) (hg : Monotone g) : Monotone fun x => Set.Ioc (f x) (g x)
Antitone.Ioo 📋 Mathlib.Order.Interval.Set.Monotone
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β} (hf : Antitone f) (hg : Monotone g) : Monotone fun x => Set.Ioo (f x) (g x)
MeasurableSet.iUnion_of_monotone_of_frequently 📋 Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
{α : Type u_1} [MeasurableSpace α] {ι : Type u_5} [Preorder ι] [Filter.atTop.IsCountablyGenerated] {s : ι → Set α} (hsm : Monotone s) (hs : ∃ᶠ (i : ι) in Filter.atTop, MeasurableSet (s i)) : MeasurableSet (⋃ i, s i)
MeasurableSet.iUnion_of_monotone 📋 Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
{α : Type u_1} [MeasurableSpace α] {ι : Type u_5} [Preorder ι] [IsDirected ι fun x1 x2 => x1 ≤ x2] [Filter.atTop.IsCountablyGenerated] {s : ι → Set α} (hsm : Monotone s) (hs : ∀ (i : ι), MeasurableSet (s i)) : MeasurableSet (⋃ i, s i)
Set.iSup_indicator 📋 Mathlib.Algebra.Order.Group.Indicator
{α : Type u_2} {M : Type u_3} [CompleteLattice M] [Zero M] {ι : Type u_4} [Preorder ι] [IsDirected ι fun x1 x2 => x1 ≤ x2] {f : ι → α → M} {s : ι → Set α} (h1 : ⊥ = 0) (hf : Monotone f) (hs : Monotone s) : ⨆ i, (s i).indicator (f i) = (⋃ i, s i).indicator (⨆ i, f i)
Set.iSup_mulIndicator 📋 Mathlib.Algebra.Order.Group.Indicator
{α : Type u_2} {M : Type u_3} [CompleteLattice M] [One M] {ι : Type u_4} [Preorder ι] [IsDirected ι fun x1 x2 => x1 ≤ x2] {f : ι → α → M} {s : ι → Set α} (h1 : ⊥ = 1) (hf : Monotone f) (hs : Monotone s) : ⨆ i, (s i).mulIndicator (f i) = (⋃ i, s i).mulIndicator (⨆ i, f i)
isPiSystem_iUnion_of_monotone 📋 Mathlib.MeasureTheory.PiSystem
{α : Type u_3} {ι : Type u_4} [SemilatticeSup ι] (p : ι → Set (Set α)) (hp_pi : ∀ (n : ι), IsPiSystem (p n)) (hp_mono : Monotone p) : IsPiSystem (⋃ n, p n)
MeasureTheory.tendsto_measure_iUnion_atTop 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
{α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Preorder ι] [Filter.atTop.IsCountablyGenerated] {s : ι → Set α} (hm : Monotone s) : Filter.Tendsto (⇑μ ∘ s) Filter.atTop (nhds (μ (⋃ n, s n)))
Monotone.measure_iUnion 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
{α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Preorder ι] [IsDirected ι fun x1 x2 => x1 ≤ x2] [Filter.atTop.IsCountablyGenerated] {s : ι → Set α} (hs : Monotone s) : μ (⋃ i, s i) = ⨆ i, μ (s i)
MeasureTheory.tendsto_measure_iInter_atBot 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
{α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Preorder ι] [Filter.atBot.IsCountablyGenerated] {s : ι → Set α} (hs : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) (hm : Monotone s) (hf : ∃ i, μ (s i) ≠ ⊤) : Filter.Tendsto (⇑μ ∘ s) Filter.atBot (nhds (μ (⋂ n, s n)))
Monotone.measure_iInter 📋 Mathlib.MeasureTheory.Measure.MeasureSpace
{α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Preorder ι] [IsDirected ι fun x1 x2 => x1 ≥ x2] [Filter.atBot.IsCountablyGenerated] {s : ι → Set α} (hs : Monotone s) (hsm : ∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) (hfin : ∃ i, μ (s i) ≠ ⊤) : μ (⋂ i, s i) = ⨅ i, μ (s i)
MeasureTheory.monotone_spanningSets 📋 Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
{α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : Monotone (MeasureTheory.spanningSets μ)
IsOpen.exists_iUnion_isClosed 📋 Mathlib.Topology.MetricSpace.HausdorffDistance
{α : Type u} [PseudoEMetricSpace α] {U : Set α} (hU : IsOpen U) : ∃ F, (∀ (n : ℕ), IsClosed (F n)) ∧ (∀ (n : ℕ), F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F
MeasureTheory.Measure.InnerRegularWRT.of_restrict 📋 Mathlib.MeasureTheory.Measure.Regular
{α : Type u_1} [MeasurableSpace α] {p : Set α → Prop} {μ : MeasureTheory.Measure α} {s : ℕ → Set α} (h : ∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet) (hs : Set.univ ⊆ ⋃ n, s n) (hmono : Monotone s) : μ.InnerRegularWRT p MeasurableSet
CauchyFilter.monotone_gen 📋 Mathlib.Topology.UniformSpace.Completion
{α : Type u} [UniformSpace α] : Monotone CauchyFilter.gen
MeasureTheory.univ_le_of_forall_fin_meas_le 📋 Mathlib.MeasureTheory.Integral.Lebesgue.Countable
{α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) [MeasureTheory.SigmaFinite (μ.trim hm)] (C : ENNReal) {f : Set α → ENNReal} (hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → f s ≤ C) (h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)) : f Set.univ ≤ C
Monotone.indicator_eventuallyEq_iUnion 📋 Mathlib.Order.Filter.IndicatorFunction
{α : Type u_1} {β : Type u_2} {ι : Type u_5} [Preorder ι] [Zero β] (s : ι → Set α) (hs : Monotone s) (f : α → β) (a : α) : (fun i => (s i).indicator f a) =ᶠ[Filter.atTop] fun x => (⋃ i, s i).indicator f a
Monotone.mulIndicator_eventuallyEq_iUnion 📋 Mathlib.Order.Filter.IndicatorFunction
{α : Type u_1} {β : Type u_2} {ι : Type u_5} [Preorder ι] [One β] (s : ι → Set α) (hs : Monotone s) (f : α → β) (a : α) : (fun i => (s i).mulIndicator f a) =ᶠ[Filter.atTop] fun x => (⋃ i, s i).mulIndicator f a
Monotone.tendsto_indicator 📋 Mathlib.Order.Filter.IndicatorFunction
{α : Type u_1} {β : Type u_2} {ι : Type u_5} [Preorder ι] [Zero β] (s : ι → Set α) (hs : Monotone s) (f : α → β) (a : α) : Filter.Tendsto (fun i => (s i).indicator f a) Filter.atTop (pure ((⋃ i, s i).indicator f a))
Monotone.tendsto_mulIndicator 📋 Mathlib.Order.Filter.IndicatorFunction
{α : Type u_1} {β : Type u_2} {ι : Type u_5} [Preorder ι] [One β] (s : ι → Set α) (hs : Monotone s) (f : α → β) (a : α) : Filter.Tendsto (fun i => (s i).mulIndicator f a) Filter.atTop (pure ((⋃ i, s i).mulIndicator f a))
MeasureTheory.tendsto_setIntegral_of_monotone 📋 Mathlib.MeasureTheory.Integral.Bochner.Set
{X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} [Preorder ι] [Filter.atTop.IsCountablyGenerated] {s : ι → Set X} (hsm : ∀ (i : ι), MeasurableSet (s i)) (h_mono : Monotone s) (hfi : MeasureTheory.IntegrableOn f (⋃ n, s n) μ) : Filter.Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) Filter.atTop (nhds (∫ (x : X) in ⋃ n, s n, f x ∂μ))
Besicovitch.TauPackage.monotone_iUnionUpTo 📋 Mathlib.MeasureTheory.Covering.Besicovitch
{α : Type u_1} [MetricSpace α] {β : Type u} [Nonempty β] (p : Besicovitch.TauPackage β α) : Monotone p.iUnionUpTo
posTangentConeAt_mono 📋 Mathlib.Analysis.Calculus.LocalExtr.Basic
{E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {a : E} : Monotone fun s => posTangentConeAt s a
SimpleGraph.Subgraph.verts_monotone 📋 Mathlib.Combinatorics.SimpleGraph.Subgraph
{V : Type u} {G : SimpleGraph V} : Monotone SimpleGraph.Subgraph.verts
Matroid.closure_mono 📋 Mathlib.Data.Matroid.Closure
{α : Type u_2} (M : Matroid α) : Monotone M.closure
Dynamics.dynEntourage_monotone 📋 Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
{X : Type u_1} (T : X → X) (n : ℕ) : Monotone fun U => Dynamics.dynEntourage T U n
FirstOrder.Language.monotone_distinctConstantsTheory 📋 Mathlib.ModelTheory.Syntax
{L : FirstOrder.Language} {α : Type u'} : Monotone L.distinctConstantsTheory
MeasureTheory.tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum 📋 Mathlib.MeasureTheory.Measure.AddContent
{α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent C} (hC : MeasureTheory.IsSetRing C) (m_iUnion : ∀ (f : ℕ → Set α), (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)) ⦃f : ℕ → Set α⦄ (hf_mono : Monotone f) (hf : ∀ (i : ℕ), f i ∈ C) (hf_Union : ⋃ i, f i ∈ C) : Filter.Tendsto (fun n => m (f n)) Filter.atTop (nhds (m (⋃ i, f i)))
MeasurableSpace.generateMeasurableRec_mono 📋 Mathlib.MeasureTheory.MeasurableSpace.Card
{α : Type u} (s : Set (Set α)) : Monotone (MeasurableSpace.generateMeasurableRec s)
ProbabilityTheory.Kernel.tendsto_densityProcess_fst_atTop_univ_of_monotone 📋 Mathlib.Probability.Kernel.Disintegration.Density
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β)) (n : ℕ) (a : α) (x : γ) (seq : ℕ → Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ i, seq i = Set.univ) : Filter.Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) Filter.atTop (nhds (κ.densityProcess κ.fst n a x Set.univ))
ProbabilityTheory.Kernel.tendsto_densityProcess_fst_atTop_ae_of_monotone 📋 Mathlib.Probability.Kernel.Disintegration.Density
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β)) [ProbabilityTheory.IsFiniteKernel κ] (n : ℕ) (a : α) (seq : ℕ → Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ i, seq i = Set.univ) : ∀ᵐ (x : γ) ∂κ.fst a, Filter.Tendsto (fun m => κ.densityProcess κ.fst n a x (seq m)) Filter.atTop (nhds 1)
ProbabilityTheory.Kernel.tendsto_density_fst_atTop_ae_of_monotone 📋 Mathlib.Probability.Kernel.Disintegration.Density
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)} [ProbabilityTheory.IsFiniteKernel κ] (a : α) (seq : ℕ → Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ i, seq i = Set.univ) (hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)) : ∀ᵐ (x : γ) ∂κ.fst a, Filter.Tendsto (fun m => κ.density κ.fst a x (seq m)) Filter.atTop (nhds 1)
ProbabilityTheory.Kernel.tendsto_integral_density_of_monotone 📋 Mathlib.Probability.Kernel.Disintegration.Density
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)} {ν : ProbabilityTheory.Kernel α γ} (hκν : κ.fst ≤ ν) [ProbabilityTheory.IsFiniteKernel ν] (a : α) (seq : ℕ → Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ i, seq i = Set.univ) (hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)) : Filter.Tendsto (fun m => ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) Filter.atTop (nhds ((κ a).real Set.univ))
exterior_mono 📋 Mathlib.Topology.Exterior
{X : Type u_2} [TopologicalSpace X] : Monotone exterior
Topology.RelCWComplex.skeletonLT_monotone 📋 Mathlib.Topology.CWComplex.Classical.Basic
{X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] : Monotone (Topology.RelCWComplex.skeletonLT C)
Topology.RelCWComplex.skeleton_monotone 📋 Mathlib.Topology.CWComplex.Classical.Basic
{X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [Topology.RelCWComplex C D] : Monotone (Topology.RelCWComplex.skeleton C)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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.

This is Loogle revision 19971e9 serving mathlib revision 40fea08