Loogle!

Result

Found 87 declarations mentioning CategoryTheory.Precoverage.ZeroHypercover.

CategoryTheory.Precoverage.ZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Precoverage C) (S : C) : Type (max (max u v) (w + 1))
CategoryTheory.Precoverage.ZeroHypercover.Small 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) : Prop
CategoryTheory.Precoverage.ZeroHypercover.instCategory 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} : CategoryTheory.Category.{max v w, max (max (w + 1) u) v} (J.ZeroHypercover S)
CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (self : J.ZeroHypercover S) : CategoryTheory.PreZeroHypercover S
CategoryTheory.Precoverage.ZeroHypercover.Hom 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Precoverage C) {S : C} (E : J.ZeroHypercover S) (F : J.ZeroHypercover S) : Type (max (max v w) w')
CategoryTheory.Precoverage.ZeroHypercover.instSmall 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) : E.Small
CategoryTheory.Precoverage.ZeroHypercover.Small.Index 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : Type w'
CategoryTheory.Precoverage.instSmallOfSmall 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Precoverage C) [J.Small] {S : C} (E : J.ZeroHypercover S) : E.Small
CategoryTheory.Precoverage.Small.mk 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} (zeroHypercoverSmall : ∀ {S : C} (E : J.ZeroHypercover S), E.Small) : J.Small
CategoryTheory.Precoverage.Small.zeroHypercoverSmall 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.Small] {S : C} (E : J.ZeroHypercover S) : E.Small
CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : J.ZeroHypercover S
CategoryTheory.Precoverage.ZeroHypercover.sum 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} [J.IsStableUnderSup] (E : J.ZeroHypercover S) (F : J.ZeroHypercover S) : J.ZeroHypercover S
CategoryTheory.Precoverage.ZeroHypercover.instSmallOfSmallI₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [Small.{w', w} E.I₀] : E.Small
CategoryTheory.Precoverage.ZeroHypercover.reindex 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} (E : J.ZeroHypercover T) {ι : Type w'} (e : ι ≃ E.I₀) : J.ZeroHypercover T
CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : CategoryTheory.Precoverage.ZeroHypercover.Small.Index E → E.I₀
CategoryTheory.Precoverage.ZeroHypercover.weaken 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {K L : CategoryTheory.Precoverage C} {X : C} (E : K.ZeroHypercover X) (h : K ≤ L) : L.ZeroHypercover X
CategoryTheory.Precoverage.ZeroHypercover.mk 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (toPreZeroHypercover : CategoryTheory.PreZeroHypercover S) (mem₀ : toPreZeroHypercover.presieve₀ ∈ J.coverings S) : J.ZeroHypercover S
CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] (K : CategoryTheory.Precoverage C) [K.HasPullbacks] {X Y : C} (E : K.ZeroHypercover X) (f : Y ⟶ X) : E.presieve₀.HasPullbacks f
CategoryTheory.Precoverage.ZeroHypercover.mem₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (self : J.ZeroHypercover S) : self.presieve₀ ∈ J.coverings S
CategoryTheory.Precoverage.ZeroHypercover.bind 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : (i : E.I₀) → J.ZeroHypercover (E.X i)) : J.ZeroHypercover T
CategoryTheory.Precoverage.ZeroHypercover.singleton 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} (f : S ⟶ T) (hf : CategoryTheory.Presieve.singleton f ∈ J.coverings T) : J.ZeroHypercover T
CategoryTheory.Precoverage.ZeroHypercover.isoMk 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {E F : J.ZeroHypercover S} (e : E.toPreZeroHypercover ≅ F.toPreZeroHypercover) : E ≅ F
CategoryTheory.Precoverage.ZeroHypercover.reindex_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} (E : J.ZeroHypercover T) {ι : Type w'} (e : ι ≃ E.I₀) : (E.reindex e).toPreZeroHypercover = E.reindex e
CategoryTheory.Precoverage.ZeroHypercover.sum_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} [J.IsStableUnderSup] (E : J.ZeroHypercover S) (F : J.ZeroHypercover S) : (E.sum F).toPreZeroHypercover = E.sum F.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.weaken_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {K L : CategoryTheory.Precoverage C} {X : C} (E : K.ZeroHypercover X) (h : K ≤ L) : (E.weaken h).toPreZeroHypercover = E.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.map 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Precoverage D} (F : CategoryTheory.Functor C D) (E : J.ZeroHypercover S) (h : J ≤ CategoryTheory.Precoverage.comap F K) : K.ZeroHypercover (F.obj S)
CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : E.restrictIndexOfSmall.toPreZeroHypercover = E.restrictIndex (CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun E)
CategoryTheory.Precoverage.ZeroHypercover.presieve₀_mem_of_iso 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.RespectsIso] {S : C} {E : J.ZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} (e : E.toPreZeroHypercover ≅ F) : F.presieve₀ ∈ J.coverings S
CategoryTheory.Precoverage.ZeroHypercover.pushforward 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderComposition] [J.HasIsos] {X Y : C} (f : X ⟶ Y) (hf : CategoryTheory.Presieve.singleton f ∈ J.coverings Y) (E : J.ZeroHypercover X) : J.ZeroHypercover Y
CategoryTheory.Precoverage.le_of_zeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J K : CategoryTheory.Precoverage C} (h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X) : J ≤ K
CategoryTheory.Precoverage.ZeroHypercover.Small.mem₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : (E.restrictIndex (CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun E)).presieve₀ ∈ J.coverings S
CategoryTheory.Precoverage.ZeroHypercover.id_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (x✝ : J.ZeroHypercover S) (a : x✝.I₀) : (CategoryTheory.CategoryStruct.id x✝).s₀ a = a
CategoryTheory.Precoverage.ZeroHypercover.pullback₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] : J.ZeroHypercover S
CategoryTheory.Precoverage.ZeroHypercover.pullback₂ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] : J.ZeroHypercover S
CategoryTheory.Precoverage.ZeroHypercover.Small.exists_restrictIndex_mem 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [self : E.Small] : ∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S
CategoryTheory.Precoverage.ZeroHypercover.Small.mk 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {E : J.ZeroHypercover S} (exists_restrictIndex_mem : ∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S) : E.Small
CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {X : C} {R : CategoryTheory.Presieve X} : R ∈ J.coverings X ↔ ∃ 𝒰, R = CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f
CategoryTheory.Precoverage.ZeroHypercover.instSmallPullback₁ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] {T : C} (f : T ⟶ S) [J.IsStableUnderBaseChange] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f E).Small
CategoryTheory.Precoverage.ZeroHypercover.pushforward_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderComposition] [J.HasIsos] {X Y : C} (f : X ⟶ Y) (hf : CategoryTheory.Presieve.singleton f ∈ J.coverings Y) (E : J.ZeroHypercover X) : (CategoryTheory.Precoverage.ZeroHypercover.pushforward f hf E).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.pushforward f E.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.add 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) {T : C} (f : T ⟶ S) (hf : E.presieve₀ ⊔ CategoryTheory.Presieve.singleton f ∈ J.coverings S) : J.ZeroHypercover S
CategoryTheory.Precoverage.ZeroHypercover.map_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Precoverage D} (F : CategoryTheory.Functor C D) (E : J.ZeroHypercover S) (h : J ≤ CategoryTheory.Precoverage.comap F K) : (CategoryTheory.Precoverage.ZeroHypercover.map F E h).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.map F E.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.bind_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : (i : E.I₀) → J.ZeroHypercover (E.X i)) : (E.bind F).toPreZeroHypercover = E.bind fun i => (F i).toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f E).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.pullback₁ f E.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.pullback₂_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] : (CategoryTheory.Precoverage.ZeroHypercover.pullback₂ f E).toPreZeroHypercover = CategoryTheory.PreZeroHypercover.pullback₂ f E.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.inter 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : J.ZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] : J.ZeroHypercover T
CategoryTheory.Precoverage.ZeroHypercover.id_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (x✝ : J.ZeroHypercover S) (x✝¹ : x✝.I₀) : (CategoryTheory.CategoryStruct.id x✝).h₀ x✝¹ = CategoryTheory.CategoryStruct.id (x✝.X x✝¹)
CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {X : C} (E : J.ZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.fst f g)] : J.ZeroHypercover (CategoryTheory.Limits.pullback f g)
CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfRight 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {Y : C} (E : J.ZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.snd f g)] : J.ZeroHypercover (CategoryTheory.Limits.pullback f g)
CategoryTheory.Precoverage.ZeroHypercover.isoMk_hom 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {E F : J.ZeroHypercover S} (e : E.toPreZeroHypercover ≅ F.toPreZeroHypercover) : (CategoryTheory.Precoverage.ZeroHypercover.isoMk e).hom = e.hom
CategoryTheory.Precoverage.ZeroHypercover.isoMk_inv 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {E F : J.ZeroHypercover S} (e : E.toPreZeroHypercover ≅ F.toPreZeroHypercover) : (CategoryTheory.Precoverage.ZeroHypercover.isoMk e).inv = e.inv
CategoryTheory.Precoverage.ZeroHypercover.add_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) {T : C} (f : T ⟶ S) (hf : E.presieve₀ ⊔ CategoryTheory.Presieve.singleton f ∈ J.coverings S) : (E.add f hf).toPreZeroHypercover = E.add f
CategoryTheory.Precoverage.ZeroHypercover.inter_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C} [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : J.ZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] : (E.inter F).toPreZeroHypercover = E.inter F.toPreZeroHypercover
CategoryTheory.Precoverage.ZeroHypercover.comp_s₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {X✝ Y✝ Z✝ : J.ZeroHypercover S} (f : X✝.Hom Y✝.toPreZeroHypercover) (g : Y✝.Hom Z✝.toPreZeroHypercover) (a✝ : X✝.I₀) : (CategoryTheory.CategoryStruct.comp f g).s₀ a✝ = g.s₀ (f.s₀ a✝)
CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {X : C} (E : J.ZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.fst f g)] : (E.pullbackCoverOfLeft f g).toPreZeroHypercover = E.pullbackCoverOfLeft f g
CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfRight_toPreZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] {Y : C} (E : J.ZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.snd f g)] : (E.pullbackCoverOfRight f g).toPreZeroHypercover = E.pullbackCoverOfRight f g
CategoryTheory.Precoverage.ZeroHypercover.comp_h₀ 📋 Mathlib.CategoryTheory.Sites.Hypercover.Zero
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {X✝ Y✝ Z✝ : J.ZeroHypercover S} (f : X✝.Hom Y✝.toPreZeroHypercover) (g : Y✝.Hom Z✝.toPreZeroHypercover) (i : X✝.I₀) : (CategoryTheory.CategoryStruct.comp f g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))
CategoryTheory.GrothendieckTopology.OneHypercover.toZeroHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C} (E : J.OneHypercover S) : J.toPrecoverage.ZeroHypercover S
CategoryTheory.Precoverage.ZeroHypercover.toOneHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.HasPullbacks] : J.toGrothendieck.OneHypercover S
CategoryTheory.Precoverage.ZeroHypercover.toOneHypercover_toPreOneHypercover 📋 Mathlib.CategoryTheory.Sites.Hypercover.One
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.HasPullbacks] : E.toOneHypercover.toPreOneHypercover = E.toPreOneHypercover
CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small 📋 Mathlib.CategoryTheory.Sites.Coverage
{C : Type u_2} [CategoryTheory.Category.{v_1, u_2} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange] [J.HasPullbacks] [J.Small] (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)) : CategoryTheory.Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), CategoryTheory.Presieve.IsSheafFor P E.presieve₀
CategoryTheory.Precoverage.ZeroHypercover.morphismProperty 📋 Mathlib.CategoryTheory.Sites.MorphismProperty
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.Precoverage C} {X : C} {E : K.ZeroHypercover X} (i : E.I₀) : K.morphismProperty (E.f i)
CategoryTheory.MorphismProperty.IsLocalAtSource.of_zeroHypercover 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) (h : ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) : P f
CategoryTheory.MorphismProperty.iff_of_zeroHypercover_source 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) : P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)
CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercover 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) : P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)
CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff_of_zeroHypercover 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.RespectsIso] (H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover X), P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) : P.IsLocalAtSource K
CategoryTheory.MorphismProperty.of_zeroHypercover_source 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) [𝒰.Small] (h : ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) : P f
CategoryTheory.MorphismProperty.IsLocalAtTarget.of_isPullback 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) {X' : C} (i : 𝒰.I₀) {fst : X' ⟶ X} {snd : X' ⟶ 𝒰.X i} (h : CategoryTheory.IsPullback fst snd f (𝒰.f i)) (hf : P f) : P snd
CategoryTheory.MorphismProperty.IsLocalAtTarget.of_zeroHypercover 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) [K.HasPullbacks] (h : ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) : P f
CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) [K.HasPullbacks] : P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))
CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) [K.HasPullbacks] : P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))
CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_isStableUnderBaseChange 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [K.HasPullbacks] [P.IsStableUnderBaseChange] (H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), (∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) → P f) : P.IsLocalAtTarget K
CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_iff_of_zeroHypercover 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [K.HasPullbacks] [P.RespectsIso] (H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) : P.IsLocalAtTarget K
CategoryTheory.MorphismProperty.of_zeroHypercover_target 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [K.HasPullbacks] [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) [𝒰.Small] (h : ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) : P f
CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_small 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [P.RespectsIso] [K.Small] (h₁ : ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X), P f → ∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) (h₂ : ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X), (∀ (i : 𝒰.I₀), P (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)) → P f) : P.IsLocalAtSource K
CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_small 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {K : CategoryTheory.Precoverage C} [K.HasPullbacks] [P.RespectsIso] [K.Small] (h₁ : ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y), P f → ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) (h₂ : ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y), (∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) → P f) : P.IsLocalAtTarget K
CategoryTheory.eq_of_zeroHypercover_target 📋 Mathlib.CategoryTheory.MorphismProperty.Local
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasPullbacks C] {X Y S : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) {J : CategoryTheory.Precoverage C} (𝒰 : J.ZeroHypercover S) [J.IsStableUnderBaseChange] [(CategoryTheory.MorphismProperty.isomorphisms C).IsLocalAtTarget J] (H : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.pullback.map s (𝒰.f i) t (𝒰.f i) f (CategoryTheory.CategoryStruct.id (𝒰.X i)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯ = CategoryTheory.Limits.pullback.map s (𝒰.f i) t (𝒰.f i) g (CategoryTheory.CategoryStruct.id (𝒰.X i)) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) : f = g
CategoryTheory.Precoverage.ZeroHypercover.Hom.isSheafFor_iff 📋 Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {K : CategoryTheory.Precoverage C} [K.IsStableUnderBaseChange] {S : C} {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} {𝒰 : K.ZeroHypercover S} {𝒱 : K.ZeroHypercover S} (f : CategoryTheory.Precoverage.ZeroHypercover.Hom K 𝒰 𝒱) (H₁ : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f)) (H₂ : ∀ {X : C} (f : X ⟶ S), CategoryTheory.Presieve.IsSeparatedFor F (CategoryTheory.Presieve.ofArrows (CategoryTheory.Precoverage.ZeroHypercover.pullback₂ f 𝒰).X (CategoryTheory.Precoverage.ZeroHypercover.pullback₂ f 𝒰).f)) : CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒱.X 𝒱.f)
TopCat.isOpenEmbedding_f_zeroHypercover 📋 Mathlib.Topology.Category.TopCat.GrothendieckTopology
{X : TopCat} (E : TopCat.precoverage.ZeroHypercover X) (i : E.I₀) : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (E.f i))
TopCat.exists_mem_zeroHypercover_range 📋 Mathlib.Topology.Category.TopCat.GrothendieckTopology
{X : TopCat} (E : TopCat.precoverage.ZeroHypercover X) (x : ↑X) : ∃ i, x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (E.f i))
CategoryTheory.ObjectProperty.of_zeroHypercover 📋 Mathlib.CategoryTheory.ObjectProperty.SiteLocal
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocal K] {X : C} (𝒰 : K.ZeroHypercover X) (h : ∀ (i : 𝒰.I₀), P (𝒰.X i)) : P X
CategoryTheory.ObjectProperty.iff_of_zeroHypercover 📋 Mathlib.CategoryTheory.ObjectProperty.SiteLocal
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {K : CategoryTheory.Precoverage C} [P.IsLocal K] {X : C} (𝒰 : K.ZeroHypercover X) : P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
CategoryTheory.ObjectProperty.IsLocal.mk_of_zeroHypercover 📋 Mathlib.CategoryTheory.ObjectProperty.SiteLocal
{C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {K : CategoryTheory.Precoverage C} [P.IsClosedUnderIsomorphisms] (H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)) : P.IsLocal K
CategoryTheory.Precoverage.ZeroHypercover.hom_ext 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.toGrothendieck.Subcanonical] {X Y : C} (𝒰 : J.ZeroHypercover X) {f g : X ⟶ Y} (h : ∀ (i : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (𝒰.f i) f = CategoryTheory.CategoryStruct.comp (𝒰.f i) g) : f = g
CategoryTheory.Precoverage.ZeroHypercover.isPullback_of_forall_isPullback 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.toGrothendieck.Subcanonical] [CategoryTheory.Limits.HasPullbacks C] [J.IsStableUnderBaseChange] {P X Y Z : C} (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z) (g : Y ⟶ Z) (𝒰 : J.ZeroHypercover X) (H : ∀ (i : 𝒰.I₀), CategoryTheory.IsPullback (CategoryTheory.Limits.pullback.snd fst (𝒰.f i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst fst (𝒰.f i)) snd) (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) : CategoryTheory.IsPullback fst snd f g
CategoryTheory.Precoverage.ZeroHypercover.glueMorphisms 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.toGrothendieck.Subcanonical] {S T : C} (𝒰 : J.ZeroHypercover S) [𝒰.HasPullbacks] (f : (i : 𝒰.I₀) → 𝒰.X i ⟶ T) (hf : ∀ (i j : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f i) (𝒰.f j)) (f i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (f j)) : S ⟶ T
CategoryTheory.Precoverage.ZeroHypercover.f_glueMorphisms 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.toGrothendieck.Subcanonical] {S T : C} (𝒰 : J.ZeroHypercover S) [𝒰.HasPullbacks] (f : (i : 𝒰.I₀) → 𝒰.X i ⟶ T) (hf : ∀ (i j : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f i) (𝒰.f j)) (f i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (f j)) (i : 𝒰.I₀) : CategoryTheory.CategoryStruct.comp (𝒰.f i) (𝒰.glueMorphisms f hf) = f i
CategoryTheory.Precoverage.ZeroHypercover.f_glueMorphisms_assoc 📋 Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
{C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.toGrothendieck.Subcanonical] {S T : C} (𝒰 : J.ZeroHypercover S) [𝒰.HasPullbacks] (f : (i : 𝒰.I₀) → 𝒰.X i ⟶ T) (hf : ∀ (i j : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f i) (𝒰.f j)) (f i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (f j)) (i : 𝒰.I₀) {Z : C} (h : T ⟶ Z) : CategoryTheory.CategoryStruct.comp (𝒰.f i) (CategoryTheory.CategoryStruct.comp (𝒰.glueMorphisms f hf) h) = CategoryTheory.CategoryStruct.comp (f i) h

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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 find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c