Loogle!

Result

Found 974 declarations whose name contains ".comap". Of these, 120 match your pattern(s).

• AddSubmonoid.comap 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N) : AddSubmonoid M
• Submonoid.comap 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) (S : Submonoid N) : Submonoid M
• AddSubgroup.comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_7} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : AddSubgroup G
• Subgroup.comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_7} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup G
• AddEquiv.comapAddSubgroup 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {H : Type u_5} [AddGroup H] (f : G ≃+ H) : AddSubgroup H ≃o AddSubgroup G
• MulEquiv.comapSubgroup 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {H : Type u_5} [Group H] (f : G ≃* H) : Subgroup H ≃o Subgroup G
• Setoid.comap 📋 Mathlib.Data.Setoid.Basic
  {α : Type u_1} {β : Type u_2} (f : α → β) (r : Setoid β) : Setoid α
• Setoid.comapQuotientEquiv 📋 Mathlib.Data.Setoid.Basic
  {α : Type u_1} {β : Type u_2} (f : α → β) (r : Setoid β) : Quotient (Setoid.comap f r) ≃ ↑(Set.range (Quotient.mk'' ∘ f))
• Submodule.comap 📋 Mathlib.Algebra.Module.Submodule.Map
  {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R₂ M₂) : Submodule R M
• Submodule.comapSubtypeEquivOfLe 📋 Mathlib.Algebra.Module.Submodule.Map
  {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} (hpq : p ≤ q) : ↥(Submodule.comap q.subtype p) ≃ₗ[R] ↥p
• AddSubsemigroup.comap 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) (S : AddSubsemigroup N) : AddSubsemigroup M
• Subsemigroup.comap 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) (S : Subsemigroup N) : Subsemigroup M
• NonUnitalSubsemiring.comap 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) (s : NonUnitalSubsemiring S) : NonUnitalSubsemiring R
• Subsemiring.comap 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (s : Subsemiring S) : Subsemiring R
• Subring.comap 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (s : Subring S) : Subring R
• Submodule.comap_equiv_self_of_inj_of_le 📋 Mathlib.Algebra.Module.Submodule.Equiv
  {R : Type u_1} {M : Type u_5} {N : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M →ₗ[R] N} {p : Submodule R N} (hf : Function.Injective ⇑f) (h : p ≤ LinearMap.range f) : ↥(Submodule.comap f p) ≃ₗ[R] ↥p
• AddCon.comap 📋 Mathlib.GroupTheory.Congruence.Defs
  {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M → N) (H : ∀ (x y : M), f (x + y) = f x + f y) (c : AddCon N) : AddCon M
• Con.comap 📋 Mathlib.GroupTheory.Congruence.Defs
  {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M → N) (H : ∀ (x y : M), f (x * y) = f x * f y) (c : Con N) : Con M
