Image

📁 Source: Mathlib/CategoryTheory/Subfunctor/Image.lean

Statistics

Metric	Count
Definitions `fromPreimage`, `image`, `preimage`, `range`, `toRange`, `fromPreimage`, `image`, `preimage`, `range`, `toRange`	10
Theorems `epi_iff_range_eq_top`, `fromPreimage_ι`, `image_comp`, `image_iSup`, `image_le_iff`, `image_top`, `lift_ι`, `preimage_comp`, `preimage_eq_top_iff`, `preimage_id`, `preimage_image_of_epi`, `range_comp`, `range_comp_le`, `range_eq_top`, `range_id`, `range_toRange`, `range_ι`, `toRange_app_val`, `toRange_ι`, `epi_iff_range_eq_top`, `fromPreimage_ι`, `fromPreimage_ι_assoc`, `image_comp`, `image_iSup`, `image_le_iff`, `image_obj`, `image_top`, `instEpiFunctorTypeToRange`, `instIsIsoFunctorTypeToRangeOfMono`, `lift_app_coe`, `lift_ι`, `lift_ι_assoc`, `preimage_comp`, `preimage_eq_top_iff`, `preimage_id`, `preimage_image_of_epi`, `preimage_obj`, `range_comp`, `range_comp_le`, `range_eq_top`, `range_id`, `range_obj`, `range_toRange`, `range_ι`, `toRange_app_val`, `toRange_ι`, `toRange_ι_assoc`	47
Total	57

CategoryTheory.Subfunctor

Definitions

