Loogle!

Result

Found 22 declarations mentioning StarSubalgebra.map.

• StarSubalgebra.map_id 📋 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 : StarSubalgebra R A) : StarSubalgebra.map (StarAlgHom.id R A) S = S
• StarSubalgebra.map 📋 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 A) : StarSubalgebra R B
• StarAlgHom.range_eq_map_top 📋 Mathlib.Algebra.Star.Subalgebra
  {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R A] [StarModule R B] (φ : A →⋆ₐ[R] B) : φ.range = StarSubalgebra.map φ ⊤
• StarSubalgebra.gc_map_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) : GaloisConnection (StarSubalgebra.map f) (StarSubalgebra.comap f)
• StarSubalgebra.map_toSubalgebra 📋 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] {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} : (StarSubalgebra.map f S).toSubalgebra = Subalgebra.map f.toAlgHom S.toSubalgebra
• StarSubalgebra.map_injective 📋 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} (hf : Function.Injective ⇑f) : Function.Injective (StarSubalgebra.map f)
• StarSubalgebra.map_mono 📋 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] {S₁ S₂ : StarSubalgebra R A} {f : A →⋆ₐ[R] B} : S₁ ≤ S₂ → StarSubalgebra.map f S₁ ≤ StarSubalgebra.map f S₂
• StarSubalgebra.map_le_iff_le_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] {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} {U : StarSubalgebra R B} : StarSubalgebra.map f S ≤ U ↔ S ≤ StarSubalgebra.comap f U
• StarAlgHom.map_adjoin 📋 Mathlib.Algebra.Star.Subalgebra
  {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R A] [StarModule R B] (f : A →⋆ₐ[R] B) (s : Set A) : StarSubalgebra.map f (StarAlgebra.adjoin R s) = StarAlgebra.adjoin R (⇑f '' s)
• StarSubalgebra.coe_map 📋 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] (S : StarSubalgebra R A) (f : A →⋆ₐ[R] B) : ↑(StarSubalgebra.map f S) = ⇑f '' ↑S
• StarSubalgebra.map_sup 📋 Mathlib.Algebra.Star.Subalgebra
  {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (S T : StarSubalgebra R A) : StarSubalgebra.map f (S ⊔ T) = StarSubalgebra.map f S ⊔ StarSubalgebra.map f T
• StarSubalgebra.mem_map 📋 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] {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} {y : B} : y ∈ StarSubalgebra.map f S ↔ ∃ x ∈ S, f x = y
• StarSubalgebra.map_iInf 📋 Mathlib.Algebra.Star.Subalgebra
  {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] {ι : Sort u_5} [Nonempty ι] (f : A →⋆ₐ[R] B) (hf : Function.Injective ⇑f) (s : ι → StarSubalgebra R A) : StarSubalgebra.map f (iInf s) = ⨅ i, StarSubalgebra.map f (s i)
• StarSubalgebra.map_map 📋 Mathlib.Algebra.Star.Subalgebra
  {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] [Semiring C] [StarRing C] [Algebra R C] [StarModule R C] (S : StarSubalgebra R A) (g : B →⋆ₐ[R] C) (f : A →⋆ₐ[R] B) : StarSubalgebra.map g (StarSubalgebra.map f S) = StarSubalgebra.map (g.comp f) S
• StarSubalgebra.map_inf 📋 Mathlib.Algebra.Star.Subalgebra
  {R : Type u_2} {A : Type u_3} {B : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] (f : A →⋆ₐ[R] B) (hf : Function.Injective ⇑f) (S T : StarSubalgebra R A) : StarSubalgebra.map f (S ⊓ T) = StarSubalgebra.map f S ⊓ StarSubalgebra.map f T
• StarSubalgebra.topologicalClosure_map 📋 Mathlib.Topology.Algebra.StarSubalgebra
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] [IsTopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : Topology.IsClosedEmbedding ⇑φ) : (StarSubalgebra.map φ s).topologicalClosure = StarSubalgebra.map φ s.topologicalClosure
• StarSubalgebra.map_topologicalClosure_le 📋 Mathlib.Topology.Algebra.StarSubalgebra
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] [IsTopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : Continuous ⇑φ) : StarSubalgebra.map φ s.topologicalClosure ≤ (StarSubalgebra.map φ s).topologicalClosure
• StarSubalgebra.topologicalClosure_map_le 📋 Mathlib.Topology.Algebra.StarSubalgebra
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [TopologicalSpace A] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] [IsTopologicalSemiring A] [ContinuousStar A] [TopologicalSpace B] [Semiring B] [Algebra R B] [StarRing B] [StarModule R B] [IsTopologicalSemiring B] [ContinuousStar B] (s : StarSubalgebra R A) (φ : A →⋆ₐ[R] B) (hφ : IsClosedMap ⇑φ) : (StarSubalgebra.map φ s).topologicalClosure ≤ StarSubalgebra.map φ s.topologicalClosure
• BoundedContinuousFunction.separatesPoints_charPoly 📋 Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
  {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] [AddCommGroup W] [Module ℝ W] [TopologicalSpace W] {e : AddChar ℝ Circle} {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} (he : Continuous ⇑e) (he' : e ≠ 1) (hL : Continuous fun p => (L p.1) p.2) (hL' : ∀ (v : V), v ≠ 0 → L v ≠ 0) : (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ ℂ) (BoundedContinuousFunction.charPoly he hL)).SeparatesPoints
• RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict 📋 Mathlib.Analysis.RCLike.BoundedContinuous
  (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [PseudoEMetricSpace E] {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)} : Subalgebra.map (BoundedContinuousFunction.toContinuousMapₐ ℝ) (Subalgebra.comap (BoundedContinuousFunction.AlgHom.compLeftContinuousBounded ℝ RCLike.ofRealAm ⋯) (Subalgebra.restrictScalars ℝ A.toSubalgebra)) = Subalgebra.comap (AlgHom.compLeftContinuous ℝ RCLike.ofRealAm ⋯) (Subalgebra.restrictScalars ℝ (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).toSubalgebra)
• MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_polish 📋 Mathlib.MeasureTheory.Measure.FiniteMeasureExt
  {E : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [MeasurableSpace E] [TopologicalSpace E] [PolishSpace E] [BorelSpace E] {P P' : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure P'] {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)} (hA : (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).SeparatesPoints) (heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') : P = P'
• MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable 📋 Mathlib.MeasureTheory.Measure.FiniteMeasureExt
  {E : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [MeasurableSpace E] [PseudoEMetricSpace E] [BorelSpace E] [CompleteSpace E] [SecondCountableTopology E] {P P' : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure P'] {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)} (hA : (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).SeparatesPoints) (heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') : P = P'

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