• AddCon.comapQuotientEquivOfSurj 📋 Mathlib.GroupTheory.Congruence.Basic
  {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (c : AddCon M) (f : N →+ M) (hf : Function.Surjective ⇑f) : (AddCon.comap ⇑f ⋯ c).Quotient ≃+ c.Quotient
• Con.comapQuotientEquivOfSurj 📋 Mathlib.GroupTheory.Congruence.Basic
  {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (c : Con M) (f : N →* M) (hf : Function.Surjective ⇑f) : (Con.comap ⇑f ⋯ c).Quotient ≃* c.Quotient
• AddCon.comapQuotientEquiv 📋 Mathlib.GroupTheory.Congruence.Basic
  {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (c : AddCon M) (f : N →+ M) : (AddCon.comap ⇑f ⋯ c).Quotient ≃+ ↥(AddMonoidHom.mrange (c.mk'.comp f))
• Con.comapQuotientEquiv 📋 Mathlib.GroupTheory.Congruence.Basic
  {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (c : Con M) (f : N →* M) : (Con.comap ⇑f ⋯ c).Quotient ≃* ↥(MonoidHom.mrange (c.mk'.comp f))
• RingCon.comap 📋 Mathlib.RingTheory.Congruence.Defs
  {R : Type u_2} {R' : Type u_3} {F : Type u_4} [Add R] [Add R'] [FunLike F R R'] [AddHomClass F R R'] [Mul R] [Mul R'] [MulHomClass F R R'] (J : RingCon R') (f : F) : RingCon R
• NonUnitalSubring.comap 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) (s : NonUnitalSubring S) : NonUnitalSubring R
• NonUnitalSubalgebra.comap 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) : NonUnitalSubalgebra R A
• Finsupp.comapDomain 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α → β) (l : β →₀ M) (hf : Set.InjOn f (f ⁻¹' ↑l.support)) : α →₀ M
• Finsupp.comapDomain.addMonoidHom 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {β : Type u_2} {M : Type u_5} [AddZeroClass M] {f : α → β} (hf : Function.Injective f) : (β →₀ M) →+ α →₀ M
• Finsupp.comapSMul 📋 Mathlib.Data.Finsupp.SMul
  {α : Type u_1} {M : Type u_3} {G : Type u_5} [Monoid G] [MulAction G α] [AddCommMonoid M] : SMul G (α →₀ M)
• Finsupp.comapMulAction 📋 Mathlib.Data.Finsupp.SMul
  {α : Type u_1} {M : Type u_3} {G : Type u_5} [Monoid G] [MulAction G α] [AddCommMonoid M] : MulAction G (α →₀ M)
• Finsupp.comapDistribMulAction 📋 Mathlib.Data.Finsupp.SMul
  {α : Type u_1} {M : Type u_3} {G : Type u_5} [Monoid G] [MulAction G α] [AddCommMonoid M] : DistribMulAction G (α →₀ M)
• Subalgebra.comap 📋 Mathlib.Algebra.Algebra.Subalgebra.Basic
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B) : Subalgebra R A
• Ideal.comap 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] (I : Ideal S) : Ideal R
• NonUnitalStarSubalgebra.comap 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) (S : NonUnitalStarSubalgebra R B) : NonUnitalStarSubalgebra R A
• DFinsupp.comapDomain 📋 Mathlib.Data.DFinsupp.Defs
  {ι : Type u} {β : ι → Type v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h) (f : Π₀ (i : ι), β i) : Π₀ (k : κ), β (h k)
• DFinsupp.comapDomain' 📋 Mathlib.Data.DFinsupp.Defs
  {ι : Type u} {β : ι → Type v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κ → ι) {h' : ι → κ} (hh' : Function.LeftInverse h' h) (f : Π₀ (i : ι), β i) : Π₀ (k : κ), β (h k)
• QuotientAddGroup.comapMk'OrderIso 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [hn : N.Normal] : AddSubgroup (G ⧸ N) ≃o { H // N ≤ H }
• QuotientGroup.comapMk'OrderIso 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [Group G] (N : Subgroup G) [hn : N.Normal] : Subgroup (G ⧸ N) ≃o { H // N ≤ H }
• Submodule.comapMkQOrderEmbedding 📋 Mathlib.LinearAlgebra.Quotient.Basic
  {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : Submodule R (M ⧸ p) ↪o Submodule R M
• Submodule.comapMkQRelIso 📋 Mathlib.LinearAlgebra.Quotient.Basic
  {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) : Submodule R (M ⧸ p) ≃o ↑(Set.Ici p)
• Filter.comap 📋 Mathlib.Order.Filter.Defs
  {α : Type u_1} {β : Type u_2} (m : α → β) (f : Filter β) : Filter α
• MonoidAlgebra.comapDistribMulActionSelf 📋 Mathlib.Algebra.MonoidAlgebra.Defs
  {k : Type u₁} {G : Type u₂} [Group G] [Semiring k] : DistribMulAction G (MonoidAlgebra k G)
• StarSubalgebra.comap 📋 Mathlib.Algebra.Star.Subalgebra
  {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] (f : A →⋆ₐ[R] B) (S : StarSubalgebra R B) : StarSubalgebra R A
• Subfield.comap 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) (s : Subfield L) : Subfield K
• CategoryTheory.Pi.comap 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) : CategoryTheory.Functor ((i : I) → C i) ((j : J) → C (h j))
• CategoryTheory.Pi.comapId 📋 Mathlib.CategoryTheory.Pi.Basic
  (I : Type w₀) (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] : CategoryTheory.Pi.comap C id ≅ CategoryTheory.Functor.id ((i : I) → C i)
• CategoryTheory.Pi.comapEvalIsoEval 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} (h : J → I) (j : J) : (CategoryTheory.Pi.comap C h).comp (CategoryTheory.Pi.eval (C ∘ h) j) ≅ CategoryTheory.Pi.eval C (h j)
• CategoryTheory.Pi.comapComp 📋 Mathlib.CategoryTheory.Pi.Basic
  {I : Type w₀} (C : I → Type u₁) [(i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₁} {K : Type w₂} (f : K → J) (g : J → I) : (CategoryTheory.Pi.comap C g).comp (CategoryTheory.Pi.comap (C ∘ g) f) ≅ CategoryTheory.Pi.comap C (g ∘ f)
• TwoSidedIdeal.comap 📋 Mathlib.RingTheory.TwoSidedIdeal.Operations
  {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] {F : Type u_3} [FunLike F R S] (f : F) [NonUnitalRingHomClass F R S] : TwoSidedIdeal S →o TwoSidedIdeal R
• Ultrafilter.comap 📋 Mathlib.Order.Filter.Ultrafilter.Defs
  {α : Type u} {β : Type v} {m : α → β} (u : Ultrafilter β) (inj : Function.Injective m) (large : Set.range m ∈ u) : Ultrafilter α
• UniformSpace.comap 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} (f : α → β) (u : UniformSpace β) : UniformSpace α
• Embedding.comapUniformSpace 📋 Mathlib.Topology.UniformSpace.UniformEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [u : UniformSpace β] (f : α → β) (h : Topology.IsEmbedding f) : UniformSpace α
• Topology.IsEmbedding.comapUniformSpace 📋 Mathlib.Topology.UniformSpace.UniformEmbedding
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [u : UniformSpace β] (f : α → β) (h : Topology.IsEmbedding f) : UniformSpace α
• CategoryTheory.GradedObject.comap 📋 Mathlib.CategoryTheory.GradedObject
  (C : Type u) [CategoryTheory.Category.{v, u} C] {I : Type u_1} {J : Type u_2} (h : J → I) : CategoryTheory.Functor (CategoryTheory.GradedObject I C) (CategoryTheory.GradedObject J C)
• CategoryTheory.GradedObject.comapEquiv 📋 Mathlib.CategoryTheory.GradedObject
  (C : Type u) [CategoryTheory.Category.{v, u} C] {β γ : Type w} (e : β ≃ γ) : CategoryTheory.GradedObject β C ≌ CategoryTheory.GradedObject γ C
• CategoryTheory.GradedObject.comapEq 📋 Mathlib.CategoryTheory.GradedObject
  (C : Type u) [CategoryTheory.Category.{v, u} C] {β γ : Type w} {f g : β → γ} (h : f = g) : CategoryTheory.GradedObject.comap C f ≅ CategoryTheory.GradedObject.comap C g
• TopologicalSpace.Opens.comap 📋 Mathlib.Topology.Sets.Opens
  {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) : FrameHom (TopologicalSpace.Opens β) (TopologicalSpace.Opens α)
• TopologicalSpace.OpenNhdsOf.comap 📋 Mathlib.Topology.Sets.Opens
  {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [TopologicalSpace β] (f : C(α, β)) (x : α) : LatticeHom (TopologicalSpace.OpenNhdsOf (f x)) (TopologicalSpace.OpenNhdsOf x)
• Sylow.comapOfInjective 📋 Mathlib.GroupTheory.Sylow
  {p : ℕ} {G : Type u_1} [Group G] (P : Sylow p G) {K : Type u_2} [Group K] (ϕ : K →* G) (hϕ : Function.Injective ⇑ϕ) (h : ↑P ≤ ϕ.range) : Sylow p K
• Sylow.comapOfKerIsPGroup 📋 Mathlib.GroupTheory.Sylow
  {p : ℕ} {G : Type u_1} [Group G] (P : Sylow p G) {K : Type u_2} [Group K] (ϕ : K →* G) (hϕ : IsPGroup p ↥ϕ.ker) (h : ↑P ≤ ϕ.range) : Sylow p K
• LTSeries.comap 📋 Mathlib.Order.RelSeries
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (p : LTSeries β) (f : α → β) (comap : ∀ ⦃x y : α⦄, f x < f y → x < y) (surjective : Function.Surjective f) : LTSeries α
• Sublattice.comap 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice β) : Sublattice α
• PrimeSpectrum.comapEquiv 📋 Mathlib.RingTheory.Spectrum.Prime.RingHom
  {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (e : R ≃+* S) : PrimeSpectrum R ≃o PrimeSpectrum S
• BooleanSubalgebra.comap 📋 Mathlib.Order.BooleanSubalgebra
  {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) (L : BooleanSubalgebra β) : BooleanSubalgebra α
• PrimeSpectrum.comap 📋 Mathlib.RingTheory.Spectrum.Prime.Topology
  {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) : C(PrimeSpectrum S, PrimeSpectrum R)
• IntermediateField.comap 📋 Mathlib.FieldTheory.IntermediateField.Basic
  {K : Type u_1} {L : Type u_2} {L' : Type u_3} [Field K] [Field L] [Field L'] [Algebra K L] [Algebra K L'] (f : L →ₐ[K] L') (S : IntermediateField K L') : IntermediateField K L
• LieSubalgebra.comap 📋 Mathlib.Algebra.Lie.Subalgebra
  {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {L₂ : Type w} [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (K₂ : LieSubalgebra R L₂) : LieSubalgebra R L
• LieSubmodule.comap 📋 Mathlib.Algebra.Lie.Submodule
  {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N' : LieSubmodule R L M') : LieSubmodule R L M
• LieIdeal.comap 📋 Mathlib.Algebra.Lie.Ideal
  {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieRing L'] [LieAlgebra R L'] [LieAlgebra R L] (f : L →ₗ⁅R⁆ L') (J : LieIdeal R L') : LieIdeal R L
• MeasurableSpace.comap 📋 Mathlib.MeasureTheory.MeasurableSpace.Basic
  {α : Type u_1} {β : Type u_2} (f : α → β) (m : MeasurableSpace β) : MeasurableSpace α
• IsUniformInducing.comapPseudoMetricSpace 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  {α : Type u_3} {β : Type u_4} [UniformSpace α] [m : PseudoMetricSpace β] (f : α → β) (h : IsUniformInducing f) : PseudoMetricSpace α
• Inducing.comapPseudoMetricSpace 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [m : PseudoMetricSpace β] {f : α → β} (hf : Topology.IsInducing f) : PseudoMetricSpace α
• Topology.IsInducing.comapPseudoMetricSpace 📋 Mathlib.Topology.MetricSpace.Pseudo.Constructions
  {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [m : PseudoMetricSpace β] {f : α → β} (hf : Topology.IsInducing f) : PseudoMetricSpace α
• IsUniformEmbedding.comapMetricSpace 📋 Mathlib.Topology.MetricSpace.Basic
  {α : Type u_2} {β : Type u_3} [UniformSpace α] [m : MetricSpace β] (f : α → β) (h : IsUniformEmbedding f) : MetricSpace α
• Embedding.comapMetricSpace 📋 Mathlib.Topology.MetricSpace.Basic
  {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [m : MetricSpace β] (f : α → β) (h : Topology.IsEmbedding f) : MetricSpace α
• Topology.IsEmbedding.comapMetricSpace 📋 Mathlib.Topology.MetricSpace.Basic
  {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [m : MetricSpace β] (f : α → β) (h : Topology.IsEmbedding f) : MetricSpace α
• MeasureTheory.OuterMeasure.comap 📋 Mathlib.MeasureTheory.OuterMeasure.Operations
  {α : Type u_1} {β : Type u_3} (f : α → β) : MeasureTheory.OuterMeasure β →ₗ[ENNReal] MeasureTheory.OuterMeasure α
• MeasureTheory.Measure.comap 📋 Mathlib.MeasureTheory.Measure.Comap
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) (μ : MeasureTheory.Measure β) : MeasureTheory.Measure α
• MeasureTheory.Measure.comapₗ 📋 Mathlib.MeasureTheory.Measure.Comap
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : MeasureTheory.Measure β →ₗ[ENNReal] MeasureTheory.Measure α
• AffineSubspace.comap 📋 Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
  {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (s : AffineSubspace k P₂) : AffineSubspace k P₁
• ZLattice.comap 📋 Mathlib.Algebra.Module.ZLattice.Basic
  (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) (e : F →ₗ[K] E) : Submodule ℤ F
• ZLattice.comap_equiv 📋 Mathlib.Algebra.Module.ZLattice.Basic
  (K : Type u_1) [NormedField K] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace K E] [NormedAddCommGroup F] [NormedSpace K F] (L : Submodule ℤ E) (e : F ≃ₗ[K] E) : ↥L ≃ₗ[ℤ] ↥(ZLattice.comap K L ↑e)
• MvPolynomial.comap 📋 Mathlib.Algebra.MvPolynomial.Comap
  {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) : (τ → R) → σ → R
• MvPolynomial.comapEquiv 📋 Mathlib.Algebra.MvPolynomial.Comap
  {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [CommSemiring R] (f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R) : (τ → R) ≃ (σ → R)
• AlgebraicGeometry.StructureSheaf.comapFun 📋 Mathlib.AlgebraicGeometry.StructureSheaf
  {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)) (hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier) (s : (x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations R ↑x) (y : ↥V) : AlgebraicGeometry.StructureSheaf.Localizations S ↑y
• AlgebraicGeometry.StructureSheaf.comap 📋 Mathlib.AlgebraicGeometry.StructureSheaf
  {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)) (hUV : V.carrier ⊆ ⇑(PrimeSpectrum.comap f) ⁻¹' U.carrier) : ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U)) →+* ↑((AlgebraicGeometry.Spec.structureSheaf S).val.obj (Opposite.op V))
• AlgebraicGeometry.Scheme.IdealSheafData.comap 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) : X.IdealSheafData
• AlgebraicGeometry.Scheme.IdealSheafData.comapIso 📋 Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
  {X Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y) : (I.comap f).subscheme ≅ CategoryTheory.Limits.pullback f I.subschemeι
• AddValuation.comap 📋 Mathlib.RingTheory.Valuation.Basic
  {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedAddCommMonoidWithTop Γ₀] {S : Type u_6} [Ring S] (f : S →+* R) (v : AddValuation R Γ₀) : AddValuation S Γ₀
• Valuation.comap 📋 Mathlib.RingTheory.Valuation.Basic
  {R : Type u_3} {Γ₀ : Type u_4} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀] {S : Type u_7} [Ring S] (f : S →+* R) (v : Valuation R Γ₀) : Valuation S Γ₀
• ValuationSubring.comap 📋 Mathlib.RingTheory.Valuation.ValuationSubring
  {K : Type u} [Field K] {L : Type u_1} [Field L] (A : ValuationSubring L) (f : K →+* L) : ValuationSubring K
• ConvexCone.comap 📋 Mathlib.Geometry.Convex.Cone.Basic
  {R : Type u_2} {M : Type u_4} {N : Type u_5} [Semiring R] [PartialOrder R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : M →ₗ[R] N) (C : ConvexCone R N) : ConvexCone R M
• LocallyConstant.comap 📋 Mathlib.Topology.LocallyConstant.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (g : LocallyConstant Y Z) : LocallyConstant X Z
• PointedCone.comap 📋 Mathlib.Geometry.Convex.Cone.Pointed
  {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [Module R E] [AddCommMonoid F] [Module R F] (f : E →ₗ[R] F) (C : PointedCone R F) : PointedCone R E
• ClosedSubmodule.comap 📋 Mathlib.Topology.Algebra.Module.ClosedSubmodule
  {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid M] [TopologicalSpace M] [Module R M] [AddCommMonoid N] [TopologicalSpace N] [Module R N] (f : M →L[R] N) (s : ClosedSubmodule R N) : ClosedSubmodule R M
• ProperCone.comap 📋 Mathlib.Analysis.Convex.Cone.Basic
  {R : Type u_1} {E : Type u_2} {F : Type u_3} [Semiring R] [PartialOrder R] [IsOrderedRing R] [AddCommMonoid E] [TopologicalSpace E] [Module R E] [AddCommMonoid F] [TopologicalSpace F] [Module R F] (f : E →L[R] F) (C : ProperCone R F) : ProperCone R E
• OpenAddSubgroup.comap 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] {N : Type u_2} [AddGroup N] [TopologicalSpace N] (f : G →+ N) (hf : Continuous ⇑f) (H : OpenAddSubgroup N) : OpenAddSubgroup G
• OpenSubgroup.comap 📋 Mathlib.Topology.Algebra.OpenSubgroup
  {G : Type u_1} [Group G] [TopologicalSpace G] {N : Type u_2} [Group N] [TopologicalSpace N] (f : G →* N) (hf : Continuous ⇑f) (H : OpenSubgroup N) : OpenSubgroup G
• Matroid.comap 📋 Mathlib.Data.Matroid.Map
  {α : Type u_1} {β : Type u_2} (N : Matroid β) (f : α → β) : Matroid α
• Matroid.comapOn 📋 Mathlib.Data.Matroid.Map
  {α : Type u_1} {β : Type u_2} (N : Matroid β) (E : Set α) (f : α → β) : Matroid α
• CategoryTheory.Subgroupoid.comap 📋 Mathlib.CategoryTheory.Groupoid.Subgroupoid
  {C : Type u} [CategoryTheory.Groupoid C] {D : Type u_1} [CategoryTheory.Groupoid D] (φ : CategoryTheory.Functor C D) (S : CategoryTheory.Subgroupoid D) : CategoryTheory.Subgroupoid C
• Mod_.comap 📋 Mathlib.CategoryTheory.Monoidal.Mod_
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {A B : C} [Mon_Class A] [Mon_Class B] (f : A ⟶ B) [IsMon_Hom f] : CategoryTheory.Functor (Mod_ D B) (Mod_ D A)
• SimpleGraph.comap 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V → W) (G : SimpleGraph W) : SimpleGraph V
• SimpleGraph.Hom.comap 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V → W) (G : SimpleGraph W) : SimpleGraph.comap f G →g G
• SimpleGraph.Embedding.comap 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ↪ W) (G : SimpleGraph W) : SimpleGraph.comap (⇑f) G ↪g G
• SimpleGraph.Iso.comap 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} (f : V ≃ W) (G : SimpleGraph W) : SimpleGraph.comap (⇑f.toEmbedding) G ≃g G
• SimpleGraph.Subgraph.comap 📋 Mathlib.Combinatorics.SimpleGraph.Subgraph
  {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G'.Subgraph) : G.Subgraph
• DFA.comap 📋 Mathlib.Computability.DFA
  {α : Type u} {σ : Type v} {α' : Type u_1} (f : α' → α) (M : DFA α σ) : DFA α' σ
• DiscreteQuotient.comap 📋 Mathlib.Topology.DiscreteQuotient
  {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (S : DiscreteQuotient Y) : DiscreteQuotient X
• LocallyConstant.comapAddMonoidHom 📋 Mathlib.Topology.LocallyConstant.Algebra
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [AddZeroClass Z] (f : C(X, Y)) : LocallyConstant Y Z →+ LocallyConstant X Z
• LocallyConstant.comapMonoidHom 📋 Mathlib.Topology.LocallyConstant.Algebra
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [MulOneClass Z] (f : C(X, Y)) : LocallyConstant Y Z →* LocallyConstant X Z
• LocallyConstant.comapRingHom 📋 Mathlib.Topology.LocallyConstant.Algebra
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} [Semiring Z] (f : C(X, Y)) : LocallyConstant Y Z →+* LocallyConstant X Z
• LocallyConstant.comapₐ 📋 Mathlib.Topology.LocallyConstant.Algebra
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} (R : Type u_7) [CommSemiring R] [Semiring Z] [Algebra R Z] (f : C(X, Y)) : LocallyConstant Y Z →ₐ[R] LocallyConstant X Z
• LocallyConstant.comapₗ 📋 Mathlib.Topology.LocallyConstant.Algebra
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_6} (R : Type u_7) [Semiring R] [AddCommMonoid Z] [Module R Z] (f : C(X, Y)) : LocallyConstant Y Z →ₗ[R] LocallyConstant X Z
• Filter.Realizer.comap 📋 Mathlib.Data.Analysis.Filter
  {α : Type u_1} {β : Type u_2} (m : α → β) {f : Filter β} (F : f.Realizer) : (Filter.comap m f).Realizer
• FirstOrder.Language.Substructure.comap 📋 Mathlib.ModelTheory.Substructures
  {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [L.Structure M] [L.Structure N] (φ : L.Hom M N) (S : L.Substructure N) : L.Substructure M
• SingularManifold.comap 📋 Mathlib.Geometry.Manifold.Bordism
  {X : Type u_1} [TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_4} {H : Type u_5} {M : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I k M] [CompactSpace M] [BoundarylessManifold I M] (s : SingularManifold X k I) {φ : M → s.M} (hφ : Continuous φ) : SingularManifold X k I
• NumberField.InfinitePlace.comap 📋 Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
  {k : Type u_1} [Field k] {K : Type u_2} [Field K] (w : NumberField.InfinitePlace K) (f : k →+* K) : NumberField.InfinitePlace k
• CompleteSublattice.comap 📋 Mathlib.Order.CompleteSublattice
  {α : Type u_1} {β : Type u_2} [CompleteLattice α] [CompleteLattice β] (f : CompleteLatticeHom α β) (L : CompleteSublattice β) : CompleteSublattice α
• ProbabilityTheory.Kernel.comapRight 📋 Mathlib.Probability.Kernel.Basic
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} {f : γ → β} (κ : ProbabilityTheory.Kernel α β) (hf : MeasurableEmbedding f) : ProbabilityTheory.Kernel α γ
• ProbabilityTheory.Kernel.comap 📋 Mathlib.Probability.Kernel.Composition.MapComap
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (g : γ → α) (hg : Measurable g) : ProbabilityTheory.Kernel γ β

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 2c2d6a2 serving mathlib revision ba454ce