Loogle!
Result
Found 7 declarations mentioning CategoryTheory.ComposableArrows.Mk₁.map.
- CategoryTheory.ComposableArrows.Mk₁.map 📋 Mathlib.CategoryTheory.ComposableArrows
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) (i j : Fin 2) : i ≤ j → (CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ i ⟶ CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ j) - CategoryTheory.ComposableArrows.Mk₁.map_id 📋 Mathlib.CategoryTheory.ComposableArrows
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) (i : Fin 2) : CategoryTheory.ComposableArrows.Mk₁.map f i i ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ i) - CategoryTheory.ComposableArrows.Mk₁.map.eq_2 📋 Mathlib.CategoryTheory.ComposableArrows
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) (isLt : 0 < 2) (isLt_1 : 1 < 2) (x_3 : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩) : CategoryTheory.ComposableArrows.Mk₁.map f ⟨0, isLt⟩ ⟨1, isLt_1⟩ x_3 = f - CategoryTheory.ComposableArrows.Mk₁.map_comp 📋 Mathlib.CategoryTheory.ComposableArrows
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) {i j k : Fin 2} (hij : i ≤ j) (hjk : j ≤ k) : CategoryTheory.ComposableArrows.Mk₁.map f i k ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.Mk₁.map f i j hij) (CategoryTheory.ComposableArrows.Mk₁.map f j k hjk) - CategoryTheory.ComposableArrows.Mk₁.map.eq_1 📋 Mathlib.CategoryTheory.ComposableArrows
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) (isLt isLt_1 : 0 < 2) (x_3 : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩) : CategoryTheory.ComposableArrows.Mk₁.map f ⟨0, isLt⟩ ⟨0, isLt_1⟩ x_3 = CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ ⟨0, isLt⟩) - CategoryTheory.ComposableArrows.Mk₁.map.eq_3 📋 Mathlib.CategoryTheory.ComposableArrows
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) (isLt isLt_1 : 1 < 2) (x_3 : ⟨1, isLt⟩ ≤ ⟨1, isLt_1⟩) : CategoryTheory.ComposableArrows.Mk₁.map f ⟨1, isLt⟩ ⟨1, isLt_1⟩ x_3 = CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.Mk₁.obj X₀ X₁ ⟨1, isLt⟩) - CategoryTheory.ComposableArrows.mk₁_map 📋 Mathlib.CategoryTheory.ComposableArrows
{C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) {X✝ Y✝ : Fin (1 + 1)} (g : X✝ ⟶ Y✝) : (CategoryTheory.ComposableArrows.mk₁ f).map g = CategoryTheory.ComposableArrows.Mk₁.map f X✝ Y✝ ⋯
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:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.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
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 findtsum_lt_tsum
even though the hypothesisf 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 40fea08