Loogle!

Result

Found 124 declarations mentioning Membership.mem, Set.Elem, Set.preimage, Subtype.val, Set.instMembership and Set. Of these, 49 match your pattern(s).

• Subtype.preimage_coe_compl' 📋 Mathlib.Data.Set.Image
  {α : Type u_1} (s : Set α) : (fun x => ↑x) ⁻¹' s = ∅
• Subtype.preimage_val_subset_preimage_val_iff 📋 Mathlib.Data.Set.Image
  {α : Type u_1} (s t u : Set α) : Subtype.val ⁻¹' t ⊆ Subtype.val ⁻¹' u ↔ s ∩ t ⊆ s ∩ u
• Set.image_restrict 📋 Mathlib.Data.Set.Restrict
  {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α) : s.restrict f '' (Subtype.val ⁻¹' t) = f '' (t ∩ s)
• Set.image_restrictPreimage 📋 Mathlib.Data.Set.Restrict
  {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) (f : α → β) : t.restrictPreimage f '' (Subtype.val ⁻¹' s) = Subtype.val ⁻¹' (f '' s)
• IsLowerSet.isUpperSet_preimage_coe 📋 Mathlib.Order.UpperLower.Basic
  {α : Type u_1} [LE α] {s t : Set α} (hs : IsLowerSet s) : IsUpperSet (Subtype.val ⁻¹' t) ↔ ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t
• IsUpperSet.isLowerSet_preimage_coe 📋 Mathlib.Order.UpperLower.Basic
  {α : Type u_1} [LE α] {s t : Set α} (hs : IsUpperSet s) : IsLowerSet (Subtype.val ⁻¹' t) ↔ ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
• Topology.IsCoherentWith.isOpen_of_forall_induced 📋 Mathlib.Topology.Defs.Induced
  {X : Type u_1} [tX : TopologicalSpace X] {S : Set (Set X)} (self : Topology.IsCoherentWith S) (u : Set X) : (∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)) → IsOpen u
• Topology.IsCoherentWith.mk 📋 Mathlib.Topology.Defs.Induced
  {X : Type u_1} [tX : TopologicalSpace X] {S : Set (Set X)} (isOpen_of_forall_induced : ∀ (u : Set X), (∀ s ∈ S, IsOpen (Subtype.val ⁻¹' u)) → IsOpen u) : Topology.IsCoherentWith S
• IsClosed.preimage_val 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s t : Set X} (ht : IsClosed t) : IsClosed (Subtype.val ⁻¹' t)
• IsOpen.preimage_val 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s t : Set X} (ht : IsOpen t) : IsOpen (Subtype.val ⁻¹' t)
• IsClosed.inter_preimage_val_iff 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsClosed s) : IsClosed (Subtype.val ⁻¹' t) ↔ IsClosed (s ∩ t)
• IsOpen.inter_preimage_val_iff 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : IsOpen s) : IsOpen (Subtype.val ⁻¹' t) ↔ IsOpen (s ∩ t)
• isClosed_preimage_val 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s t : Set X} : IsClosed (Subtype.val ⁻¹' t) ↔ s ∩ closure (s ∩ t) ⊆ t
• Topology.IsClosedEmbedding.inclusion 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hst : s ⊆ t) (hs : IsClosed (Subtype.val ⁻¹' s)) : Topology.IsClosedEmbedding (Set.inclusion hst)
• Topology.IsOpenEmbedding.inclusion 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s t : Set X} (hst : s ⊆ t) (hs : IsOpen (Subtype.val ⁻¹' s)) : Topology.IsOpenEmbedding (Set.inclusion hst)
• nhdsWithin_subtype_eq_bot_iff 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s t : Set X} {x : ↑s} : nhdsWithin x (Subtype.val ⁻¹' t) = ⊥ ↔ nhdsWithin (↑x) t ⊓ Filter.principal s = ⊥
• preimage_coe_mem_nhds_subtype 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} {a : ↑s} : Subtype.val ⁻¹' t ∈ nhds a ↔ t ∈ nhdsWithin (↑a) s
• Set.preimage_val_eq_univ_of_subset 📋 Mathlib.Data.Set.Subset
  {α : Type u_2} {A B : Set α} (h : A ⊆ B) : Subtype.val ⁻¹' B = Set.univ
• Set.image_val_preimage_val_subset_self 📋 Mathlib.Data.Set.Subset
  {α : Type u_2} {A B : Set α} : Subtype.val '' (Subtype.val ⁻¹' B) ⊆ B
• Set.preimage_val_image_val_eq_self 📋 Mathlib.Data.Set.Subset
  {α : Type u_2} {A : Set α} {D : Set ↑A} : Subtype.val ⁻¹' (Subtype.val '' D) = D
• Set.preimage_val_iInter 📋 Mathlib.Data.Set.Subset
  {ι : Sort u_1} {α : Type u_2} {A : Set α} {s : ι → Set α} : Subtype.val ⁻¹' ⋂ i, s i = ⋂ i, Subtype.val ⁻¹' s i
• Set.preimage_val_sInter_eq_sInter 📋 Mathlib.Data.Set.Subset
  {α : Type u_2} {A : Set α} {S : Set (Set α)} : Subtype.val ⁻¹' ⋂₀ S = ⋂₀ ((fun x => Subtype.val ⁻¹' x) '' S)
• Set.eq_of_preimage_val_eq_of_subset 📋 Mathlib.Data.Set.Subset
  {α : Type u_2} {A B C : Set α} (hB : B ⊆ A) (hC : C ⊆ A) (h : Subtype.val ⁻¹' B = Subtype.val ⁻¹' C) : B = C
• Set.subset_preimage_val_image_val_iff 📋 Mathlib.Data.Set.Subset
  {α : Type u_2} {A : Set α} {D E : Set ↑A} : D ⊆ Subtype.val ⁻¹' (Subtype.val '' E) ↔ D ⊆ E
• Set.preimage_val_sInter 📋 Mathlib.Data.Set.Subset
  {α : Type u_2} {A : Set α} {S : Set (Set α)} : Subtype.val ⁻¹' ⋂₀ S = ⋂₀ {x | ∃ B ∈ S, Subtype.val ⁻¹' B = x}
• Set.preimage_val_sUnion 📋 Mathlib.Data.Set.Subset
  {α : Type u_2} {A : Set α} {S : Set (Set α)} : Subtype.val ⁻¹' ⋃₀ S = ⋃₀ {x | ∃ B ∈ S, Subtype.val ⁻¹' B = x}
• IsClopen.biUnion_connectedComponentIn 📋 Mathlib.Topology.Connected.Clopen
  {X : Type u_3} [TopologicalSpace X] {u v : Set X} (hu : IsClopen (Subtype.val ⁻¹' u)) (huv₁ : u ⊆ v) : u = ⋃ x ∈ u, connectedComponentIn v x
• isClopen_preimage_val 📋 Mathlib.Topology.Connected.Clopen
  {X : Type u_3} [TopologicalSpace X] {u v : Set X} (hu : IsOpen u) (huv : Disjoint (frontier u) v) : IsClopen (Subtype.val ⁻¹' u)
• Topology.IsCoherentWith.of_isClosed 📋 Mathlib.Topology.Coherent
  {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} (h : ∀ (t : Set X), (∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)) → IsClosed t) : Topology.IsCoherentWith S
• Topology.IsCoherentWith.isClosed_iff 📋 Mathlib.Topology.Coherent
  {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} {t : Set X} (hS : Topology.IsCoherentWith S) : IsClosed t ↔ ∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)
• Topology.IsCoherentWith.isOpen_iff 📋 Mathlib.Topology.Coherent
  {X : Type u_1} [TopologicalSpace X] {S : Set (Set X)} {t : Set X} (hS : Topology.IsCoherentWith S) : IsOpen t ↔ ∀ s ∈ S, IsOpen (Subtype.val ⁻¹' t)
• isClosed_preimage_val_coborder 📋 Mathlib.Topology.LocallyClosed
  {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsClosed (Subtype.val ⁻¹' s)
• IsLocallyClosed.isOpen_preimage_val_closure 📋 Mathlib.Topology.LocallyClosed
  {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsLocallyClosed s) : IsOpen (Subtype.val ⁻¹' s)
• isLocallyClosed_tfae 📋 Mathlib.Topology.LocallyClosed
  {X : Type u_1} [TopologicalSpace X] (s : Set X) : [IsLocallyClosed s, IsOpen (coborder s), ∀ x ∈ s, ∃ U ∈ nhds x, IsClosed (Subtype.val ⁻¹' s), ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s, IsOpen (Subtype.val ⁻¹' s)].TFAE
• Topology.IsLocallyConstructible.of_isOpenCover 📋 Mathlib.Topology.Constructible
  {X : Type u_2} [TopologicalSpace X] {s : Set X} {ι : Type u_4} {U : ι → TopologicalSpace.Opens X} (hU : TopologicalSpace.IsOpenCover U) (H : ∀ (i : ι), Topology.IsLocallyConstructible (Subtype.val ⁻¹' s)) : Topology.IsLocallyConstructible s
• Topology.IsLocallyConstructible.iff_of_isOpenCover 📋 Mathlib.Topology.Constructible
  {X : Type u_2} [TopologicalSpace X] {s : Set X} {ι : Type u_4} {U : ι → TopologicalSpace.Opens X} (hU : TopologicalSpace.IsOpenCover U) : Topology.IsLocallyConstructible s ↔ ∀ (i : ι), Topology.IsLocallyConstructible (Subtype.val ⁻¹' s)
• MeasurableSet.image_inclusion' 📋 Mathlib.MeasureTheory.MeasurableSpace.Constructions
  {α : Type u_1} {m : MeasurableSpace α} {s t : Set α} (h : s ⊆ t) {u : Set ↑s} (hs : MeasurableSet (Subtype.val ⁻¹' s)) (hu : MeasurableSet u) : MeasurableSet (Set.inclusion h '' u)
• HasCountableSeparatingOn.subtype_iff 📋 Mathlib.Order.Filter.CountableSeparatingOn
  {α : Type u_1} {p : Set α → Prop} {t : Set α} : HasCountableSeparatingOn (↑t) (fun u => ∃ v, p v ∧ Subtype.val ⁻¹' v = u) Set.univ ↔ HasCountableSeparatingOn α p t
• HasCountableSeparatingOn.of_subtype 📋 Mathlib.Order.Filter.CountableSeparatingOn
  {α : Type u_1} {p : Set α → Prop} {t : Set α} {q : Set ↑t → Prop} [h : HasCountableSeparatingOn (↑t) q Set.univ] (hpq : ∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U) : HasCountableSeparatingOn α p t
• AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus 📋 Mathlib.AlgebraicGeometry.AffineScheme
  {X : AlgebraicGeometry.Scheme} (U : X.Opens) (s : Set ↑(X.presheaf.obj (Opposite.op U))) : ⇑(CategoryTheory.ConcreteCategory.hom U.toSpecΓ.base) ⁻¹' PrimeSpectrum.zeroLocus s = Subtype.val ⁻¹' X.zeroLocus s
• Measurable.measurableSet_preimage_iff_preimage_val 📋 Mathlib.MeasureTheory.Constructions.Polish.Basic
  {X : Type u_3} {Z : Type u_5} [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Z] {f : X → Z} [MeasurableSpace.CountablySeparated ↑(Set.range f)] (hf : Measurable f) {s : Set Z} : MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (Subtype.val ⁻¹' s)
• compactlyGeneratedSpace_of_isOpen_of_t2 📋 Mathlib.Topology.Compactness.CompactlyGeneratedSpace
  {X : Type u} [TopologicalSpace X] [T2Space X] (h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen (Subtype.val ⁻¹' s)) → IsOpen s) : CompactlyGeneratedSpace X
• Matroid.restrictSubtype_inter_indep_iff 📋 Mathlib.Data.Matroid.Map
  {α : Type u_1} {X I : Set α} {M : Matroid α} : (M.restrictSubtype X).Indep (Subtype.val ⁻¹' I) ↔ M.Indep (X ∩ I)
• Matroid.restrictSubtype_indep_iff_of_subset 📋 Mathlib.Data.Matroid.Map
  {α : Type u_1} {X I : Set α} {M : Matroid α} (hIX : I ⊆ X) : (M.restrictSubtype X).Indep (Subtype.val ⁻¹' I) ↔ M.Indep I
• Matroid.mapSetEquiv_indep_iff 📋 Mathlib.Data.Matroid.Map
  {α : Type u_1} {β : Type u_2} (M : Matroid α) {E : Set β} (e : ↑M.E ≃ ↑E) {I : Set β} : (M.mapSetEquiv e).Indep I ↔ M.Indep (Subtype.val '' (⇑e.symm '' (Subtype.val ⁻¹' I))) ∧ I ⊆ E
• Dynamics.coverEntropyInf_restrict_subset 📋 Mathlib.Dynamics.TopologicalEntropy.Semiconj
  {X : Type u_1} [UniformSpace X] {T : X → X} {F G : Set X} (hF : F ⊆ G) (hG : Set.MapsTo T G G) : Dynamics.coverEntropyInf (Set.MapsTo.restrict T G G hG) (Subtype.val ⁻¹' F) = Dynamics.coverEntropyInf T F
• Dynamics.coverEntropy_restrict_subset 📋 Mathlib.Dynamics.TopologicalEntropy.Semiconj
  {X : Type u_1} [UniformSpace X] {T : X → X} {F G : Set X} (hF : F ⊆ G) (hG : Set.MapsTo T G G) : Dynamics.coverEntropy (Set.MapsTo.restrict T G G hG) (Subtype.val ⁻¹' F) = Dynamics.coverEntropy T F
• Ordinal.accPt_subtype 📋 Mathlib.SetTheory.Ordinal.Topology
  {p o : Ordinal.{u_1}} (S : Set Ordinal.{u_1}) (hpo : p < o) : AccPt p (Filter.principal S) ↔ AccPt ⟨p, hpo⟩ (Filter.principal (Subtype.val ⁻¹' S))
• Topology.image_snd_preimageImageRestrict 📋 Mathlib.Topology.IsClosedRestrict
  {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι} [(i : ι) → TopologicalSpace (α i)] : Prod.snd '' (⇑(Homeomorph.preimageImageRestrict α S s) '' ((fun x => ↑x) ⁻¹' s)) = S.restrict '' 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 40fea08