Loogle!

Result

Found 24 declarations mentioning Subtype.map.

• Subtype.map 📋 Mathlib.Data.Subtype
  {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p a → q (f a)) : Subtype p → Subtype q
• Subtype.map_involutive 📋 Mathlib.Data.Subtype
  {α : Sort u_1} {p : α → Prop} {f : α → α} (h : ∀ (a : α), p a → p (f a)) (hf : Function.Involutive f) : Function.Involutive (Subtype.map f h)
• Subtype.map_id 📋 Mathlib.Data.Subtype
  {α : Sort u_1} {p : α → Prop} {h : ∀ (a : α), p a → p (id a)} : Subtype.map id h = id
• Subtype.map_injective 📋 Mathlib.Data.Subtype
  {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} {f : α → β} (h : ∀ (a : α), p a → q (f a)) (hf : Function.Injective f) : Function.Injective (Subtype.map f h)
• Subtype.map_coe 📋 Mathlib.Data.Subtype
  {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p a → q (f a)) (a✝ : Subtype p) : ↑(Subtype.map f h a✝) = f ↑a✝
• Subtype.map_def 📋 Mathlib.Data.Subtype
  {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p a → q (f a)) : Subtype.map f h = fun x => ⟨f ↑x, ⋯⟩
• Subtype.map_comp 📋 Mathlib.Data.Subtype
  {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {p : α → Prop} {q : β → Prop} {r : γ → Prop} {x : Subtype p} (f : α → β) (h : ∀ (a : α), p a → q (f a)) (g : β → γ) (l : ∀ (a : β), q a → r (g a)) : Subtype.map g l (Subtype.map f h x) = Subtype.map (g ∘ f) ⋯ x
• Equiv.coe_subtypeEquiv_eq_map 📋 Mathlib.Logic.Equiv.Basic
  {X : Sort u_9} {Y : Sort u_10} {p : X → Prop} {q : Y → Prop} (e : X ≃ Y) (h : ∀ (x : X), p x ↔ q (e x)) : ⇑(e.subtypeEquiv h) = Subtype.map ⇑e ⋯
• Subtype.map.eq_1 📋 Mathlib.Data.Set.Image
  {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p a → q (f a)) (x : Subtype p) : Subtype.map f h x = ⟨f ↑x, ⋯⟩
• 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})
• List.filter_attach 📋 Mathlib.Data.List.Basic
  {α : Type u} (l : List α) (p : α → Bool) : List.filter (fun x => p ↑x) l.attach = List.map (Subtype.map id ⋯) (List.filter p l).attach
