Loogle!

Result

Found 15 declarations mentioning LocallyConstant.map.

• LocallyConstant.map 📋 Mathlib.Topology.LocallyConstant.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] (f : Y → Z) (g : LocallyConstant X Y) : LocallyConstant X Z
• LocallyConstant.map_id 📋 Mathlib.Topology.LocallyConstant.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] : LocallyConstant.map id = id
• LocallyConstant.map_apply 📋 Mathlib.Topology.LocallyConstant.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] (f : Y → Z) (g : LocallyConstant X Y) : ⇑(LocallyConstant.map f g) = f ∘ ⇑g
• LocallyConstant.map_comp 📋 Mathlib.Topology.LocallyConstant.Basic
  {X : Type u_1} [TopologicalSpace X] {Y₁ : Type u_5} {Y₂ : Type u_6} {Y₃ : Type u_7} (g : Y₂ → Y₃) (f : Y₁ → Y₂) : LocallyConstant.map g ∘ LocallyConstant.map f = LocallyConstant.map (g ∘ f)
• LocallyConstant.congrRight_apply 📋 Mathlib.Topology.LocallyConstant.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] (e : Y ≃ Z) (g : LocallyConstant X Y) : (LocallyConstant.congrRight e) g = LocallyConstant.map (⇑e) g
• LocallyConstant.congrRight_symm_apply 📋 Mathlib.Topology.LocallyConstant.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] (e : Y ≃ Z) (g : LocallyConstant X Z) : (LocallyConstant.congrRight e).symm g = LocallyConstant.map (⇑e.symm) g
• Profinite.exists_locallyConstant_finite_aux 📋 Mathlib.Topology.Category.Profinite.CofilteredLimit
  {J : Type v} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofiltered J] {F : CategoryTheory.Functor J Profinite} (C : CategoryTheory.Limits.Cone F) {α : Type u_1} [Finite α] (hC : CategoryTheory.Limits.IsLimit C) (f : LocallyConstant (↑C.pt.toTop) α) : ∃ j g, LocallyConstant.map (fun a b => if a = b then 0 else 1) f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g
• CompHausLike.LocallyConstant.functorToPresheaves_map_app 📋 Mathlib.Condensed.Discrete.LocallyConstant
  {P : TopCat → Prop} {X✝ Y✝ : Type (max u w)} (f : X✝ ⟶ Y✝) (x✝ : (CompHausLike P)ᵒᵖ) (t : { obj := fun x => match x with | Opposite.op S => LocallyConstant (↑S.toTop) X✝, map := fun {X Y} f g => LocallyConstant.comap (TopCat.Hom.hom f.unop) g, map_id := ⋯, map_comp := ⋯ }.obj x✝) : (CompHausLike.LocallyConstant.functorToPresheaves.map f).app x✝ t = LocallyConstant.map f t
• LocallyConstant.instPow.eq_1 📋 Mathlib.Topology.LocallyConstant.Algebra
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {α : Type u_3} [Pow Y α] : LocallyConstant.instPow = { pow := fun f n => LocallyConstant.map (fun x => x ^ n) f }
• LocallyConstant.smul.eq_1 📋 Mathlib.Topology.LocallyConstant.Algebra
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {α : Type u_3} [SMul α Y] : LocallyConstant.smul = { smul := fun n f => LocallyConstant.map (fun x => n • x) f }
• LocallyConstant.vadd.eq_1 📋 Mathlib.Topology.LocallyConstant.Algebra
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {α : Type u_3} [VAdd α Y] : LocallyConstant.vadd = { vadd := fun n f => LocallyConstant.map (fun x => n +ᵥ x) f }
• LocallyConstant.mapAddMonoidHom_apply 📋 Mathlib.Topology.LocallyConstant.Algebra
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} [AddZeroClass Y] [AddZeroClass Z] (f : Y →+ Z) (g : LocallyConstant X Y) : (LocallyConstant.mapAddMonoidHom f) g = LocallyConstant.map (⇑f) g
• LocallyConstant.mapMonoidHom_apply 📋 Mathlib.Topology.LocallyConstant.Algebra
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} [MulOneClass Y] [MulOneClass Z] (f : Y →* Z) (g : LocallyConstant X Y) : (LocallyConstant.mapMonoidHom f) g = LocallyConstant.map (⇑f) g
• LocallyConstant.mapAddMonoidHom.eq_1 📋 Mathlib.Topology.LocallyConstant.Algebra
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} [AddZeroClass Y] [AddZeroClass Z] (f : Y →+ Z) : LocallyConstant.mapAddMonoidHom f = { toFun := LocallyConstant.map ⇑f, map_zero' := ⋯, map_add' := ⋯ }
• LocallyConstant.mapMonoidHom.eq_1 📋 Mathlib.Topology.LocallyConstant.Algebra
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {Z : Type u_6} [MulOneClass Y] [MulOneClass Z] (f : Y →* Z) : LocallyConstant.mapMonoidHom f = { toFun := LocallyConstant.map ⇑f, map_one' := ⋯, map_mul' := ⋯ }

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