Name	Category	Theorems
`fromPreimage` 📖	CompOp	3 math math: `fromPreimage_ι`, `Subpresheaf.fromPreimage_ι`, `fromPreimage_ι_assoc`
`image` 📖	CompOp	19 math math: `preimage_image_of_epi`, `Subpresheaf.image_le_iff`, `image_comp`, `image_le_iff`, `Subpresheaf.image_top`, `image_isFinite`, `Subpresheaf.image_comp`, `Subpresheaf.range_comp`, `Subpresheaf.preimage_image_of_epi`, `Subpresheaf.IsGeneratedBy.image`, `image_top`, `Subpresheaf.image_isFinite`, `ofSection_image`, `image_iSup`, `image_obj`, `range_comp`, `Subpresheaf.ofSection_image`, `IsGeneratedBy.image`, `Subpresheaf.image_iSup`
`preimage` 📖	CompOp	14 math math: `Subpresheaf.preimage_id`, `Subpresheaf.preimage_eq_top_iff`, `preimage_image_of_epi`, `preimage_comp`, `Subpresheaf.image_le_iff`, `image_le_iff`, `preimage_id`, `preimage_obj`, `Subpresheaf.preimage_image_of_epi`, `fromPreimage_ι`, `Subpresheaf.preimage_comp`, `Subpresheaf.fromPreimage_ι`, `fromPreimage_ι_assoc`, `preimage_eq_top_iff`
`range` 📖	CompOp	56 math math: `Subpresheaf.range_eq_ofSection'`, `Subpresheaf.range_eq_ofSection`, `range_le_equalizer_iff`, `ofSection_eq_range`, `range_toRange`, `Subpresheaf.preimage_eq_top_iff`, `Subpresheaf.ofSection_eq_range'`, `CategoryTheory.Sheaf.imageι_val`, `range_ι`, `equivalenceMonoOver_inverse_map`, `range_eq_top`, `Subpresheaf.image_top`, `ofSection_eq_range'`, `equivalenceMonoOver_inverse_obj`, `Subpresheaf.range_comp`, `Subpresheaf.toRange_ι`, `CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top`, `range_eq_ofSection'`, `CategoryTheory.Presheaf.isLocallySurjective_iff_range_sheafify_eq_top'`, `Subpresheaf.epi_iff_range_eq_top`, `instEpiFunctorTypeToRange`, `Subpresheaf.range_ι`, `Subpresheaf.range_le_equalizer_iff`, `Subpresheaf.range_id`, `toRange_ι_assoc`, `instIsIsoFunctorTypeToRangeOfMono`, `range_obj`, `CategoryTheory.Presheaf.imageSieve_eq_sieveOfSection`, `range_eq_ofSection`, `image_top`, `toRange_app_val`, `equivalenceMonoOver_unitIso`, `range_isFinite`, `orderIsoSubobject_symm_apply`, `CategoryTheory.Presheaf.instIsLocallySurjectiveHomToRangeSheafify`, `range_subobjectMk_ι`, `Subpresheaf.toRange_app_val`, `toRangeSheafify_app_coe`, `range_comp`, `CategoryTheory.PresheafIsGeneratedBy.range`, `Subpresheaf.range_comp_le`, `Subpresheaf.subobjectMk_range_arrow`, `Subpresheaf.range_subobjectMk_ι`, `CategoryTheory.FunctorToTypes.monoFactorisation_m`, `CategoryTheory.FunctorToTypes.monoFactorisation_I`, `preimage_eq_top_iff`, `epi_iff_range_eq_top`, `Subpresheaf.ofSection_eq_range`, `Subpresheaf.range_eq_top`, `range_id`, `range_comp_le`, `equivalenceMonoOver_counitIso`, `Subpresheaf.range_toRange`, `subobjectMk_range_arrow`, `toRange_ι`, `CategoryTheory.Sheaf.image_val`
`toRange` 📖	CompOp	12 math math: `range_toRange`, `Subpresheaf.toRange_ι`, `instEpiFunctorTypeToRange`, `toRange_ι_assoc`, `instIsIsoFunctorTypeToRangeOfMono`, `toRange_app_val`, `Subpresheaf.toRange_app_val`, `toRangeSheafify_app_coe`, `equivalenceMonoOver_counitIso`, `CategoryTheory.FunctorToTypes.monoFactorisation_e`, `Subpresheaf.range_toRange`, `toRange_ι`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_iff_range_eq_top` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Functor.category` `range` `Top.top` `CategoryTheory.Subfunctor` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `CategoryTheory.Limits.Types.hasColimitsOfSize` `UnivLE.self`
`fromPreimage_ι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `toFunctor` `preimage` `fromPreimage` `ι`	—	—
`fromPreimage_ι_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `toFunctor` `preimage` `fromPreimage` `ι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `fromPreimage_ι`
`image_comp` 📖	mathematical	—	`image` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	`ext` `Set.ext` `Set.image_congr`
`image_iSup` 📖	mathematical	—	`image` `iSup` `CategoryTheory.Subfunctor` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CategoryTheory.instCompleteLatticeSubfunctor`	—	`ext` `Set.ext` `iSup_obj`
`image_le_iff` 📖	mathematical	—	`CategoryTheory.Subfunctor` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `image` `preimage`	—	—
`image_obj` 📖	mathematical	—	`obj` `image` `Set.image` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.NatTrans.app`	—	—
`image_top` 📖	mathematical	—	`image` `Top.top` `CategoryTheory.Subfunctor` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `range`	—	`ext` `Set.ext` `Set.image_univ`
`instEpiFunctorTypeToRange` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Functor.category` `toFunctor` `range` `toRange`	—	`range_toRange`
`instIsIsoFunctorTypeToRangeOfMono` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Functor.category` `toFunctor` `range` `toRange`	—	`CategoryTheory.mono_of_mono_fac` `toRange_ι` `CategoryTheory.NatTrans.isIso_iff_isIso_app` `CategoryTheory.isIso_iff_bijective` `CategoryTheory.mono_iff_injective` `CategoryTheory.instMonoAppOfFunctor` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `CategoryTheory.Limits.Types.hasLimitsOfSize` `UnivLE.self` `CategoryTheory.epi_iff_surjective` `CategoryTheory.instEpiAppOfFunctor` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `CategoryTheory.Limits.Types.hasColimitsOfSize` `instEpiFunctorTypeToRange`
`lift_app_coe` 📖	mathematical	`CategoryTheory.Subfunctor` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `range`	`CategoryTheory.Functor.obj` `CategoryTheory.types` `Set` `Set.instMembership` `obj` `CategoryTheory.NatTrans.app` `toFunctor` `lift`	—	—
`lift_ι` 📖	mathematical	`CategoryTheory.Subfunctor` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `range`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `toFunctor` `lift` `ι`	—	—
`lift_ι_assoc` 📖	mathematical	`CategoryTheory.Subfunctor` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `range`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `toFunctor` `lift` `ι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lift_ι`
`preimage_comp` 📖	mathematical	—	`preimage` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	—
`preimage_eq_top_iff` 📖	mathematical	—	`preimage` `Top.top` `CategoryTheory.Subfunctor` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CategoryTheory.instPartialOrderSubfunctor` `range`	—	`image_top` `image_le_iff`
`preimage_id` 📖	mathematical	—	`preimage` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	—
`preimage_image_of_epi` 📖	mathematical	—	`image` `preimage`	—	`le_antisymm` `image_le_iff` `le_refl` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Limits.hasFiniteColimits_of_hasColimits` `CategoryTheory.Limits.Types.hasColimitsOfSize` `UnivLE.self`
`preimage_obj` 📖	mathematical	—	`obj` `preimage` `Set.preimage` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.NatTrans.app`	—	—
`range_comp` 📖	mathematical	—	`range` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `image`	—	`ext` `Set.ext`
`range_comp_le` 📖	mathematical	—	`CategoryTheory.Subfunctor` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `range` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	—
`range_eq_top` 📖	mathematical	—	`range` `Top.top` `CategoryTheory.Subfunctor` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`epi_iff_range_eq_top`
`range_id` 📖	mathematical	—	`range` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Top.top` `CategoryTheory.Subfunctor` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`ext` `Set.ext`
`range_obj` 📖	mathematical	—	`obj` `range` `Set.range` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.NatTrans.app`	—	—
`range_toRange` 📖	mathematical	—	`range` `toFunctor` `toRange` `Top.top` `CategoryTheory.Subfunctor` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`ext` `Set.ext`
`range_ι` 📖	mathematical	—	`range` `toFunctor` `ι`	—	`ext` `Set.ext`
`toRange_app_val` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.types` `Set` `Set.instMembership` `obj` `range` `CategoryTheory.NatTrans.app` `toFunctor` `toRange`	—	—
`toRange_ι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `toFunctor` `range` `toRange` `ι`	—	—
`toRange_ι_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `toFunctor` `range` `toRange` `ι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `toRange_ι`

