Loogle!

Result

Found 8 declarations mentioning DirectLimit.map.

• DirectLimit.map 📋 Mathlib.Order.DirectedInverseSystem
  {ι : Type u_1} [Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)] [DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] [DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] [IsDirected ι fun x1 x2 => x1 ≤ x2] (ih : (i : ι) → F₁ i → F₂ i) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i), (f₂ i j h) (ih i x) = ih j ((f₁ i j h) x)) (z : DirectLimit F₁ f₁) : DirectLimit F₂ f₂
• DirectLimit.map_def 📋 Mathlib.Order.DirectedInverseSystem
  {ι : Type u_1} [Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)] [DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] [DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] [IsDirected ι fun x1 x2 => x1 ≤ x2] (ih : (i : ι) → F₁ i → F₂ i) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i), (f₂ i j h) (ih i x) = ih j ((f₁ i j h) x)) (x : (i : ι) × F₁ i) : DirectLimit.map f₁ f₂ ih compat ⟦x⟧ = ⟦⟨x.fst, ih x.fst x.snd⟩⟧
• DirectLimit.instSMul.eq_1 📋 Mathlib.Algebra.Colimit.DirectLimit
  {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirected ι fun x1 x2 => x1 ≤ x2] [(i : ι) → SMul R (G i)] [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] : DirectLimit.instSMul = { smul := fun r => DirectLimit.map f f (fun x x_1 => r • x_1) ⋯ }
• DirectLimit.instVAdd.eq_1 📋 Mathlib.Algebra.Colimit.DirectLimit
  {R : Type u_1} {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirected ι fun x1 x2 => x1 ≤ x2] [(i : ι) → VAdd R (G i)] [∀ (i j : ι) (h : i ≤ j), AddActionHomClass (T h) R (G i) (G j)] : DirectLimit.instVAdd = { vadd := fun r => DirectLimit.map f f (fun x x_1 => r +ᵥ x_1) ⋯ }
• DirectLimit.instAddMonoid.eq_1 📋 Mathlib.Algebra.Colimit.DirectLimit
  {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirected ι fun x1 x2 => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddMonoid (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : DirectLimit.instAddMonoid = { toAddSemigroup := DirectLimit.instAddSemigroupOfAddHomClass, toZero := DirectLimit.instZero, zero_add := ⋯, add_zero := ⋯, nsmul := fun n => DirectLimit.map f f (fun x x_1 => n • x_1) ⋯, nsmul_zero := ⋯, nsmul_succ := ⋯ }
• DirectLimit.instMonoid.eq_1 📋 Mathlib.Algebra.Colimit.DirectLimit
  {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirected ι fun x1 x2 => x1 ≤ x2] [Nonempty ι] [(i : ι) → Monoid (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] : DirectLimit.instMonoid = { toSemigroup := DirectLimit.instSemigroupOfMulHomClass, toOne := DirectLimit.instOne, one_mul := ⋯, mul_one := ⋯, npow := fun n => DirectLimit.map f f (fun x x_1 => x_1 ^ n) ⋯, npow_zero := ⋯, npow_succ := ⋯ }
• DirectLimit.instAddGroup.eq_1 📋 Mathlib.Algebra.Colimit.DirectLimit
  {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirected ι fun x1 x2 => x1 ≤ x2] [Nonempty ι] [(i : ι) → AddGroup (G i)] [∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] : DirectLimit.instAddGroup = { toAddMonoid := DirectLimit.instAddMonoid, neg := DirectLimit.map f f (fun x x_1 => -x_1) ⋯, sub := DirectLimit.map₂ f f f (fun x x1 x2 => x1 - x2) ⋯, sub_eq_add_neg := ⋯, zsmul := fun n => DirectLimit.map f f (fun x x_1 => n • x_1) ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
• DirectLimit.instGroup.eq_1 📋 Mathlib.Algebra.Colimit.DirectLimit
  {ι : Type u_2} [Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_4} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [(i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [IsDirected ι fun x1 x2 => x1 ≤ x2] [Nonempty ι] [(i : ι) → Group (G i)] [∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] : DirectLimit.instGroup = { toMonoid := DirectLimit.instMonoid, inv := DirectLimit.map f f (fun x x_1 => x_1⁻¹) ⋯, div := DirectLimit.map₂ f f f (fun x x1 x2 => x1 / x2) ⋯, div_eq_mul_inv := ⋯, zpow := fun n => DirectLimit.map f f (fun x x_1 => x_1 ^ n) ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }

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