ExistsUnique 📖 | MathDef | 162 mathmath: existsUnique_sub_zpow_mem_Ioc, uniq_inv_of_isField, Function.Injective.existsUnique_of_mem_range, SimpleGraph.Subgraph.degree_eq_one_iff_unique_adj, existsUnique_congr, discrim_eq_zero_iff, existsUnique_const, ExistsUnique.intro, SimpleGraph.isTree_iff_existsUnique_path, CategoryTheory.Bicategory.Lan.existsUnique, Pell.existsUnique_pos_generator, SimpleGraph.Subgraph.isPerfectMatching_iff, existsUnique_div_zpow_mem_Ico, existsUnique_zsmul_near_of_pos', CategoryTheory.CostructuredArrow.IsUniversal.existsUnique, Function.Injective.mem_range_iff_existsUnique, existsUnique_eq, CategoryTheory.Limits.IsColimit.existsUnique, IsCyclic.unique_zpow_zmod, IsAddCyclic.unique_zsmul_zmod, UniqueMul.exists_iff_exists_existsUnique, CategoryTheory.Functor.IsStronglyCocartesian.universal_property', wittStructureInt_existsUnique, IsLocalRing.maximal_ideal_unique, existsUnique_add_zsmul_mem_Ioc, FirstOrder.Language.BoundedFormula.realize_iExsUnique, Cardinal.mk_eq_two_iff', existsUnique_add_zpow_mem_Ioc, CharP.existsUnique, CategoryTheory.Presieve.isSheafFor_singleton, Polynomial.unique_int_coeff_of_cycl, Ring.krullDimLE_zero_and_isLocalRing_tfae, BoxIntegral.Prepartition.IsPartition.existsUnique, IsLocalHomeomorph.existsUnique_continuousMap_lifts, Ring.KrullDimLE.existsUnique_isPrime, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types, CategoryTheory.Limits.Fork.IsLimit.existsUnique, Equiv.existsUnique_subtype_congr, IsLocalizedModule.is_universal, Nat.card_eq_two_iff', CategoryTheory.StructuredArrow.IsUniversal.existsUnique, Subgroup.isComplement_subgroup_left_iff_existsUnique_quotientMk'', UniqueMul.iff_existsUnique, Polynomial.existsUnique_hilbertPoly, AddSubgroup.isComplement_iff_existsUnique_neg_add_mem, Rat.AbsoluteValue.equiv_real_or_padic, CategoryTheory.Bicategory.LanLift.existsUnique, Setoid.classes_eqv_classes, AddSubgroup.IsComplement.existsUnique, CategoryTheory.Presieve.isSheafFor_arrows_iff, Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype, Function.Bijective.existsUnique, NumberField.mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet, existsUnique_prop, Subgroup.isComplement_iff_existsUnique, TopCat.Sheaf.existsUnique_gluing, Nat.finMulAntidiag_existsUnique_prime_dvd, existsUnique_of_exists_of_unique, StandardEtalePair.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot, AddSubgroup.isComplement_addSubgroup_right_iff_existsUnique_quotientAddGroupMk, UniqueAdd.exists_iff_exists_existsUnique, existsUnique_add_zsmul_mem_Ico, existsUnique_isIdempotentElem_eq_of_ker_isNilpotent, CategoryTheory.Functor.IsCartesian.universal_property, AddSubgroup.mem_closure_singleton_iff_existsUnique_zsmul, CategoryTheory.Functor.IsStronglyCartesian.universal_property', forall_existsUnique_iff, SimpleGraph.Subgraph.degree_eq_one_iff_existsUnique_adj, TopCat.Sheaf.existsUnique_gluing', IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le, CategoryTheory.Limits.limit.existsUnique, unique_iff_existsUnique, CategoryTheory.PreGaloisCategory.exists_autMap, Subgroup.IsComplement.existsUnique, Equiv.existsUnique_congr_left, AddSubgroup.isComplement_addSubgroup_left_iff_existsUnique_quotientMk'', Fintype.existsUnique_iff_card_one, ZSpan.exist_unique_vadd_mem_fundamentalDomain, Equiv.existsUnique_congr_right, ZFSet.map_unique, existsUnique_false, Equiv.Perm.IsCycle.existsUnique_cycle_subtype, Symmetric.forall_existsUnique_iff', CategoryTheory.Functor.IsCocartesian.universal_property, existsUnique_zpow_near_of_one_lt', Configuration.HasLines.existsUnique_line, IsBaseChange.iff_lift_unique, Int.existsUnique_mem_box, Symmetric.forall_existsUnique_iff, existsUnique_sub_zsmul_mem_Ioc, CategoryTheory.Limits.equalizer.existsUnique, Subgroup.mem_closure_singleton_iff_existsUnique_zpow, CategoryTheory.Presheaf.IsSheaf.existsUnique_amalgamation_ofArrows, AddSubgroup.isComplement_iff_existsUnique, existsUnique_prop_of_true, Submodule.existsUnique_from_graph, isPrimePow_iff_unique_prime_dvd, Polynomial.existsUnique_nilpotent_sub_and_aeval_eq_zero, unique_subtype_iff_existsUnique, ExistsUnique.intro₂, Equiv.existsUnique_congr', CategoryTheory.Limits.Cofork.IsColimit.existsUnique, Setoid.eqv_classes_of_disjoint_union, CategoryTheory.Limits.colimit.existsUnique, Configuration.HasPoints.existsUnique_point, Finpartition.existsUnique_mem, Subgroup.isComplement_iff_existsUnique_inv_mul_mem, IsDiscreteValuationRing.TFAE, CategoryTheory.Functor.IsStronglyCartesian.universal_property, CategoryTheory.Presieve.isSheafFor_arrows_iff_pullbacks, Rat.AbsoluteValue.equiv_padic_of_bounded, IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime, CategoryTheory.Limits.Types.unique_of_type_equalizer, existsUnique_mul_zpow_mem_Ico, DirichletCharacter.FactorsThrough.existsUnique, SimpleGraph.IsTree.existsUnique_path, IsFreeGroupoid.unique_lift, Localization.existsUnique_algebraMap_eq_of_span_eq_top, Equiv.existsUnique_congr, PrimeSpectrum.existsUnique_idempotent_basicOpen_eq_of_isClopen, Subgroup.isComplement_iff_existsUnique_mul_inv_mem, existsUnique_sub_zsmul_mem_Ico, IsCoveringMapOn.existsUnique_continuousMap_lifts, SimpleGraph.IsCycles.existsUnique_ne_adj, FirstOrder.Language.Formula.realize_iExsUnique, Equiv.Perm.IsCycle.existsUnique_cycle, NumberField.Units.exist_unique_eq_mul_prod, IsPrimitiveRoot.existsUnique, LinearMap.existsUnique_eq_smul_id_of_finrank_eq_one, CategoryTheory.Limits.coequalizer.existsUnique, Subgroup.isComplement_subgroup_right_iff_existsUnique_quotientGroupMk, pairwiseDisjoint_unique, wittStructureRat_existsUnique, SimpleGraph.ConnectedComponent.Represents.existsUnique_rep, SSet.S.IsUniquelyCodimOneFace.existsUnique_δ_cast_simplex, AffineIndependent.existsUnique_dist_eq, Function.Bijective.existsUnique_iff, IsFreeGroup.unique_lift, ExpChar.exists_unique, existsUnique_zpow_near_of_one_lt, CategoryTheory.Limits.IsLimit.existsUnique, SetRel.exists_graph_eq_iff, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing, existsUnique_zsmul_near_of_pos, IsCoveringMap.existsUnique_continuousMap_lifts, existsUnique_iff_exists, SSet.S.IsUniquelyCodimOneFace.iff, Finset.singleton_iff_unique_mem, forall_existsUnique_iff', AddSubgroup.isComplement_iff_existsUnique_add_neg_mem, UniqueAdd.iff_existsUnique, PadicInt.existsUnique_mem_range, CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.existsUnique_section, Function.bijective_iff_existsUnique, existsUnique_eq', Submodule.existsUnique_add_of_isCompl_prod, CategoryTheory.Limits.Types.isLimit_iff, SimpleGraph.degree_eq_one_iff_existsUnique_adj, CategoryTheory.Limits.Types.type_equalizer_iff_unique, LinearPMap.IsClosable.existsUnique, CategoryTheory.Functor.IsStronglyCocartesian.universal_property, SSet.S.existsUnique_n
|