CategoryTheory.Subfunctor.Subpresheaf

Definitions

Name	Category	Theorems
`fromPreimage` 📖	CompOp	—
`image` 📖	CompOp	—
`preimage` 📖	CompOp	—
`range` 📖	CompOp	—
`toRange` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`epi_iff_range_eq_top` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Subfunctor.range` `Top.top` `CategoryTheory.Subfunctor` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`CategoryTheory.Subfunctor.epi_iff_range_eq_top`
`fromPreimage_ι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Subfunctor.toFunctor` `CategoryTheory.Subfunctor.preimage` `CategoryTheory.Subfunctor.fromPreimage` `CategoryTheory.Subfunctor.ι`	—	`CategoryTheory.Subfunctor.fromPreimage_ι`
`image_comp` 📖	mathematical	—	`CategoryTheory.Subfunctor.image` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	`CategoryTheory.Subfunctor.image_comp`
`image_iSup` 📖	mathematical	—	`CategoryTheory.Subfunctor.image` `iSup` `CategoryTheory.Subfunctor` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `CategoryTheory.instCompleteLatticeSubfunctor`	—	`CategoryTheory.Subfunctor.image_iSup`
`image_le_iff` 📖	mathematical	—	`CategoryTheory.Subfunctor` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `CategoryTheory.Subfunctor.image` `CategoryTheory.Subfunctor.preimage`	—	`CategoryTheory.Subfunctor.image_le_iff`
`image_top` 📖	mathematical	—	`CategoryTheory.Subfunctor.image` `Top.top` `CategoryTheory.Subfunctor` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CategoryTheory.Subfunctor.range`	—	`CategoryTheory.Subfunctor.image_top`
`lift_ι` 📖	mathematical	`CategoryTheory.Subfunctor` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `CategoryTheory.Subfunctor.range`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Subfunctor.toFunctor` `CategoryTheory.Subfunctor.lift` `CategoryTheory.Subfunctor.ι`	—	`CategoryTheory.Subfunctor.lift_ι`
`preimage_comp` 📖	mathematical	—	`CategoryTheory.Subfunctor.preimage` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	`CategoryTheory.Subfunctor.preimage_comp`
`preimage_eq_top_iff` 📖	mathematical	—	`CategoryTheory.Subfunctor.preimage` `Top.top` `CategoryTheory.Subfunctor` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CategoryTheory.instPartialOrderSubfunctor` `CategoryTheory.Subfunctor.range`	—	`CategoryTheory.Subfunctor.preimage_eq_top_iff`
`preimage_id` 📖	mathematical	—	`CategoryTheory.Subfunctor.preimage` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	`CategoryTheory.Subfunctor.preimage_id`
`preimage_image_of_epi` 📖	mathematical	—	`CategoryTheory.Subfunctor.image` `CategoryTheory.Subfunctor.preimage`	—	`CategoryTheory.Subfunctor.preimage_image_of_epi`
`range_comp` 📖	mathematical	—	`CategoryTheory.Subfunctor.range` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Subfunctor.image`	—	`CategoryTheory.Subfunctor.range_comp`
`range_comp_le` 📖	mathematical	—	`CategoryTheory.Subfunctor` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.instPartialOrderSubfunctor` `CategoryTheory.Subfunctor.range` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category`	—	`CategoryTheory.Subfunctor.range_comp_le`
`range_eq_top` 📖	mathematical	—	`CategoryTheory.Subfunctor.range` `Top.top` `CategoryTheory.Subfunctor` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`CategoryTheory.Subfunctor.range_eq_top`
`range_id` 📖	mathematical	—	`CategoryTheory.Subfunctor.range` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `Top.top` `CategoryTheory.Subfunctor` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`CategoryTheory.Subfunctor.range_id`
`range_toRange` 📖	mathematical	—	`CategoryTheory.Subfunctor.range` `CategoryTheory.Subfunctor.toFunctor` `CategoryTheory.Subfunctor.toRange` `Top.top` `CategoryTheory.Subfunctor` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticeSubfunctor` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`CategoryTheory.Subfunctor.range_toRange`
`range_ι` 📖	mathematical	—	`CategoryTheory.Subfunctor.range` `CategoryTheory.Subfunctor.toFunctor` `CategoryTheory.Subfunctor.ι`	—	`CategoryTheory.Subfunctor.range_ι`
`toRange_app_val` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.types` `Set` `Set.instMembership` `CategoryTheory.Subfunctor.obj` `CategoryTheory.Subfunctor.range` `CategoryTheory.NatTrans.app` `CategoryTheory.Subfunctor.toFunctor` `CategoryTheory.Subfunctor.toRange`	—	`CategoryTheory.Subfunctor.toRange_app_val`
`toRange_ι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Subfunctor.toFunctor` `CategoryTheory.Subfunctor.range` `CategoryTheory.Subfunctor.toRange` `CategoryTheory.Subfunctor.ι`	—	`CategoryTheory.Subfunctor.toRange_ι`

---

← Back to Index