Loogle!

Result

Found 1367 declarations mentioning CategoryTheory.ObjectProperty. Of these, only the first 200 are shown.

• CategoryTheory.ObjectProperty 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  (C : Type u) [CategoryTheory.CategoryStruct.{v, u} C] : Type u
• CategoryTheory.ObjectProperty.Nonempty 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) : Prop
• CategoryTheory.ObjectProperty.singleton 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (X : C) : CategoryTheory.ObjectProperty C
• CategoryTheory.ObjectProperty.Is 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : C) : Prop
• CategoryTheory.ObjectProperty.pair 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (X Y : C) : CategoryTheory.ObjectProperty C
• CategoryTheory.ObjectProperty.ofObj 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u'} (X : ι → C) : CategoryTheory.ObjectProperty C
• CategoryTheory.ObjectProperty.arbitrary 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.Nonempty] : C
• CategoryTheory.ObjectProperty.nonempty_of_prop 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : C} (h : P X) : P.Nonempty
• CategoryTheory.ObjectProperty.is_of_prop 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X : C} (hX : P X) : P.Is X
• CategoryTheory.ObjectProperty.prop_of_is 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : C) [P.Is X] : P X
• CategoryTheory.ObjectProperty.Is.mk 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : C} (prop : P X) : P.Is X
• CategoryTheory.ObjectProperty.Is.prop 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {inst✝ : CategoryTheory.CategoryStruct.{v, u} C} {P : CategoryTheory.ObjectProperty C} {X : C} [self : P.Is X] : P X
• CategoryTheory.ObjectProperty.exists_prop_of_nonempty 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.Nonempty] : ∃ X, P X
• CategoryTheory.ObjectProperty.is_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : C) : P.Is X ↔ P X
• CategoryTheory.ObjectProperty.Nonempty.exists_prop 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {inst✝ : CategoryTheory.CategoryStruct.{v, u} C} {P : CategoryTheory.ObjectProperty C} [self : P.Nonempty] : ∃ X, P X
• CategoryTheory.ObjectProperty.Nonempty.mk 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P : CategoryTheory.ObjectProperty C} (exists_prop : ∃ X, P X) : P.Nonempty
• CategoryTheory.ObjectProperty.nonempty_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.Nonempty ↔ ∃ X, P X
• CategoryTheory.ObjectProperty.prop_arbitrary 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.Nonempty] : P P.arbitrary
• CategoryTheory.ObjectProperty.ofObj_subtypeVal 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.ObjectProperty.ofObj Subtype.val = P
• CategoryTheory.ObjectProperty.inverseImage 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) : CategoryTheory.ObjectProperty C
• CategoryTheory.ObjectProperty.map 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) : CategoryTheory.ObjectProperty D
• CategoryTheory.ObjectProperty.strictMap 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) : CategoryTheory.ObjectProperty D
• CategoryTheory.ObjectProperty.singleton_le_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {X : C} {P : CategoryTheory.ObjectProperty C} : CategoryTheory.ObjectProperty.singleton X ≤ P ↔ P X
• CategoryTheory.ObjectProperty.le_def 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C} : P ≤ Q ↔ ∀ (X : C), P X → Q X
• CategoryTheory.ObjectProperty.Nonempty.mono 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C} [P.Nonempty] (hPQ : P ≤ Q) : Q.Nonempty
• CategoryTheory.ObjectProperty.ofObj_le_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u'} (X : ι → C) (P : CategoryTheory.ObjectProperty C) : CategoryTheory.ObjectProperty.ofObj X ≤ P ↔ ∀ (i : ι), P (X i)
• CategoryTheory.ObjectProperty.nonempty_of_lt 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C} (h : P < Q) : Q.Nonempty
• CategoryTheory.ObjectProperty.not_le_iff_exists 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C} : ¬P ≤ Q ↔ ∃ X, P X ∧ ¬Q X
• CategoryTheory.ObjectProperty.prop_map_obj 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) {X : C} (hX : P X) : P.map F (F.obj X)
• CategoryTheory.ObjectProperty.strictMap_obj 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) {X : C} (hX : P X) : P.strictMap F (F.obj X)
• CategoryTheory.ObjectProperty.strictMap.mk 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] {P : CategoryTheory.ObjectProperty C} {F : CategoryTheory.Functor C D} (X : C) (hX : P X) : P.strictMap F (F.obj X)
• CategoryTheory.ObjectProperty.instNonemptyMap 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) [P.Nonempty] : (P.map F).Nonempty
• CategoryTheory.ObjectProperty.instNonemptyStrictMap 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) [P.Nonempty] : (P.strictMap F).Nonempty
• CategoryTheory.ObjectProperty.prop_inverseImage_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (X : C) : P.inverseImage F X ↔ P (F.obj X)
• CategoryTheory.ObjectProperty.strictMap_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) (Y : D) : P.strictMap F Y ↔ ∃ X, P X ∧ F.obj X = Y
• CategoryTheory.ObjectProperty.strictMap_le_map 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) : P.strictMap F ≤ P.map F
• CategoryTheory.ObjectProperty.strictMap_singleton 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (X : C) (F : CategoryTheory.Functor C D) : (CategoryTheory.ObjectProperty.singleton X).strictMap F = CategoryTheory.ObjectProperty.singleton (F.obj X)
• CategoryTheory.ObjectProperty.prop_map_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) (Y : D) : P.map F Y ↔ ∃ X, P X ∧ Nonempty (F.obj X ≅ Y)
• CategoryTheory.ObjectProperty.strictMap_ofObj 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] {ι : Type u'} (X : ι → C) (F : CategoryTheory.Functor C D) : (CategoryTheory.ObjectProperty.ofObj X).strictMap F = CategoryTheory.ObjectProperty.ofObj (F.obj ∘ X)
• CategoryTheory.ObjectProperty.map_monotone 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] {P Q : CategoryTheory.ObjectProperty C} (h : P ≤ Q) (F : CategoryTheory.Functor C D) : P.map F ≤ Q.map F
• CategoryTheory.ObjectProperty.strictMap_monotone 📋 Mathlib.CategoryTheory.ObjectProperty.Basic
  {C : Type u} {D : Type u'} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v', u'} D] {P Q : CategoryTheory.ObjectProperty C} (h : P ≤ Q) (F : CategoryTheory.Functor C D) : P.strictMap F ≤ Q.strictMap F
• CategoryTheory.ObjectProperty.FullSubcategory 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : Type u
• CategoryTheory.ObjectProperty.FullSubcategory.category 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.Category.{v, u} P.FullSubcategory
• CategoryTheory.ObjectProperty.FullSubcategory.obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (self : P.FullSubcategory) : C
• CategoryTheory.ObjectProperty.FullSubcategory.mk 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (obj : C) (property : P obj) : P.FullSubcategory
• CategoryTheory.ObjectProperty.FullSubcategory.property 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (self : P.FullSubcategory) : P self.obj
• CategoryTheory.ObjectProperty.instNonemptyFullSubcategoryOfNonempty 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.Nonempty] : Nonempty P.FullSubcategory
• CategoryTheory.ObjectProperty.ι 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.Functor P.FullSubcategory C
• CategoryTheory.ObjectProperty.faithful_ι 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.ι.Faithful
• CategoryTheory.ObjectProperty.full_ι 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.ι.Full
• CategoryTheory.ObjectProperty.fullyFaithfulι 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.ι.FullyFaithful
• CategoryTheory.ObjectProperty.prop_ι_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : P.FullSubcategory) : P (P.ι.obj X)
• CategoryTheory.ObjectProperty.ι_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X : P.FullSubcategory} : P.ι.obj X = X.obj
• CategoryTheory.ObjectProperty.FullSubcategory.ext 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C} {x y : P.FullSubcategory} (obj : x.obj = y.obj) : x = y
• CategoryTheory.ObjectProperty.lift 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) : CategoryTheory.Functor C P.FullSubcategory
• CategoryTheory.ObjectProperty.FullSubcategory.ext_iff 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C} {x y : P.FullSubcategory} : x = y ↔ x.obj = y.obj
• CategoryTheory.ObjectProperty.isoMk 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} (e : X.obj ≅ Y.obj) : X ≅ Y
• CategoryTheory.ObjectProperty.ιOfLE 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') : CategoryTheory.Functor P.FullSubcategory P'.FullSubcategory
• CategoryTheory.ObjectProperty.faithful_ιOfLE 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') : (CategoryTheory.ObjectProperty.ιOfLE h).Faithful
• CategoryTheory.ObjectProperty.full_ιOfLE 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') : (CategoryTheory.ObjectProperty.ιOfLE h).Full
• CategoryTheory.ObjectProperty.fullyFaithfulιOfLE 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') : (CategoryTheory.ObjectProperty.ιOfLE h).FullyFaithful
• CategoryTheory.ObjectProperty.instFaithfulFullSubcategoryLift 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) [F.Faithful] : (P.lift F hF).Faithful
• CategoryTheory.ObjectProperty.instFullFullSubcategoryLift 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) [F.Full] : (P.lift F hF).Full
• CategoryTheory.ObjectProperty.homMk 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X.obj ⟶ Y.obj) : X ⟶ Y
• CategoryTheory.ObjectProperty.lift_obj_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C) : ((P.lift F hF).obj X).obj = F.obj X
• CategoryTheory.ObjectProperty.homMk_surjective 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} : Function.Surjective CategoryTheory.ObjectProperty.homMk
• CategoryTheory.ObjectProperty.liftCompιIso 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) : (P.lift F hF).comp P.ι ≅ F
• CategoryTheory.ObjectProperty.ιOfLE_obj_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') (X : P.FullSubcategory) : ((CategoryTheory.ObjectProperty.ιOfLE h).obj X).obj = X.obj
• CategoryTheory.ObjectProperty.FullSubcategory.id_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : P.FullSubcategory) : (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id X.obj
• CategoryTheory.ObjectProperty.ι_obj_lift_obj 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C) : P.ι.obj ((P.lift F hF).obj X) = F.obj X
• CategoryTheory.ObjectProperty.homMk_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X.obj ⟶ Y.obj) : (CategoryTheory.ObjectProperty.homMk f).hom = f
• CategoryTheory.ObjectProperty.instIsIsoHomFullSubcategory 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X ⟶ Y) [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.hom
• CategoryTheory.ObjectProperty.isIso_hom_iff 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X ⟶ Y) : CategoryTheory.IsIso f.hom ↔ CategoryTheory.IsIso f
• CategoryTheory.ObjectProperty.ιOfLECompιIso 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') : (CategoryTheory.ObjectProperty.ιOfLE h).comp P'.ι ≅ P.ι
• CategoryTheory.ObjectProperty.isoMk_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} (e : X.obj ≅ Y.obj) : (P.isoMk e).hom = CategoryTheory.ObjectProperty.homMk e.hom
• CategoryTheory.ObjectProperty.isoMk_inv 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} (e : X.obj ≅ Y.obj) : (P.isoMk e).inv = CategoryTheory.ObjectProperty.homMk e.inv
• CategoryTheory.ObjectProperty.ι_map 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} {f : X ⟶ Y} : P.ι.map f = f.hom
• CategoryTheory.ObjectProperty.liftCompιOfLEIso 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) {Q : CategoryTheory.ObjectProperty D} (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (h : P ≤ Q) : (P.lift F hF).comp (CategoryTheory.ObjectProperty.ιOfLE h) ≅ Q.lift F ⋯
• CategoryTheory.ObjectProperty.isoHom_inv_id_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.hom.hom e.inv.hom = CategoryTheory.CategoryStruct.id X.obj
• CategoryTheory.ObjectProperty.isoInv_hom_id_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) : CategoryTheory.CategoryStruct.comp e.inv.hom e.hom.hom = CategoryTheory.CategoryStruct.id Y.obj
• CategoryTheory.ObjectProperty.hom_ext 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y : P.FullSubcategory} {f g : X ⟶ Y} (h : f.hom = g.hom) : f = g
• CategoryTheory.ObjectProperty.hom_inv 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (f : X ⟶ Y) [CategoryTheory.IsIso f] : (CategoryTheory.inv f).hom = CategoryTheory.inv f.hom
• CategoryTheory.ObjectProperty.hom_ext_iff 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} {f g : X ⟶ Y} : f = g ↔ f.hom = g.hom
• CategoryTheory.ObjectProperty.isoHom_inv_id_hom_assoc 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) {Z : C} (h : X.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp e.hom.hom (CategoryTheory.CategoryStruct.comp e.inv.hom h) = h
• CategoryTheory.ObjectProperty.isoInv_hom_id_hom_assoc 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (e : X ≅ Y) {Z : C} (h : Y.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp e.inv.hom (CategoryTheory.CategoryStruct.comp e.hom.hom h) = h
• CategoryTheory.ObjectProperty.lift_map 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (P.lift F hF).map f = CategoryTheory.ObjectProperty.homMk (F.map f)
• CategoryTheory.ObjectProperty.FullSubcategory.comp_hom 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y Z : P.FullSubcategory} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
• CategoryTheory.ObjectProperty.ιOfLE_map 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P') {X✝ Y✝ : P.FullSubcategory} (f : X✝ ⟶ Y✝) : (CategoryTheory.ObjectProperty.ιOfLE h).map f = CategoryTheory.ObjectProperty.homMk f.hom
• CategoryTheory.ObjectProperty.ι_obj_lift_map 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) {X Y : C} (f : X ⟶ Y) : P.ι.map ((P.lift F hF).map f) = F.map f
• CategoryTheory.ObjectProperty.FullSubcategory.comp_hom_assoc 📋 Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {X Y Z : P.FullSubcategory} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : Z.obj ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
• CategoryTheory.FullSubcategory.concreteCategory 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_2} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.ConcreteCategory P.FullSubcategory fun X Y => FC X.obj Y.obj
• CategoryTheory.ObjectProperty.FullSubcategory.concreteCategory 📋 Mathlib.CategoryTheory.ConcreteCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_2} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [CategoryTheory.ConcreteCategory C FC] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.ConcreteCategory P.FullSubcategory fun X Y => FC X.obj Y.obj
• CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : Prop
• CategoryTheory.ObjectProperty.isoClosure 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.ObjectProperty C
• CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsIsoClosure 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.isoClosure.IsClosedUnderIsomorphisms
• CategoryTheory.ObjectProperty.instNonemptyIsoClosure 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.Nonempty] : P.isoClosure.Nonempty
• CategoryTheory.ObjectProperty.isoClosure_eq_self 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] : P.isoClosure = P
• CategoryTheory.ObjectProperty.prop_of_iso 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y) (hX : P X) : P Y
• CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms.mk 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} (of_iso : ∀ {X Y : C} (x : X ≅ Y), P X → P Y) : P.IsClosedUnderIsomorphisms
• CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms.of_iso 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C} [self : P.IsClosedUnderIsomorphisms] {X Y : C} : ∀ (x : X ≅ Y), P X → P Y
• CategoryTheory.ObjectProperty.isClosedUnderIsomorphisms_iff_isoClosure_eq_self 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.IsClosedUnderIsomorphisms ↔ P.isoClosure = P
• CategoryTheory.ObjectProperty.prop_iff_of_iso 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (e : X ≅ Y) : P X ↔ P Y
• CategoryTheory.ObjectProperty.le_isoClosure 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P ≤ P.isoClosure
• CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMap 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) : (P.map F).IsClosedUnderIsomorphisms
• CategoryTheory.ObjectProperty.prop_isoClosure_iff 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : C) : P.isoClosure X ↔ ∃ Y, ∃ (_ : P Y), Nonempty (X ≅ Y)
• CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsInverseImage 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor D C) [P.IsClosedUnderIsomorphisms] : (P.inverseImage F).IsClosedUnderIsomorphisms
• CategoryTheory.ObjectProperty.prop_isoClosure 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : C} (h : P X) (e : X ⟶ Y) [CategoryTheory.IsIso e] : P.isoClosure Y
• CategoryTheory.ObjectProperty.prop_of_isIso 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] (hX : P X) : P Y
• CategoryTheory.ObjectProperty.prop_iff_of_isIso 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : P X ↔ P Y
• CategoryTheory.ObjectProperty.isoClosure_strictMap 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) : (P.strictMap F).isoClosure = P.map F
• CategoryTheory.ObjectProperty.map_isoClosure 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) : P.isoClosure.map F = P.map F
• CategoryTheory.ObjectProperty.monotone_isoClosure 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.ObjectProperty C} (h : P ≤ Q) : P.isoClosure ≤ Q.isoClosure
• CategoryTheory.ObjectProperty.isoClosure_le_iff 📋 Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) [Q.IsClosedUnderIsomorphisms] : P.isoClosure ≤ Q ↔ P ≤ Q
• CategoryTheory.Functor.essImage 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : CategoryTheory.ObjectProperty D
• CategoryTheory.Functor.isoClosure_eq_essImage 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} : (CategoryTheory.ObjectProperty.isoClosure fun x => x ∈ Set.range F.obj) = F.essImage
• CategoryTheory.ObjectProperty.map_top 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : ⊤.map F = F.essImage
• CategoryTheory.Functor.essImage_eq_of_natIso 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F F' : CategoryTheory.Functor C D} (h : F ≅ F') : F.essImage = F'.essImage
• CategoryTheory.Functor.essImage_comp_of_essSurj 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} {E : Type u₃} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [F.EssSurj] : (F.comp G).essImage = G.essImage
• CategoryTheory.Functor.essImage_ι_comp 📋 Mathlib.CategoryTheory.EssentialImage
  {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) : (P.ι.comp F).essImage = P.map F
