Loogle!

Result

Found 89 declarations mentioning CategoryTheory.IsCofilteredOrEmpty.

CategoryTheory.IsCofilteredOrEmpty 📋 Mathlib.CategoryTheory.Filtered.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] : Prop
CategoryTheory.IsCofiltered.min 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] (j j' : C) : C
CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsCofiltered C] : CategoryTheory.IsCofilteredOrEmpty C
CategoryTheory.IsCofiltered.mk 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [toIsCofilteredOrEmpty : CategoryTheory.IsCofilteredOrEmpty C] [nonempty : Nonempty C] : CategoryTheory.IsCofiltered C
CategoryTheory.isCofilteredOrEmpty_of_isFilteredOrEmpty_op 📋 Mathlib.CategoryTheory.Filtered.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty Cᵒᵖ] : CategoryTheory.IsCofilteredOrEmpty C
CategoryTheory.isCofilteredOrEmpty_of_semilatticeInf 📋 Mathlib.CategoryTheory.Filtered.Basic
(α : Type u) [SemilatticeInf α] : CategoryTheory.IsCofilteredOrEmpty α
CategoryTheory.isCofilteredOrEmpty_op_of_isFilteredOrEmpty 📋 Mathlib.CategoryTheory.Filtered.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] : CategoryTheory.IsCofilteredOrEmpty Cᵒᵖ
CategoryTheory.isFilteredOrEmpty_of_isCofilteredOrEmpty_op 📋 Mathlib.CategoryTheory.Filtered.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty Cᵒᵖ] : CategoryTheory.IsFilteredOrEmpty C
CategoryTheory.isFilteredOrEmpty_op_of_isCofilteredOrEmpty 📋 Mathlib.CategoryTheory.Filtered.Basic
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] : CategoryTheory.IsFilteredOrEmpty Cᵒᵖ
CategoryTheory.isCofilteredOrEmpty_of_directed_ge 📋 Mathlib.CategoryTheory.Filtered.Basic
(α : Type u) [Preorder α] [IsCodirectedOrder α] : CategoryTheory.IsCofilteredOrEmpty α
CategoryTheory.IsCofilteredOrEmpty.of_equivalence 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (h : C ≌ D) : CategoryTheory.IsCofilteredOrEmpty D
CategoryTheory.instIsCofilteredOrEmptyForall 📋 Mathlib.CategoryTheory.Filtered.Basic
{α : Type w} {I : α → Type u₁} [(i : α) → CategoryTheory.Category.{v₁, u₁} (I i)] [∀ (i : α), CategoryTheory.IsCofilteredOrEmpty (I i)] : CategoryTheory.IsCofilteredOrEmpty ((i : α) → I i)
CategoryTheory.instIsCofilteredOrEmptyProd 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsCofilteredOrEmpty C] [CategoryTheory.IsCofilteredOrEmpty D] : CategoryTheory.IsCofilteredOrEmpty (C × D)
CategoryTheory.IsCofiltered.minToLeft 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] (j j' : C) : CategoryTheory.IsCofiltered.min j j' ⟶ j
CategoryTheory.IsCofiltered.minToRight 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] (j j' : C) : CategoryTheory.IsCofiltered.min j j' ⟶ j'
CategoryTheory.IsCofilteredOrEmpty.of_isLeftAdjoint 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (L : CategoryTheory.Functor C D) [L.IsLeftAdjoint] : CategoryTheory.IsCofilteredOrEmpty D
CategoryTheory.IsCofiltered.eq 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {j j' : C} (f f' : j ⟶ j') : C
CategoryTheory.IsCofilteredOrEmpty.of_left_adjoint 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) : CategoryTheory.IsCofilteredOrEmpty D
CategoryTheory.IsCofiltered.eqHom 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {j j' : C} (f f' : j ⟶ j') : CategoryTheory.IsCofiltered.eq f f' ⟶ j
CategoryTheory.IsCofilteredOrEmpty.cone_objs 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsCofilteredOrEmpty C] (X Y : C) : ∃ W x x, True
CategoryTheory.IsCofilteredOrEmpty.cone_maps 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsCofilteredOrEmpty C] ⦃X Y : C⦄ (f g : X ⟶ Y) : ∃ W h, CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g
CategoryTheory.IsCofiltered.eq_condition 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {j j' : C} (f f' : j ⟶ j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') f = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') f'
CategoryTheory.IsCofiltered.wideCospan 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {I : Type u_1} [Finite I] {i : C} {j : I → C} (f : (x : I) → j x ⟶ i) : ∃ k fki g, ∀ (x : I), CategoryTheory.CategoryStruct.comp (g x) (f x) = fki
CategoryTheory.IsCofiltered.cospan 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {i j j' : C} (f : j ⟶ i) (f' : j' ⟶ i) : ∃ k g g', CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp g' f'
CategoryTheory.IsCofiltered.eq_condition_assoc 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {j j' : C} (f f' : j ⟶ j') {Z : C} (h : j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCofiltered.eqHom f f') (CategoryTheory.CategoryStruct.comp f' h)
CategoryTheory.IsCofilteredOrEmpty.mk 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] (cone_objs : ∀ (X Y : C), ∃ W x x, True) (cone_maps : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ W h, CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) : CategoryTheory.IsCofilteredOrEmpty C
CategoryTheory.IsCofiltered.bowtie 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {j₁ j₂ k₁ k₂ : C} (f₁ : k₁ ⟶ j₁) (g₁ : k₂ ⟶ j₁) (f₂ : k₁ ⟶ j₂) (g₂ : k₂ ⟶ j₂) : ∃ s α β, CategoryTheory.CategoryStruct.comp α f₁ = CategoryTheory.CategoryStruct.comp β g₁ ∧ CategoryTheory.CategoryStruct.comp α f₂ = CategoryTheory.CategoryStruct.comp β g₂
CategoryTheory.Functor.ranges_directed 📋 Mathlib.CategoryTheory.Filtered.Basic
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] (F : CategoryTheory.Functor C (Type u_1)) (j : C) : Directed (fun x1 x2 => x1 ⊇ x2) fun f => Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f.snd))
CategoryTheory.IsCofilteredOrEmpty.of_initial 📋 Mathlib.CategoryTheory.Limits.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Initial] [CategoryTheory.IsCofilteredOrEmpty C] : CategoryTheory.IsCofilteredOrEmpty D
CategoryTheory.IsCofilteredOrEmpty.isPreconnected 📋 Mathlib.CategoryTheory.Filtered.Connected
(C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] : CategoryTheory.IsPreconnected C
CategoryTheory.IsCofiltered.over 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofilteredOrEmpty C] (c : C) : CategoryTheory.IsCofiltered (CategoryTheory.Over c)
CategoryTheory.Functor.initial_diag_of_isFiltered 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofilteredOrEmpty C] : (CategoryTheory.Functor.diag C).Initial
CategoryTheory.Over.initial_forget 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofilteredOrEmpty C] (c : C) : (CategoryTheory.Over.forget c).Initial
CategoryTheory.Functor.initial_iff_isCofiltered_costructuredArrow 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] : F.Initial ↔ ∀ (d : D), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)
CategoryTheory.instIsCofilteredCostructuredArrowProdDiagOfIsCofilteredOrEmpty 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsCofilteredOrEmpty C] (X : C × C) : CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag C) X)
CategoryTheory.CostructuredArrow.initial_proj_of_isCofiltered 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.IsCofilteredOrEmpty C] (T : CategoryTheory.Functor C D) [T.Initial] (Y : D) : (CategoryTheory.CostructuredArrow.proj T Y).Initial
CategoryTheory.IsCofilteredOrEmpty.of_exists_of_isCofiltered_of_fullyFaithful 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty D] [F.Full] [F.Faithful] (h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) : CategoryTheory.IsCofilteredOrEmpty C
CategoryTheory.Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty D] [F.Full] [F.Faithful] (h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) : F.Initial
CategoryTheory.Functor.Initial.exists_eq 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] [F.Initial] {d : D} {c : C} (s s' : F.obj c ⟶ d) : ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s'
CategoryTheory.Functor.initial_of_exists_of_isCofiltered 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] (h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) (h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s') : F.Initial
CategoryTheory.Functor.initial_iff_of_isCofiltered 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] : F.Initial ↔ (∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) ∧ ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s'
CategoryTheory.isCofiltered_costructuredArrow_of_isCofiltered_of_exists 📋 Mathlib.CategoryTheory.Filtered.Final
{C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C] (d : D) (h₁ : ∃ c, Nonempty (F.obj c ⟶ d)) (h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s') : CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)
CategoryTheory.initiallySmall_of_essentiallySmall_weakly_initial_objectProperty 📋 Mathlib.CategoryTheory.Limits.FinallySmall
{J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.IsCofilteredOrEmpty J] (P : CategoryTheory.ObjectProperty J) [CategoryTheory.ObjectProperty.EssentiallySmall.{v, v, u} P] (hP : ∀ (i : J), ∃ j, P j ∧ Nonempty (j ⟶ i)) : CategoryTheory.InitiallySmall J
CategoryTheory.initiallySmall_of_small_weakly_initial_set 📋 Mathlib.CategoryTheory.Limits.FinallySmall
{J : Type u} [CategoryTheory.Category.{v, u} J] [CategoryTheory.IsCofilteredOrEmpty J] (s : Set J) [Small.{v, u} ↑s] (hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)) : CategoryTheory.InitiallySmall J
CategoryTheory.initiallySmall_iff_exists_small_weakly_initial_set 📋 Mathlib.CategoryTheory.Limits.FinallySmall
(J : Type u) [CategoryTheory.Category.{v, u} J] [CategoryTheory.IsCofilteredOrEmpty J] : CategoryTheory.InitiallySmall J ↔ ∃ s, ∃ (_ : Small.{v, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
CategoryTheory.Over.isLimitConePost 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
{J : Type u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty J] {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cone F} (i : J) (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Limits.IsLimit ((CategoryTheory.Over.conePost F i).obj c)
AlgebraicGeometry.Scheme.nonempty_of_isLimit 📋 Mathlib.AlgebraicGeometry.AffineTransitionLimit
{I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofilteredOrEmpty I] [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] [∀ (i : I), Nonempty ↥(D.obj i)] [∀ (i : I), CompactSpace ↥(D.obj i)] : Nonempty ↥c.pt
AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty 📋 Mathlib.AlgebraicGeometry.AffineTransitionLimit
{I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofilteredOrEmpty I] [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] (Z : (i : I) → Set ↥(D.obj i)) (hZc : ∀ (i : I), IsClosed (Z i)) (hZne : ∀ (i : I), (Z i).Nonempty) (hZcpt : ∀ (i : I), IsCompact (Z i)) (hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')) : ∃ s, ∀ (i : I), (c.π.app i) s ∈ Z i
AlgebraicGeometry.exists_mem_of_isClosed_of_nonempty' 📋 Mathlib.AlgebraicGeometry.AffineTransitionLimit
{I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofilteredOrEmpty I] [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] {j : I} (Z : (i : I) → (i ⟶ j) → Set ↥(D.obj i)) (hZc : ∀ (i : I) (hij : i ⟶ j), IsClosed (Z i hij)) (hZne : ∀ (i : I) (hij : i ⟶ j), (Z i hij).Nonempty) (hZcpt : ∀ (i : I) (hij : i ⟶ j), IsCompact (Z i hij)) (hstab : ∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j), Set.MapsTo (⇑(D.map hi'i)) (Z i' (CategoryTheory.CategoryStruct.comp hi'i hij)) (Z i hij)) : ∃ s, ∀ (i : I) (hij : i ⟶ j), (c.π.app i) s ∈ Z i hij
TopCat.partialSections.nonempty 📋 Mathlib.Topology.Category.TopCat.Limits.Konig
{J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) [CategoryTheory.IsCofilteredOrEmpty J] [h : ∀ (j : J), Nonempty ↑(F.obj j)] {G : Finset J} (H : Finset (TopCat.FiniteDiagramArrow✝ G)) : (TopCat.partialSections F H).Nonempty
TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system 📋 Mathlib.Topology.Category.TopCat.Limits.Konig
{J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat) [CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Nonempty ↑(F.obj j)] [∀ (j : J), CompactSpace ↑(F.obj j)] [∀ (j : J), T2Space ↑(F.obj j)] : Nonempty ↑(TopCat.limitCone F).pt
CategoryTheory.Functor.toEventualRanges 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] : CategoryTheory.Functor J (Type v)
CategoryTheory.Functor.toEventualRanges_finite 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Finite (F.obj j)] (j : J) : Finite (F.toEventualRanges.obj j)
CategoryTheory.Functor.IsMittagLeffler.toPreimages 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} (s : Set (F.obj i)) [CategoryTheory.IsCofilteredOrEmpty J] (h : F.IsMittagLeffler) : (F.toPreimages s).IsMittagLeffler
CategoryTheory.Functor.toEventualRanges_nonempty 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] (h : F.IsMittagLeffler) [∀ (j : J), Nonempty (F.obj j)] (j : J) : Nonempty (F.toEventualRanges.obj j)
CategoryTheory.Functor.toEventualRanges_obj 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] (j : J) : F.toEventualRanges.obj j = ↑(F.eventualRange j)
nonempty_sections_of_finite_cofiltered_system 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{w, u} J] [CategoryTheory.IsCofilteredOrEmpty J] (F : CategoryTheory.Functor J (Type v)) [∀ (j : J), Finite (F.obj j)] [∀ (j : J), Nonempty (F.obj j)] : F.sections.Nonempty
nonempty_sections_of_finite_cofiltered_system.init 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCofilteredOrEmpty J] (F : CategoryTheory.Functor J (Type u)) [hf : ∀ (j : J), Finite (F.obj j)] [hne : ∀ (j : J), Nonempty (F.obj j)] : F.sections.Nonempty
CategoryTheory.Functor.toEventualRangesSectionsEquiv 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] : ↑F.toEventualRanges.sections ≃ ↑F.sections
CategoryTheory.Functor.eventualRange_mapsTo 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i j : J} [CategoryTheory.IsCofilteredOrEmpty J] (f : j ⟶ i) : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) (F.eventualRange j) (F.eventualRange i)
CategoryTheory.Functor.IsMittagLeffler.eq_image_eventualRange 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i j : J} [CategoryTheory.IsCofilteredOrEmpty J] (h : F.IsMittagLeffler) (f : j ⟶ i) : F.eventualRange i = ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) '' F.eventualRange j
CategoryTheory.Functor.isMittagLeffler_of_exists_finite_range 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] (h : ∀ (j : J), ∃ i f, (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))).Finite) : F.IsMittagLeffler
CategoryTheory.Functor.toPreimages_nonempty_of_surjective 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J} (s : Set (F.obj i)) [CategoryTheory.IsCofilteredOrEmpty J] [hFn : ∀ (j : J), Nonempty (F.obj j)] (Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) (hs : s.Nonempty) (j : J) : Nonempty ((F.toPreimages s).obj j)
CategoryTheory.Functor.surjective_toEventualRanges 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] (h : F.IsMittagLeffler) ⦃i j : J⦄ (f : i ⟶ j) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.toEventualRanges.map f))
CategoryTheory.Functor.thin_diagram_of_surjective 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] (Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) {i j : J} (f g : i ⟶ j) : F.map f = F.map g
CategoryTheory.Functor.eval_section_injective_of_eventually_injective 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] {j : J} (Finj : ∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) (i : J) (f : i ⟶ j) : Function.Injective fun s => ↑s j
CategoryTheory.Functor.toEventualRanges_map 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) : F.toEventualRanges.map f = TypeCat.ofHom (Set.MapsTo.restrict (⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) (F.eventualRange X✝) (F.eventualRange Y✝) ⋯)
CategoryTheory.Functor.eval_section_surjective_of_surjective 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Nonempty (F.obj j)] [∀ (j : J), Finite (F.obj j)] (Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) (i : J) : Function.Surjective fun s => ↑s i
CategoryTheory.Functor.eventually_injective 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Nonempty (F.obj j)] [∀ (j : J), Finite (F.obj j)] (Fsur : ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) [Nonempty J] [Finite ↑F.sections] : ∃ j, ∀ (i : J) (f : i ⟶ j), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))
CategoryTheory.Functor.isMittagLeffler_iff_subset_range_comp 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) [CategoryTheory.IsCofilteredOrEmpty J] : F.IsMittagLeffler ↔ ∀ (j : J), ∃ i f, ∀ ⦃k : J⦄ (g : k ⟶ i), Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CategoryStruct.comp g f)))
CategoryTheory.Functor.eventualRange_eq_iff 📋 Mathlib.CategoryTheory.CofilteredSystem
{J : Type u} [CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i j : J} [CategoryTheory.IsCofilteredOrEmpty J] {f : i ⟶ j} : F.eventualRange j = Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ↔ ∀ ⦃k : J⦄ (g : k ⟶ i), Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CategoryStruct.comp g f)))
CategoryTheory.IsCofiltered.cofilteredClosure 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} (f : α → C) : CategoryTheory.ObjectProperty C
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : Type (max u₁ v)
CategoryTheory.IsCofiltered.cofilteredClosure.base 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} {f : α → C} (x : α) : CategoryTheory.IsCofiltered.cofilteredClosure f (f x)
CategoryTheory.IsCofiltered.small_fullSubcategory_cofilteredClosure 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} (f : α → C) : Small.{max v w, u} (CategoryTheory.IsCofiltered.cofilteredClosure f).FullSubcategory
CategoryTheory.IsCofiltered.instSmallCategorySmallCofilteredIntermediate 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.SmallCategory (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F)
CategoryTheory.IsCofiltered.instEssentiallySmallFullSubcategoryCofilteredClosure 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} (f : α → C) : CategoryTheory.EssentiallySmall.{max v w, v, u} (CategoryTheory.IsCofiltered.cofilteredClosure f).FullSubcategory
CategoryTheory.IsCofiltered.instIsCofilteredOrEmptyFullSubcategoryCofilteredClosure 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} (f : α → C) : CategoryTheory.IsCofilteredOrEmpty (CategoryTheory.IsCofiltered.cofilteredClosure f).FullSubcategory
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instIsCofilteredOrEmpty 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.IsCofilteredOrEmpty (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F)
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoring 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Functor D (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F)
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : CategoryTheory.Functor (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F) C
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instOfNonempty 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) [Nonempty D] : CategoryTheory.IsCofiltered (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F)
CategoryTheory.IsCofiltered.cofilteredClosure.min 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} {f : α → C} {j j' : C} : CategoryTheory.IsCofiltered.cofilteredClosure f j → CategoryTheory.IsCofiltered.cofilteredClosure f j' → CategoryTheory.IsCofiltered.cofilteredClosure f (CategoryTheory.IsCofiltered.min j j')
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instFaithfulInclusion 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion F).Faithful
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instFullInclusion 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion F).Full
CategoryTheory.IsCofiltered.cofilteredClosure.eq 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {α : Type w} {f : α → C} {j j' : C} : CategoryTheory.IsCofiltered.cofilteredClosure f j → CategoryTheory.IsCofiltered.cofilteredClosure f j' → ∀ (f✝ f' : j ⟶ j'), CategoryTheory.IsCofiltered.cofilteredClosure f (CategoryTheory.IsCofiltered.eq f✝ f')
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoringCompInclusion 📋 Mathlib.CategoryTheory.Filtered.Small
{C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) : (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.factoring F).comp (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion F) ≅ F
CategoryTheory.PreGaloisCategory.PointedGaloisObject.instIsCofilteredOrEmpty 📋 Mathlib.CategoryTheory.Galois.Prorepresentability
{C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.GaloisCategory C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.IsCofilteredOrEmpty (CategoryTheory.PreGaloisCategory.PointedGaloisObject F)
CategoryTheory.WithTerminal.instIsCofilteredOfIsCofilteredOrEmpty 📋 Mathlib.CategoryTheory.WithTerminal.Lemmas
{C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsCofilteredOrEmpty C] : CategoryTheory.IsCofiltered (CategoryTheory.WithTerminal C)

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