Iso 📖 | CompData | 178 mathmath: Discrete.sumEquiv_counitIso_inv_app, Limits.diagramIsoPair_hom_app, ObjectProperty.prop_isoClosure_iff, Limits.WalkingMultispan.functorExt_hom_app, ObjectProperty.prop_map_iff, Iso.nonempty_iso_refl, Discrete.sumEquiv_unitIso_inv_app, Iso.isoCongr_symm_apply, WithInitial.opEquiv_unitIso_inv_app, Limits.cospanIsoMk_inv_app, FintypeCat.instFiniteIso, WithInitial.liftToInitialUnique_hom_app, FintypeCat.uSwitch_map_uSwitch_map, Limits.MultispanIndex.toLinearOrderMultispanIso_inv_app, equivEquivIso_hom, Pretriangulated.Opposite.mem_distinguishedTriangles_iff', Limits.MultispanIndex.toLinearOrderMultispanIso_hom_app, Limits.PushoutCocone.unop_π_app, finrank_hom_simple_simple_eq_one_iff, Limits.mapPairIso_inv_app, Sequential.isoEquivHomeo_apply, linearEquivIsoModuleIso_hom, Sequential.isoEquivHomeo_symm_apply, CatCenter.smul_iso_inv_eq', WithTerminal.mapComp_hom_app, Limits.WidePullbackShape.functorExt_hom_app, FintypeCat.equivEquivIso_apply_hom, Functor.FullyFaithful.isoEquiv_apply, WithInitial.opEquiv_counitIso_hom_app, Limits.cospanIsoMk_hom_app, ThinSkeleton.fromThinSkeleton_map, Limits.parallelPairIsoMk_inv_app, equivIsoIso_hom, WithTerminal.opEquiv_counitIso_inv_app, CommBialgCat.isoEquivBialgEquiv_apply, CatCenter.smul_iso_inv_eq'_assoc, Limits.spanOp_hom_app, skeletonEquivalence_unitIso, WithTerminal.opEquiv_unitIso_hom_app, Functor.map_isoCongr, Preadditive.smul_iso_hom, WithTerminal.opEquiv_counitIso_hom_app, CompHausLike.isoEquivHomeo_symm_apply, FintypeCat.equivEquivIso_symm_apply_symm_apply, Preadditive.neg_iso_hom, WithInitial.mapId_inv_app, Limits.PullbackCone.op_ι_app, Limits.MultispanIndex.multispanMapIso_inv_app, Functor.mapIso_injective, toSkeleton_eq_iff, Preadditive.smul_iso_inv, subsingleton_iso, Limits.HasZeroObject.instSubsingletonIsoOfNat, Limits.parallelPairIsoMk_hom_app, Pi.optionEquivalence_unitIso, Limits.idZeroEquivIsoZero_apply_inv, CommAlgCat.isoEquivAlgEquiv_apply, Limits.spanOp_inv_app, PreGaloisCategory.exists_lift_of_continuous, Ind.exists_nonempty_arrow_mk_iso_ind_lim, FintypeCat.equivEquivIso_apply_inv, Limits.opSpan_hom_app, CatCenter.smul_iso_hom_eq'_assoc, Discrete.sumEquiv_unitIso_hom_app, Bicategory.conjugateIsoEquiv_apply_inv, GrothendieckTopology.Cover.multicospanComp_inv_app, Groupoid.isoEquivHom_apply, Groupoid.isoEquivHom_symm_apply_hom, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_inv_app_left_app, WithTerminal.liftToTerminalUnique_inv_app, WithTerminal.mapComp_inv_app, Limits.opCospan_hom_app, finrank_hom_simple_simple_eq_zero_iff, linearEquivIsoModuleIsoₛ_hom, Discrete.sumEquiv_counitIso_hom_app, Iso.trans_def, Functor.RepresentableBy.equivUliftYonedaIso_symm_apply_homEquiv, FintypeCat.equivEquivIso_symm_apply_apply, Limits.WalkingMultispan.functorExt_inv_app, Limits.PushoutCocone.op_π_app, Limits.parallelPair.ext_hom_app, CommBialgCat.isoEquivBialgEquiv_symm_apply, Limits.opCospan_inv_app, Equivalence.ext_iff, Limits.idZeroEquivIsoZero_apply_hom, Limits.PullbackCone.unop_ι_app, Pretriangulated.mem_distTriang_op_iff', Limits.cospanOp_hom_app, AlgebraicGeometry.Scheme.local_affine, AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app, algEquivIsoAlgebraIso_inv, CatCenter.smul_iso_inv_eq_assoc, CochainComplex.exists_iso_single, WithInitial.opEquiv_counitIso_inv_app, finrank_hom_simple_simple, DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE, equivIsoIso_inv, Functor.CorepresentableBy.equivUliftCoyonedaIso_symm_apply_homEquiv, GrothendieckTopology.Cover.multicospanComp_hom_app, Bicategory.conjugateIsoEquiv_apply_hom, Bicategory.conjugateIsoEquiv_symm_apply_hom, WithInitial.equivComma_unitIso_inv_app_app, DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE, CatCenter.smul_iso_hom_eq_assoc, IsPreconnected.iso_constant, Iso.nonempty_iso_symm, Iso.isoCongr_apply, ContinuousMap.piComparison_fac, Limits.Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_inv_app_app, isoOpEquiv_symm_apply, Limits.MultispanIndex.multispanMapIso_hom_app, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, DerivedCategory.exists_iso_Q_obj_of_isGE, WithInitial.equivComma_unitIso_hom_app_app, Functor.CorepresentableBy.equivUliftCoyonedaIso_apply, CatCenter.smul_iso_inv_eq, CommAlgCat.isoEquivAlgEquiv_symm_apply, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_hom_app_app, CompactlyGenerated.isoEquivHomeo_symm_apply, PreGaloisCategory.has_decomp_quotients, AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app, WithTerminal.mapId_hom_app, Limits.WalkingMulticospan.functorExt_hom_app, HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit, CompactlyGenerated.isoEquivHomeo_apply, Limits.WidePullbackShape.functorExt_inv_app, CatCenter.smul_iso_hom_eq', Limits.spanIsoMk_hom_app, Limits.WalkingMulticospan.functorExt_inv_app, Functor.FullyFaithful.isoEquiv_symm_apply, conjugateIsoEquiv_apply_hom, conjugateIsoEquiv_apply_inv, Pseudofunctor.DescentData.exists_equivalence_of_sieve_eq, linearEquivIsoModuleIso_inv, FDRep.char_orthonormal, conjugateIsoEquiv_symm_apply_inv, algEquivIsoAlgebraIso_hom, CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, Groupoid.isoEquivHom_symm_apply_inv, Limits.cospanOp_inv_app, Functor.RepresentableBy.equivUliftYonedaIso_apply, isoOpEquiv_apply, ShortComplex.exact_iff_homology_iso_zero, DerivedCategory.exists_iso_Q_obj_of_isLE, WithTerminal.mapId_inv_app, AlgebraicGeometry.Scheme.affineBasisCover_map_range, Limits.parallelPair.eqOfHomEq_hom_app, conjugateIsoEquiv_symm_apply_hom, CompHausLike.isoEquivHomeo_apply, PreGaloisCategory.exists_lift_of_quotient_openSubgroup, AlgebraicGeometry.Scheme.affineOpenCover_X, Limits.diagramIsoPair_inv_app, DerivedCategory.mem_distTriang_iff, CatCenter.smul_iso_hom_eq, toSkeleton_eq_toSkeleton_iff, Limits.parallelPair.eqOfHomEq_inv_app, WithInitial.liftToInitialUnique_inv_app, WithInitial.mapComp_inv_app, Iso.symm_bijective, Limits.opSpan_inv_app, Limits.mapPairIso_hom_app, equivEquivIso_inv, WithInitial.opEquiv_unitIso_hom_app, WithTerminal.equivComma_unitIso_hom_app_app, WithTerminal.opEquiv_unitIso_inv_app, Functor.mem_mapTriangle_essImage_of_distinguished, Limits.spanIsoMk_inv_app, Bicategory.conjugateIsoEquiv_symm_apply_inv, linearEquivIsoModuleIsoₛ_inv, WithTerminal.liftToTerminalUnique_hom_app, WithTerminal.equivComma_unitIso_inv_app_app, Preadditive.neg_iso_inv, WithInitial.mapId_hom_app, WithInitial.mapComp_hom_app, AugmentedSimplexCategory.equivAugmentedCosimplicialObject_unitIso_hom_app_app, Limits.parallelPair.ext_inv_app, FDRep.finrank_hom_simple_simple
|