Loogle!

Result

Found 29 declarations mentioning Filter.generate.

• Filter.generate 📋 Mathlib.Order.Filter.Basic
  {α : Type u} (g : Set (Set α)) : Filter α
• Filter.generate_univ 📋 Mathlib.Order.Filter.Basic
  {α : Type u} : Filter.generate Set.univ = ⊥
• Filter.mkOfClosure 📋 Mathlib.Order.Filter.Basic
  {α : Type u} (s : Set (Set α)) (hs : (Filter.generate s).sets = s) : Filter α
• Filter.generate_empty 📋 Mathlib.Order.Filter.Basic
  {α : Type u} : Filter.generate ∅ = ⊤
• Filter.generate_singleton 📋 Mathlib.Order.Filter.Basic
  {α : Type u} (s : Set α) : Filter.generate {s} = Filter.principal s
• Filter.mkOfClosure_sets 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s : Set (Set α)} {hs : (Filter.generate s).sets = s} : Filter.mkOfClosure s hs = Filter.generate s
• Filter.iInf_eq_generate 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {ι : Sort x} (s : ι → Filter α) : iInf s = Filter.generate (⋃ i, (s i).sets)
• Filter.mem_generate_of_mem 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s : Set (Set α)} {U : Set α} (h : U ∈ s) : U ∈ Filter.generate s
• Filter.generate_iUnion 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {ι : Sort x} {s : ι → Set (Set α)} : Filter.generate (⋃ i, s i) = ⨅ i, Filter.generate (s i)
• Filter.generate_union 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s t : Set (Set α)} : Filter.generate (s ∪ t) = Filter.generate s ⊓ Filter.generate t
• Filter.le_generate_iff 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {s : Set (Set α)} {f : Filter α} : f ≤ Filter.generate s ↔ s ⊆ f.sets
• Filter.giGenerate 📋 Mathlib.Order.Filter.Basic
  (α : Type u_2) : GaloisInsertion Filter.generate Filter.sets
• Filter.generate_eq_biInf 📋 Mathlib.Order.Filter.Basic
  {α : Type u} (S : Set (Set α)) : Filter.generate S = ⨅ s ∈ S, Filter.principal s
• Filter.generate_image_preimage_le_comap 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (U : Set (Set α)) (f : β → α) : Filter.generate ((fun x => f ⁻¹' x) '' U) ≤ Filter.comap f (Filter.generate U)
• Filter.map_generate_le_generate_preimage_preimage 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (U : Set (Set β)) (f : β → α) : Filter.map f (Filter.generate U) ≤ Filter.generate ((fun x => f ⁻¹' x) ⁻¹' U)
• FilterBasis.generate 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} (B : FilterBasis α) : Filter.generate B.sets = B.filter
• Filter.HasBasis.eq_generate 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s) : l = Filter.generate {U | ∃ i, p i ∧ s i = U}
• Filter.IsBasis.filter_eq_generate 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) : h.filter = Filter.generate {U | ∃ i, p i ∧ s i = U}
• Filter.atTop_eq_generate_Ici 📋 Mathlib.Order.Filter.AtTopBot.Defs
  {α : Type u_3} [Preorder α] : Filter.atTop = Filter.generate (Set.range Set.Ici)
• Filter.atTop_eq_generate_of_forall_exists_le 📋 Mathlib.Order.Filter.AtTopBot.Defs
  {α : Type u_3} [Preorder α] {s : Set α} (hs : ∀ (x : α), ∃ y ∈ s, x ≤ y) : Filter.atTop = Filter.generate (Set.Ici '' s)
• Filter.atTop_eq_generate_of_not_bddAbove 📋 Mathlib.Order.Filter.AtTopBot.Defs
  {α : Type u_3} [LinearOrder α] {s : Set α} (hs : ¬BddAbove s) : Filter.atTop = Filter.generate (Set.Ici '' s)
• Filter.mem_generate_iff 📋 Mathlib.Order.Filter.Finite
  {α : Type u} {s : Set (Set α)} {U : Set α} : U ∈ Filter.generate s ↔ ∃ t ⊆ s, t.Finite ∧ ⋂₀ t ⊆ U
• Filter.smallSets_eq_generate 📋 Mathlib.Order.Filter.SmallSets
  {α : Type u_1} {f : Filter α} : f.smallSets = Filter.generate (Set.powerset '' f.sets)
• Filter.ofSets_filter_eq_generate 📋 Mathlib.Order.Filter.Bases.Finite
  {α : Type u_1} (s : Set (Set α)) : (Filter.FilterBasis.ofSets s).filter = Filter.generate s
• Filter.generate_neBot_iff 📋 Mathlib.Order.Filter.Bases.Finite
  {α : Type u_1} {s : Set (Set α)} : (Filter.generate s).NeBot ↔ ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty
• Filter.hasBasis_generate 📋 Mathlib.Order.Filter.Bases.Finite
  {α : Type u_1} (s : Set (Set α)) : (Filter.generate s).HasBasis (fun t => t.Finite ∧ t ⊆ s) fun t => ⋂₀ t
• Filter.generate_eq_generate_inter 📋 Mathlib.Order.Filter.Bases.Finite
  {α : Type u_1} (s : Set (Set α)) : Filter.generate s = Filter.generate (Set.sInter '' {t | t.Finite ∧ t ⊆ s})
• Filter.IsCountablyGenerated.mk 📋 Mathlib.Order.Filter.CountablyGenerated
  {α : Type u_1} {f : Filter α} (out : ∃ s, s.Countable ∧ f = Filter.generate s) : f.IsCountablyGenerated
• Filter.IsCountablyGenerated.out 📋 Mathlib.Order.Filter.CountablyGenerated
  {α : Type u_1} {f : Filter α} [self : f.IsCountablyGenerated] : ∃ s, s.Countable ∧ f = Filter.generate s

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:

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.

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 f167e8d