• CategoryTheory.ObjectProperty.fullSubcategoryCongr 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P') : P.FullSubcategory ≌ P'.FullSubcategory
• CategoryTheory.ObjectProperty.fullSubcategoryCongr_functor 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P') : (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).functor = CategoryTheory.ObjectProperty.ιOfLE ⋯
• CategoryTheory.ObjectProperty.fullSubcategoryCongr_inverse 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P') : (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).inverse = CategoryTheory.ObjectProperty.ιOfLE ⋯
• CategoryTheory.ObjectProperty.fullSubcategoryCongr_unitIso 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P') : (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id P.FullSubcategory)
• CategoryTheory.ObjectProperty.fullSubcategoryCongr_counitIso 📋 Mathlib.CategoryTheory.Equivalence
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P') : (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.ObjectProperty.ιOfLE ⋯).comp (CategoryTheory.ObjectProperty.ιOfLE ⋯))
• CategoryTheory.ObjectProperty.eqToHom_hom 📋 Mathlib.CategoryTheory.EqToHom
  {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] {P : CategoryTheory.ObjectProperty C} {X Y : P.FullSubcategory} (h : X = Y) : (CategoryTheory.eqToHom h).hom = CategoryTheory.eqToHom ⋯
• CategoryTheory.FullSubcategory.hasForget₂ 📋 Mathlib.CategoryTheory.ConcreteCategory.Forget
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [CategoryTheory.ConcreteCategory C FC] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.HasForget₂ P.FullSubcategory C
• CategoryTheory.ObjectProperty.FullSubcategory.hasForget₂ 📋 Mathlib.CategoryTheory.ConcreteCategory.Forget
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)} {CC : outParam (C → Type w)} [outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] [CategoryTheory.ConcreteCategory C FC] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.HasForget₂ P.FullSubcategory C
• CategoryTheory.locallySmall_fullSubcategory 📋 Mathlib.CategoryTheory.EssentiallySmall
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.LocallySmall.{w, v, u} P.FullSubcategory
• CategoryTheory.ObjectProperty.instHasZeroMorphismsFullSubcategory 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.Limits.HasZeroMorphisms P.FullSubcategory
• CategoryTheory.ObjectProperty.homMk_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P : CategoryTheory.ObjectProperty C) (X Y : P.FullSubcategory) : CategoryTheory.ObjectProperty.homMk 0 = 0
• CategoryTheory.ObjectProperty.zero_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (P : CategoryTheory.ObjectProperty C) (X Y : P.FullSubcategory) : CategoryTheory.InducedCategory.Hom.hom 0 = 0
• CategoryTheory.Preadditive.fullSubcategory 📋 Mathlib.CategoryTheory.Preadditive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (Z : CategoryTheory.ObjectProperty C) : CategoryTheory.Preadditive Z.FullSubcategory
• CategoryTheory.Linear.fullSubcategory 📋 Mathlib.CategoryTheory.Linear.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type w} [Semiring R] [CategoryTheory.Linear R C] (Z : CategoryTheory.ObjectProperty C) : CategoryTheory.Linear R Z.FullSubcategory
• CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsBot 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] : ⊥.IsClosedUnderIsomorphisms
• CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsTop 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] : ⊤.IsClosedUnderIsomorphisms
• CategoryTheory.ObjectProperty.nonempty_top 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] [Nonempty C] : ⊤.Nonempty
• CategoryTheory.ObjectProperty.ne_bot_iff_exists 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : ¬P = ⊥ ↔ ∃ X, P X
• CategoryTheory.ObjectProperty.nonempty_iff_ne_bot 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.Nonempty ↔ ¬P = ⊥
• CategoryTheory.ObjectProperty.not_nonempty_iff_eq_bot 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : ¬P.Nonempty ↔ P = ⊥
• CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsIInf 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Sort u_1} (P : α → CategoryTheory.ObjectProperty C) [∀ (a : α), (P a).IsClosedUnderIsomorphisms] : (⨅ a, P a).IsClosedUnderIsomorphisms
• CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsISup 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Sort u_1} (P : α → CategoryTheory.ObjectProperty C) [∀ (a : α), (P a).IsClosedUnderIsomorphisms] : (⨆ a, P a).IsClosedUnderIsomorphisms
• CategoryTheory.ObjectProperty.prop_iSup_iff 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Sort u_1} (P : α → CategoryTheory.ObjectProperty C) (X : C) : (⨆ a, P a) X ↔ ∃ a, P a X
• CategoryTheory.ObjectProperty.prop_inf_iff 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) (X : C) : (P ⊓ Q) X ↔ P X ∧ Q X
• CategoryTheory.ObjectProperty.prop_sup_iff 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) (X : C) : (P ⊔ Q) X ↔ P X ∨ Q X
• CategoryTheory.ObjectProperty.nonempty_iSup 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Sort u_1} (P : α → CategoryTheory.ObjectProperty C) (a : α) [(P a).Nonempty] : (⨆ a, P a).Nonempty
• CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMax 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms] : (P ⊔ Q).IsClosedUnderIsomorphisms
• CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMin 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms] : (P ⊓ Q).IsClosedUnderIsomorphisms
• CategoryTheory.ObjectProperty.nonempty_sup_left 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) [P.Nonempty] : (P ⊔ Q).Nonempty
• CategoryTheory.ObjectProperty.nonempty_sup_right 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) [Q.Nonempty] : (P ⊔ Q).Nonempty
• CategoryTheory.ObjectProperty.isoClosure_iSup 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] {α : Sort u_1} (P : α → CategoryTheory.ObjectProperty C) : (⨆ a, P a).isoClosure = ⨆ a, (P a).isoClosure
• CategoryTheory.ObjectProperty.ι_map_top 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : ⊤.map P.ι = P.isoClosure
• CategoryTheory.ObjectProperty.isoClosure_sup 📋 Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) : (P ⊔ Q).isoClosure = P.isoClosure ⊔ Q.isoClosure
• CategoryTheory.exactFunctor 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : CategoryTheory.ObjectProperty (CategoryTheory.Functor C D)
• CategoryTheory.leftExactFunctor 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : CategoryTheory.ObjectProperty (CategoryTheory.Functor C D)
• CategoryTheory.rightExactFunctor 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : CategoryTheory.ObjectProperty (CategoryTheory.Functor C D)
• CategoryTheory.exactFunctor_le_leftExactFunctor 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : CategoryTheory.exactFunctor C D ≤ CategoryTheory.leftExactFunctor C D
• CategoryTheory.exactFunctor_le_rightExactFunctor 📋 Mathlib.CategoryTheory.Limits.ExactFunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] : CategoryTheory.exactFunctor C D ≤ CategoryTheory.rightExactFunctor C D
• CategoryTheory.additiveFunctor 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  (C : Type u_1) (D : Type u_2) [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] : CategoryTheory.ObjectProperty (CategoryTheory.Functor C D)
• CategoryTheory.Functor.fullSubcategoryInclusion_additive 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] (Z : CategoryTheory.ObjectProperty C) : Z.ι.Additive
• CategoryTheory.Functor.instAdditiveFullSubcategoryLift 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor D C) [F.Additive] (P : CategoryTheory.ObjectProperty C) (hF : ∀ (X : D), P (F.obj X)) : (P.lift F hF).Additive
• CategoryTheory.exactFunctor_le_additiveFunctor 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.exactFunctor C D ≤ CategoryTheory.additiveFunctor C D
• CategoryTheory.leftExactFunctor_le_additiveFunctor 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.leftExactFunctor C D ≤ CategoryTheory.additiveFunctor C D
• CategoryTheory.rightExactFunctor_le_additiveFunctor 📋 Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
  (C : Type u₁) (D : Type u₂) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.rightExactFunctor C D ≤ CategoryTheory.additiveFunctor C D
