Loogle!

Result

Found 120 declarations mentioning Subtype, Set.preimage and Subtype.val. Of these, 63 match your pattern(s).

• Set.range_subtype_map 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (x : α), p x → q (f x)) : Set.range (Subtype.map f h) = Subtype.val ⁻¹' (f '' {x | p x})
• Subtype.preimage_coe_nonempty 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {s t : Set α} : (Subtype.val ⁻¹' t).Nonempty ↔ (s ∩ t).Nonempty
• Subtype.coe_preimage_self 📋 Mathlib.Data.Set.Image
  {α : Type u_1} (s : Set α) : Subtype.val ⁻¹' s = Set.univ
• Set.eq_preimage_subtype_val_iff 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {p : α → Prop} {s : Set (Subtype p)} {t : Set α} : s = Subtype.val ⁻¹' t ↔ ∀ (x : α) (h : p x), ⟨x, h⟩ ∈ s ↔ x ∈ t
• Subtype.image_preimage_coe 📋 Mathlib.Data.Set.Image
  {α : Type u_1} (s t : Set α) : Subtype.val '' (Subtype.val ⁻¹' t) = s ∩ t
• Subtype.image_preimage_val 📋 Mathlib.Data.Set.Image
  {α : Type u_1} (s t : Set α) : Subtype.val '' (Subtype.val ⁻¹' t) = s ∩ t
• Subtype.preimage_coe_compl 📋 Mathlib.Data.Set.Image
  {α : Type u_1} (s : Set α) : Subtype.val ⁻¹' sᶜ = ∅
• Subtype.preimage_coe_inter_self 📋 Mathlib.Data.Set.Image
  {α : Type u_1} (s t : Set α) : Subtype.val ⁻¹' (t ∩ s) = Subtype.val ⁻¹' t
• Subtype.preimage_coe_self_inter 📋 Mathlib.Data.Set.Image
  {α : Type u_1} (s t : Set α) : Subtype.val ⁻¹' (s ∩ t) = Subtype.val ⁻¹' t
• Subtype.preimage_coe_eq_empty 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {s t : Set α} : Subtype.val ⁻¹' t = ∅ ↔ s ∩ t = ∅
• Subtype.preimage_coe_eq_preimage_coe_iff 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {s t u : Set α} : Subtype.val ⁻¹' t = Subtype.val ⁻¹' u ↔ s ∩ t = s ∩ u
• Subtype.preimage_val_eq_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.preimage_subtype_coe_eq_compl 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {s u v : Set α} (hsuv : s ⊆ u ∪ v) (H : s ∩ (u ∩ v) = ∅) : Subtype.val ⁻¹' u = (Subtype.val ⁻¹' v)ᶜ
• Set.range_restrictPreimage 📋 Mathlib.Data.Set.Restrict
  {α : Type u_1} {β : Type u_2} (t : Set β) (f : α → β) : Set.range (t.restrictPreimage f) = Subtype.val ⁻¹' Set.range f
• Set.MapsTo.range_restrict 📋 Mathlib.Data.Set.Restrict
  {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β) (h : Set.MapsTo f s t) : Set.range (Set.MapsTo.restrict f s t h) = Subtype.val ⁻¹' (f '' 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)
• Equiv.Set.image_symm_preimage 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) (u s : Set α) : (fun x => ↑((Equiv.Set.image f s hf).symm x)) ⁻¹' u = Subtype.val ⁻¹' (f '' u)
• Set.preimage_subtype_val_Ici 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} [Preorder α] {p : α → Prop} (a : { x // p x }) : Subtype.val ⁻¹' Set.Ici ↑a = Set.Ici a
• Set.preimage_subtype_val_Iic 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} [Preorder α] {p : α → Prop} (a : { x // p x }) : Subtype.val ⁻¹' Set.Iic ↑a = Set.Iic a
• Set.preimage_subtype_val_Iio 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} [Preorder α] {p : α → Prop} (a : { x // p x }) : Subtype.val ⁻¹' Set.Iio ↑a = Set.Iio a
• Set.preimage_subtype_val_Ioi 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} [Preorder α] {p : α → Prop} (a : { x // p x }) : Subtype.val ⁻¹' Set.Ioi ↑a = Set.Ioi a
• Set.preimage_subtype_val_Icc 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} [Preorder α] {p : α → Prop} (a b : { x // p x }) : Subtype.val ⁻¹' Set.Icc ↑a ↑b = Set.Icc a b
• Set.preimage_subtype_val_Ico 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} [Preorder α] {p : α → Prop} (a b : { x // p x }) : Subtype.val ⁻¹' Set.Ico ↑a ↑b = Set.Ico a b
• Set.preimage_subtype_val_Ioc 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} [Preorder α] {p : α → Prop} (a b : { x // p x }) : Subtype.val ⁻¹' Set.Ioc ↑a ↑b = Set.Ioc a b
• Set.preimage_subtype_val_Ioo 📋 Mathlib.Order.Interval.Set.Image
  {α : Type u_1} [Preorder α] {p : α → Prop} (a b : { x // p x }) : Subtype.val ⁻¹' Set.Ioo ↑a ↑b = Set.Ioo a b
• AddSubmonoid.closure_closure_coe_preimage 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_5} [AddZeroClass M] {s : Set M} : AddSubmonoid.closure (Subtype.val ⁻¹' s) = ⊤
• Submonoid.closure_closure_coe_preimage 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_5} [MulOneClass M] {s : Set M} : Submonoid.closure (Subtype.val ⁻¹' s) = ⊤
• AddSubgroup.closure_closure_coe_preimage 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [AddGroup G] {k : Set G} : AddSubgroup.closure (Subtype.val ⁻¹' k) = ⊤
• Subgroup.closure_closure_coe_preimage 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] {k : Set G} : Subgroup.closure (Subtype.val ⁻¹' k) = ⊤
• SubAddAction.val_preimage_orbit 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {R : Type u} {M : Type v} [AddMonoid R] [AddAction R M] {p : SubAddAction R M} (m : ↥p) : Subtype.val ⁻¹' AddAction.orbit R ↑m = AddAction.orbit R m
• SubMulAction.val_preimage_orbit 📋 Mathlib.GroupTheory.GroupAction.SubMulAction
  {R : Type u} {M : Type v} [Monoid R] [MulAction R M] {p : SubMulAction R M} (m : ↥p) : Subtype.val ⁻¹' MulAction.orbit R ↑m = MulAction.orbit R m
• AddSubsemigroup.closure_closure_coe_preimage 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} [Add M] {s : Set M} : AddSubsemigroup.closure (Subtype.val ⁻¹' s) = ⊤
• Subsemigroup.closure_closure_coe_preimage 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} [Mul M] {s : Set M} : Subsemigroup.closure (Subtype.val ⁻¹' s) = ⊤
• Submodule.span_span_coe_preimage 📋 Mathlib.LinearAlgebra.Span.Defs
  {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} : Submodule.span R (Subtype.val ⁻¹' s) = ⊤
• Algebra.adjoin_adjoin_coe_preimage 📋 Mathlib.Algebra.Algebra.Subalgebra.Lattice
  {R : Type uR} {A : Type uA} [CommSemiring R] [Semiring A] [Algebra R A] {s : Set A} : Algebra.adjoin R (Subtype.val ⁻¹' s) = ⊤
• mem_nhds_subtype 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] (s : Set X) (x : { x // x ∈ s }) (t : Set { x // x ∈ s }) : t ∈ nhds x ↔ ∃ u ∈ nhds ↑x, Subtype.val ⁻¹' u ⊆ t
• isTopologicalBasis_subtype 📋 Mathlib.Topology.Bases
  {α : Type u_1} [TopologicalSpace α] {B : Set (Set α)} (h : TopologicalSpace.IsTopologicalBasis B) (p : α → Prop) : TopologicalSpace.IsTopologicalBasis (Set.preimage Subtype.val '' B)
• continuousOn_boolIndicator_iff_isClopen 📋 Mathlib.Topology.Clopen
  {X : Type u} [TopologicalSpace X] (s U : Set X) : ContinuousOn U.boolIndicator s ↔ IsClopen (Subtype.val ⁻¹' U)
• IsPathConnected.preimage_coe 📋 Mathlib.Topology.Connected.PathConnected
  {X : Type u_1} [TopologicalSpace X] {U W : Set X} (hW : IsPathConnected W) (hWU : W ⊆ U) : IsPathConnected (Subtype.val ⁻¹' W)
• PartialHomeomorph.subtypeRestr_source 📋 Mathlib.Topology.PartialHomeomorph
  {X : Type u_1} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (e : PartialHomeomorph X Y) {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s) : (e.subtypeRestr hs).source = Subtype.val ⁻¹' e.source
• TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage 📋 Mathlib.Topology.LocalAtTarget
  {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ι → TopologicalSpace.Opens β} (hU : TopologicalSpace.IsOpenCover U) {s : Set β} : IsClosed s ↔ ∀ (i : ι), IsClosed (Subtype.val ⁻¹' s)
• TopologicalSpace.IsOpenCover.isLocallyClosed_iff_coe_preimage 📋 Mathlib.Topology.LocalAtTarget
  {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ι → TopologicalSpace.Opens β} (hU : TopologicalSpace.IsOpenCover U) {s : Set β} : IsLocallyClosed s ↔ ∀ (i : ι), IsLocallyClosed (Subtype.val ⁻¹' s)
• TopologicalSpace.IsOpenCover.isOpen_iff_coe_preimage 📋 Mathlib.Topology.LocalAtTarget
  {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ι → TopologicalSpace.Opens β} {s : Set β} (hU : TopologicalSpace.IsOpenCover U) : IsOpen s ↔ ∀ (i : ι), IsOpen (Subtype.val ⁻¹' s)
• isClosed_iff_coe_preimage_of_iSup_eq_top 📋 Mathlib.Topology.LocalAtTarget
  {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ι → TopologicalSpace.Opens β} (hU : iSup U = ⊤) (s : Set β) : IsClosed s ↔ ∀ (i : ι), IsClosed (Subtype.val ⁻¹' s)
• isLocallyClosed_iff_coe_preimage_of_iSup_eq_top 📋 Mathlib.Topology.LocalAtTarget
  {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ι → TopologicalSpace.Opens β} (hU : iSup U = ⊤) (s : Set β) : IsLocallyClosed s ↔ ∀ (i : ι), IsLocallyClosed (Subtype.val ⁻¹' s)
• isOpen_iff_coe_preimage_of_iSup_eq_top 📋 Mathlib.Topology.LocalAtTarget
  {β : Type u_2} [TopologicalSpace β] {ι : Type u_3} {U : ι → TopologicalSpace.Opens β} (hU : iSup U = ⊤) (s : Set β) : IsOpen s ↔ ∀ (i : ι), IsOpen (Subtype.val ⁻¹' s)
• MeasurableSet.of_union_cover 📋 Mathlib.MeasureTheory.MeasurableSpace.Constructions
  {α : Type u_1} {m : MeasurableSpace α} {s t u : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) (h : Set.univ ⊆ s ∪ t) (hsu : MeasurableSet (Subtype.val ⁻¹' u)) (htu : MeasurableSet (Subtype.val ⁻¹' u)) : MeasurableSet u
• volume_preimage_coe 📋 Mathlib.MeasureTheory.Measure.Restrict
  {α : Type u_2} [MeasureTheory.MeasureSpace α] {s t : Set α} (hs : MeasureTheory.NullMeasurableSet s MeasureTheory.volume) (ht : MeasurableSet t) : MeasureTheory.volume (Subtype.val ⁻¹' t) = MeasureTheory.volume (t ∩ s)
• AffineSubspace.preimage_coe_affineSpan_singleton 📋 Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
  (k : Type u_1) (V : Type u_2) {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [S : AddTorsor V P] (x : P) : Subtype.val ⁻¹' {x} = Set.univ
• affineSpan_coe_preimage_eq_top 📋 Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
  {k : Type u_1} {V : Type u_2} {P : Type u_3} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (A : Set P) [Nonempty ↑A] : affineSpan k (Subtype.val ⁻¹' A) = ⊤
• AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
  {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] (f : A) (z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)) : AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun f ⁻¹' ↑(PrimeSpectrum.basicOpen (HomogeneousLocalization.mk z)) = Subtype.val ⁻¹' ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑z.num)
• AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen 📋 Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
  {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : ℕ → Submodule R A} [GradedAlgebra 𝒜] {f : A} (z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)) : ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f)) ⁻¹' ↑(PrimeSpectrum.basicOpen (HomogeneousLocalization.mk z)) = Subtype.val ⁻¹' ↑(ProjectiveSpectrum.basicOpen 𝒜 ↑z.num)
• LocallyConstant.piecewise'.eq_1 📋 Mathlib.Topology.LocallyConstant.Basic
  {X : Type u_1} {Z : Type u_3} [TopologicalSpace X] {C₀ C₁ C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂) (h₁ : IsClosed C₁) (h₂ : IsClosed C₂) (f₁ : LocallyConstant (↑C₁) Z) (f₂ : LocallyConstant (↑C₂) Z) [DecidablePred fun x => x ∈ C₁] (hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩) : LocallyConstant.piecewise' h₀ h₁ h₂ f₁ f₂ hf = LocallyConstant.piecewise ⋯ ⋯ ⋯ (LocallyConstant.comap { toFun := C₁.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₁) (LocallyConstant.comap { toFun := C₂.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₂) ⋯
• IsClosed.intrinsicClosure 📋 Mathlib.Analysis.Convex.Intrinsic
  {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} (hs : IsClosed (Subtype.val ⁻¹' s)) : intrinsicClosure 𝕜 s = s
• intrinsicClosure.eq_1 📋 Mathlib.Analysis.Convex.Intrinsic
  (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (s : Set P) : intrinsicClosure 𝕜 s = Subtype.val '' closure (Subtype.val ⁻¹' s)
• intrinsicFrontier.eq_1 📋 Mathlib.Analysis.Convex.Intrinsic
  (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (s : Set P) : intrinsicFrontier 𝕜 s = Subtype.val '' frontier (Subtype.val ⁻¹' s)
• intrinsicInterior.eq_1 📋 Mathlib.Analysis.Convex.Intrinsic
  (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] (s : Set P) : intrinsicInterior 𝕜 s = Subtype.val '' interior (Subtype.val ⁻¹' s)
• mem_intrinsicClosure 📋 Mathlib.Analysis.Convex.Intrinsic
  {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} {x : P} : x ∈ intrinsicClosure 𝕜 s ↔ ∃ y ∈ closure (Subtype.val ⁻¹' s), ↑y = x
• mem_intrinsicFrontier 📋 Mathlib.Analysis.Convex.Intrinsic
  {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} {x : P} : x ∈ intrinsicFrontier 𝕜 s ↔ ∃ y ∈ frontier (Subtype.val ⁻¹' s), ↑y = x
• mem_intrinsicInterior 📋 Mathlib.Analysis.Convex.Intrinsic
  {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [Ring 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace P] [AddTorsor V P] {s : Set P} {x : P} : x ∈ intrinsicInterior 𝕜 s ↔ ∃ y ∈ interior (Subtype.val ⁻¹' s), ↑y = x
• PFun.preimage_asSubtype 📋 Mathlib.Data.PFun
  {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) : f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s
• AddAction.IsBlock.subtype_val_preimage 📋 Mathlib.GroupTheory.GroupAction.Blocks
  {G : Type u_1} [AddGroup G] {X : Type u_2} [AddAction G X] {B : Set X} {C : SubAddAction G X} (hB : AddAction.IsBlock G B) : AddAction.IsBlock G (Subtype.val ⁻¹' B)
• MulAction.IsBlock.subtype_val_preimage 📋 Mathlib.GroupTheory.GroupAction.Blocks
  {G : Type u_1} [Group G] {X : Type u_2} [MulAction G X] {B : Set X} {C : SubMulAction G X} (hB : MulAction.IsBlock G B) : MulAction.IsBlock G (Subtype.val ⁻¹' B)

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 bce1d65