• List.filter_attach' 📋 Mathlib.Data.List.Basic
  {α : Type u} (l : List α) (p : { a // a ∈ l } → Bool) [DecidableEq α] : List.filter p l.attach = List.map (Subtype.map id ⋯) (List.filter (fun x => decide (∃ (h : x ∈ l), p ⟨x, h⟩ = true)) l).attach
• Multiset.filter_attach 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (s : Multiset α) (p : α → Prop) [DecidablePred p] : Multiset.filter (fun a => p ↑a) s.attach = Multiset.map (Subtype.map id ⋯) (Multiset.filter p s).attach
• Multiset.filter_attach' 📋 Mathlib.Data.Multiset.Filter
  {α : Type u_1} (s : Multiset α) (p : { a // a ∈ s } → Prop) [DecidableEq α] [DecidablePred p] : Multiset.filter p s.attach = Multiset.map (Subtype.map id ⋯) (Multiset.filter (fun x => ∃ (h : x ∈ s), p ⟨x, h⟩) s).attach
• Finset.filter_attach' 📋 Mathlib.Data.Finset.Image
  {α : Type u_1} [DecidableEq α] (s : Finset α) (p : { x // x ∈ s } → Prop) [DecidablePred p] : Finset.filter p s.attach = Finset.map { toFun := Subtype.map id ⋯, inj' := ⋯ } {x ∈ s | ∃ (h : x ∈ s), p ⟨x, h⟩}.attach
• StarSubalgebra.inclusion_apply 📋 Mathlib.Algebra.Star.Subalgebra
  {R : Type u_2} {A : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂) (a✝ : ↥S₁) : (StarSubalgebra.inclusion h) a✝ = Subtype.map id h a✝
• Continuous.subtype_map 📋 Mathlib.Topology.Constructions
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : X → Prop} {f : X → Y} (h : Continuous f) {q : Y → Prop} (hpq : ∀ (x : X), p x → q (f x)) : Continuous (Subtype.map f hpq)
• Measurable.subtype_map 📋 Mathlib.MeasureTheory.MeasurableSpace.Constructions
  {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} {p : α → Prop} {q : β → Prop} (hf : Measurable f) (hpq : ∀ (x : α), p x → q (f x)) : Measurable (Subtype.map f hpq)
• unitary.map_apply 📋 Mathlib.Algebra.Star.Unitary
  {F : Type u_2} {R : Type u_3} {S : Type u_4} [Monoid R] [StarMul R] [Monoid S] [StarMul S] [FunLike F R S] [StarHomClass F R S] [MonoidHomClass F R S] (f : F) (a✝ : ↥(unitary R)) : (unitary.map f) a✝ = Subtype.map ⇑f ⋯ a✝
• cfcHomSuperset_apply 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A} (ha : p a) {s : Set R} (hs : spectrum R a ⊆ s) (a✝ : C(↑s, R)) : (cfcHomSuperset ha hs) a✝ = (cfcHom ha) (a✝.comp { toFun := Subtype.map id hs, continuous_toFun := ⋯ })
• cfcₙHomSuperset_apply 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
  {R : Type u_1} {A : Type u_2} {p : A → Prop} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a) {s : Set R} (hs : quasispectrum R a ⊆ s) (a✝ : ContinuousMapZero (↑s) R) : (cfcₙHomSuperset ha hs) a✝ = (cfcₙHom ha) (a✝.comp { toFun := Subtype.map id hs, continuous_toFun := ⋯, map_zero' := ⋯ })
• SpectrumRestricts.starAlgHom_apply 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
  {R : Type u} {S : Type v} {A : Type w} [Semifield R] [StarRing R] [TopologicalSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Semifield S] [StarRing S] [TopologicalSpace S] [IsTopologicalSemiring S] [ContinuousStar S] [Ring A] [StarRing A] [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] {a : A} (φ : C(↑(spectrum S a), S) →⋆ₐ[S] A) {f : C(S, R)} (h : SpectrumRestricts a ⇑f) (a✝ : C(↑(spectrum R a), R)) : (SpectrumRestricts.starAlgHom φ h) a✝ = φ ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp (a✝.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
• QuasispectrumRestricts.nonUnitalStarAlgHom_apply 📋 Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
  {R : Type u} {S : Type v} {A : Type w} [Semifield R] [StarRing R] [TopologicalSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Field S] [StarRing S] [TopologicalSpace S] [IsTopologicalRing S] [ContinuousStar S] [NonUnitalRing A] [StarRing A] [Algebra R S] [Module R A] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] {a : A} (φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A) {f : C(S, R)} (h : QuasispectrumRestricts a ⇑f) (a✝ : ContinuousMapZero (↑(quasispectrum R a)) R) : (QuasispectrumRestricts.nonUnitalStarAlgHom φ h) a✝ = φ ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯, map_zero' := ⋯ }.comp (a✝.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯, map_zero' := ⋯ }))
• Set.MapsTo.restrict.eq_1 📋 Mathlib.CategoryTheory.CofilteredSystem
  {α : Type u} {β : Type v} (f : α → β) (s : Set α) (t : Set β) (h : Set.MapsTo f s t) : Set.MapsTo.restrict f s t h = Subtype.map f h

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