• CategoryTheory.MonoidalCategory.fullSubcategory 📋 Mathlib.CategoryTheory.Monoidal.Category
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) (tensorUnit : P (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (tensorObj : ∀ (X Y : C), P X → P Y → P (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) : CategoryTheory.MonoidalCategory P.FullSubcategory
• CategoryTheory.Functor.fullSubcategoryInclusionLinear 📋 Mathlib.CategoryTheory.Linear.LinearFunctor
  (R : Type u_1) [Semiring R] {C : Type u_4} [CategoryTheory.Category.{v_3, u_4} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (Z : CategoryTheory.ObjectProperty C) : CategoryTheory.Functor.Linear R Z.ι
• CategoryTheory.ObjectProperty.op 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) : CategoryTheory.ObjectProperty Cᵒᵖ
• CategoryTheory.ObjectProperty.unop 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ) : CategoryTheory.ObjectProperty C
• CategoryTheory.ObjectProperty.subtypeOpEquiv 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) : Subtype P.op ≃ Subtype P
• CategoryTheory.ObjectProperty.op_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : Cᵒᵖ) : P.op X ↔ P (Opposite.unop X)
• CategoryTheory.ObjectProperty.unop_op 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.op.unop = P
• CategoryTheory.ObjectProperty.instNonemptyOppositeOp 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.Nonempty] : P.op.Nonempty
• CategoryTheory.ObjectProperty.unop_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ) (X : C) : P.unop X ↔ P (Opposite.op X)
• CategoryTheory.ObjectProperty.instNonemptyUnopOfOpposite 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ) [P.Nonempty] : P.unop.Nonempty
• CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsOppositeOp 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderIsomorphisms] : P.op.IsClosedUnderIsomorphisms
• CategoryTheory.ObjectProperty.op_unop 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ) : P.unop.op = P
• CategoryTheory.ObjectProperty.unop_singleton 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (X : Cᵒᵖ) : (CategoryTheory.ObjectProperty.singleton X).unop = CategoryTheory.ObjectProperty.singleton (Opposite.unop X)
• CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsUnopOfOpposite 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ) [P.IsClosedUnderIsomorphisms] : P.unop.IsClosedUnderIsomorphisms
• CategoryTheory.ObjectProperty.op_singleton 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (X : C) : (CategoryTheory.ObjectProperty.singleton X).op = CategoryTheory.ObjectProperty.singleton (Opposite.op X)
• CategoryTheory.ObjectProperty.op_injective 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C} (h : P.op = Q.op) : P = Q
• CategoryTheory.ObjectProperty.op_injective_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C} : P.op = Q.op ↔ P = Q
• CategoryTheory.ObjectProperty.unop_ofObj 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u_1} (X : ι → Cᵒᵖ) : (CategoryTheory.ObjectProperty.ofObj X).unop = CategoryTheory.ObjectProperty.ofObj fun i => Opposite.unop (X i)
• CategoryTheory.ObjectProperty.op_ofObj 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u_1} (X : ι → C) : (CategoryTheory.ObjectProperty.ofObj X).op = CategoryTheory.ObjectProperty.ofObj fun i => Opposite.op (X i)
• CategoryTheory.ObjectProperty.unop_injective 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty Cᵒᵖ} (h : P.unop = Q.unop) : P = Q
• CategoryTheory.ObjectProperty.unop_injective_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty Cᵒᵖ} : P.unop = Q.unop ↔ P = Q
• CategoryTheory.ObjectProperty.op_isoClosure 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.isoClosure.op = P.op.isoClosure
• CategoryTheory.ObjectProperty.unop_isoClosure 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty Cᵒᵖ) : P.isoClosure.unop = P.unop.isoClosure
• CategoryTheory.ObjectProperty.op_monotone 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C} (h : P ≤ Q) : P.op ≤ Q.op
• CategoryTheory.ObjectProperty.op_monotone_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty C} : P.op ≤ Q.op ↔ P ≤ Q
• CategoryTheory.ObjectProperty.opEquivalence 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.op.FullSubcategory ≌ P.FullSubcategoryᵒᵖ
• CategoryTheory.ObjectProperty.unop_monotone 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty Cᵒᵖ} (h : P ≤ Q) : P.unop ≤ Q.unop
• CategoryTheory.ObjectProperty.unop_monotone_iff 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty Cᵒᵖ} : P.unop ≤ Q.unop ↔ P ≤ Q
• CategoryTheory.ObjectProperty.op_inf 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) : (P ⊓ Q).op = P.op ⊓ Q.op
• CategoryTheory.ObjectProperty.op_sup 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C) : (P ⊔ Q).op = P.op ⊔ Q.op
• CategoryTheory.ObjectProperty.unop_inf 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty Cᵒᵖ) : (P ⊓ Q).unop = P.unop ⊓ Q.unop
• CategoryTheory.ObjectProperty.unop_sup 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty Cᵒᵖ) : (P ⊔ Q).unop = P.unop ⊔ Q.unop
• CategoryTheory.ObjectProperty.opEquivalence_inverse 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.opEquivalence.inverse = P.op.lift P.ι.op ⋯
• CategoryTheory.ObjectProperty.opEquivalence_functor 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.opEquivalence.functor = (P.lift P.op.ι.leftOp ⋯).rightOp
• CategoryTheory.ObjectProperty.opEquivalence_unitIso 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.opEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id P.op.FullSubcategory)
• CategoryTheory.ObjectProperty.opEquivalence_counitIso 📋 Mathlib.CategoryTheory.ObjectProperty.Opposite
  {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) : P.opEquivalence.counitIso = CategoryTheory.Iso.refl ((P.op.lift P.ι.op ⋯).comp (P.lift P.op.ι.leftOp ⋯).rightOp)
• CategoryTheory.MorphismProperty.overObj 📋 Mathlib.CategoryTheory.MorphismProperty.Comma
  {T : Type u_3} [CategoryTheory.Category.{v_3, u_3} T] (W : CategoryTheory.MorphismProperty T) {X : T} : CategoryTheory.ObjectProperty (CategoryTheory.Over X)

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:

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.

5. 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