| Metric | Count |
|---|
Definitionsinf, inf', sup, sup' | 4 |
Theoremsinf_eq_bot_iff, sup_eq_top_iff, codisjoint_inf_left, codisjoint_inf_right, coe_inf', coe_inf_of_nonempty, coe_sup', coe_sup_of_nonempty, comp_inf'_eq_inf'_comp, comp_inf_eq_inf_comp, comp_inf_eq_inf_comp_of_is_total, comp_sup'_eq_sup'_comp, comp_sup_eq_sup_comp, comp_sup_eq_sup_comp_of_is_total, comp_sup_eq_sup_comp_of_nonempty, compl_inf, compl_sup, disjoint_sup_left, disjoint_sup_right, exists_inf_eq_iInf, exists_inf_le, exists_mem_eq_inf, exists_mem_eq_inf', exists_mem_eq_sup, exists_mem_eq_sup', exists_sup_eq_iSup, exists_sup_ge, inf'_apply, inf'_comm, inf'_comp_eq_image, inf'_comp_eq_map, inf'_congr, inf'_cons, inf'_const, inf'_eq_inf, inf'_eq_of_forall, inf'_image, inf'_induction, inf'_insert, inf'_le, inf'_le_iff, inf'_le_of_le, inf'_lt_iff, inf'_map, inf'_mem, inf'_mono, inf'_singleton, inf'_sup_distrib_left, inf'_sup_distrib_right, inf'_union, inf_apply, inf_attach, inf_coe, inf_comm, inf_congr, inf_cons, inf_const, inf_def, inf_disjSum, inf_dite_neg_le, inf_dite_pos_le, inf_empty, inf_eq_bot_iff, inf_eq_iInf, inf_eq_sInf_image, inf_eq_top_iff, inf_erase_top, inf_himp_right, inf_id_eq_sInf, inf_id_set_eq_sInter, inf_image, inf_induction, inf_inf, inf_insert, inf_ite, inf_le, inf_le_iff, inf_le_of_le, inf_lt_iff, inf_map, inf_mem, inf_mono, inf_mono_fun, inf_of_mem, inf_sdiff_left, inf_sdiff_right, inf_set_eq_iInter, inf_singleton, inf_sup_distrib_left, inf_sup_distrib_right, inf_top, inf_union, isGLB_inf, isGLB_inf', isGLB_inf_id, isLUB_sup, isLUB_sup', isLUB_sup_id, le_inf, le_inf', le_inf'_iff, le_inf_const_le, le_inf_iff, le_sup, le_sup', le_sup'_iff, le_sup'_of_le, le_sup_dite_neg, le_sup_dite_pos, le_sup_iff, le_sup_of_le, lt_inf'_iff, lt_inf_iff, lt_sup'_iff, lt_sup_iff, mem_inf', mem_sup, mem_sup', ofDual_inf, ofDual_inf', ofDual_sup, ofDual_sup', subset_range_sup_succ, sup'_apply, sup'_comm, sup'_comp_eq_image, sup'_comp_eq_map, sup'_congr, sup'_cons, sup'_const, sup'_eq_of_forall, sup'_eq_sup, sup'_image, sup'_induction, sup'_inf_distrib_left, sup'_inf_distrib_right, sup'_insert, sup'_le, sup'_le_iff, sup'_lt_iff, sup'_map, sup'_mem, sup'_mono, sup'_mono_fun, sup'_singleton, sup'_union, sup_apply, sup_attach, sup_bot, sup_coe, sup_comm, sup_congr, sup_cons, sup_const, sup_const_le, sup_def, sup_disjSum, sup_empty, sup_eq_bot_iff, sup_eq_bot_of_isEmpty, sup_eq_iSup, sup_eq_sSup_image, sup_eq_top_iff, sup_erase_bot, sup_himp_left, sup_himp_right, sup_id_eq_sSup, sup_id_set_eq_sUnion, sup_image, sup_induction, sup_inf_distrib_left, sup_inf_distrib_right, sup_insert, sup_ite, sup_le, sup_le_iff, sup_le_of_le_directed, sup_lt_iff, sup_map, sup_mem, sup_mem_of_nonempty, sup_mono, sup_mono_fun, sup_of_mem, sup_sdiff_left, sup_sdiff_right, sup_set_eq_biUnion, sup_singleton, sup_singleton_apply, sup_singleton_eq_self, sup_sup, sup_toFinset, sup_union, toDual_inf, toDual_inf', toDual_sup, toDual_sup', foldr_inf_eq_inf_toFinset, foldr_sup_eq_sup_toFinset, count_finset_sup, map_finset_sup, mem_sup, map_finset_inf, map_finset_inf', map_finset_sup, map_finset_sup' | 206 |
| Total | 210 |
| Name | Category | Theorems |
|---|
inf π | CompOp | 168 mathmath: coe_inf', inf_sigma, Set.Finite.einfsep, exists_mem_eq_inf, Set.einfsep_of_fintype, AlgebraicTopology.NormalizedMooreComplex.obj_d, inf_id_set_eq_sInter, le_inf_div, InfPrime.finset_inf_le, min_eq_inf_withTop, inf_eq_top_iff, ContinuousWithinAt.finset_inf_apply, inf_lt_iff, ContinuousAt.finset_inf, List.foldr_inf_eq_inf_toFinset, compl_inf, inf_ite, inf_inf, ofDual_inf, inf_map, inf_le_iff, inf_sub_left, Ideal.comap_finsetInf, Submodule.colon_finsetInf, inf_biUnion, inf_sup_distrib_right, compl_sup, inclusion_exclusion_card_inf_compl, isBoundedUnder_ge_finset_inf, inf_id_eq_sInf, inf_mul_left, OrderIso.infIrredUpperSet_symm_apply, ContinuousOn.finset_inf_apply, Ideal.isPrimary_finsetInf, inf_zero, inf_prodMap, Set.Finset.coe_einfsep, Ideal.prod_le_inf, Submodule.mem_finset_inf, le_inf_imageβ, le_inf_add, inf_union, ContinuousOn.finset_inf, inf_sup, inf_mem, inf_sup_distrib_left, inf_apply, Ideal.IsPrime.inf_le', ContinuousAt.finset_inf_apply, inf_himp_right, inf_congr, isGLB_inf, inf_induction, inf_const, inf_eq_of_min, Ideal.isPrimary_finset_inf, AddMonoidAlgebra.le_inf_support_add, inf_image, inf_sub_right, PrimitiveSpectrum.hull_finsetInf, inclusion_exclusion_sum_inf_compl, inf_mono_fun, Submodule.IsMinimalPrimaryDecomposition.inf_eq, AddMonoidAlgebra.le_inf_support_pow, mul_inf_le_inf_mul_of_nonneg, inf_product_left, inf_def, inf_inv, inf_attach, Seminorm.closedBall_finset_sup, Topology.IsLocallyConstructible.finsetInf, Submodule.comap_finsetInf, Submodule.coe_finsetInf, ContinuousWithinAt.finset_inf, inf_product_right, TopologicalSpace.Closeds.coe_finset_inf, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_isLimit_lift, inf_eq_bot_iff, AddMonoidAlgebra.le_inf_support_list_prod, le_inf_mul, inf_imageβ_left, inf_comm, inf_sdiff_right, TopologicalSpace.Opens.coe_finset_inf, inf_dite_neg_le, inf_insert, comp_inf_eq_inf_comp_of_is_total, inf_set_eq_iInter, Ideal.finset_inf_span_singleton, InfClosed.finsetInf_mem, inf_add_left, map_finset_inf, toDual_inf, CategoryTheory.Limits.CompleteLattice.finite_limit_eq_finset_univ_inf, sup_inf, lt_inf_iff, le_inf_iff, PrimitiveSpectrum.preimage_upperClosure_compl_finset, inf_mono, inf_add_right, Nonempty.inf_eq_bot_iff, Submodule.IsMinimalPrimaryDecomposition.minimal, inf_dite_pos_le, IsDedekindDomain.inf_prime_pow_eq_prod, coe_inf_of_nonempty, CategoryTheory.Subobject.finset_inf_factors, Continuous.finset_inf_apply, inf_of_mem, inf_eq_of_isMinOn, inf_mul_right, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_pt, trop_inf, AddMonoidAlgebra.le_inf_support_mul, exists_infIrred_decomposition, inf_empty, mem_inf, exists_inf_le, toDual_sup, untrop_sum', comp_inf_eq_inf_comp, inf_coe, inf_le_of_le, sup_sdiff_left, inf_erase_top, AlgebraicTopology.NormalizedMooreComplex.objX_add_one, inf_sup_inf, Continuous.finset_inf, inf_eq_sInf_image, sup_himp_right, inf_eq_iInf, inf_imageβ_right, inf_singleton, isGLB_inf_id, Ideal.eq_inf_of_isPrime_inf, Submodule.finset_inf_coe, Submodule.mem_finsetInf, liminf_finset_inf, le_inf, inf_sdiff_left, exists_inf_eq_iInf, inf_le, Filter.Tendsto.finset_inf_nhds_apply, inf_div_left, inf_univ_eq_iInf, inf_disjSum, Set.definable_finset_inf, inf_div_right, inf_neg, inf'_eq_inf, inf_top, inf_one, le_inf_const_le, AddMonoidAlgebra.le_inf_support_finset_prod, Seminorm.ball_finset_sup, AddMonoidAlgebra.le_inf_support_multiset_prod, Ideal.radical_finset_inf, codisjoint_inf_left, CategoryTheory.Subobject.finset_inf_arrow_factors, le_inf_sub, CategoryTheory.Limits.CompleteLattice.finiteLimitCone_cone_Ο_app, Filter.Tendsto.finset_inf_nhds, inf_Ici, IsRetrocompact.finsetInf, inf_cons, ofDual_sup, Submodule.isPrimary_finsetInf, CategoryTheory.Limits.CompleteLattice.finite_product_eq_finset_inf, codisjoint_inf_right
|
inf' π | CompOp | 92 mathmath: inf'_inv, coe_inf', Continuous.finset_inf', ContinuousOn.finset_inf'_apply, inf'_univ_eq_ciInf, inf'_sup_inf', inf'_zero, inf'_comm, inf'_lt_iff, ContinuousMap.coe_inf', le_inf'_iff, inf'_product_left, inf'_mem, inf'_congr, inf'_map, Set.Finite.infsep_of_nontrivial, coe_infsep_of_offDiag_nonempty, Set.Nontrivial.infsep_of_fintype, Set.Finite.infsep, inf'_const, inf'_sup_distrib_right, inf'_one, IsRetrocompact.finsetInf', ContinuousOn.finset_inf', inf'_pow, inf'_Ici, inf'_prodMap, le_inf'_imageβ, toDual_inf', ofDual_sup', Set.infsep_of_fintype, map_finset_inf', inf'_imageβ_right, Filter.Tendsto.finset_inf'_nhds_apply, nsmul_inf', coe_infsep, inclusion_exclusion_card_biUnion, inf'_product_right, ContinuousMap.inf'_apply, ContinuousWithinAt.finset_inf'_apply, isCoboundedUnder_ge_finset_inf', inf'_comp_eq_image, CompactlySupportedContinuousMap.finsetInf'_apply, inf'_cons, ContinuousAt.finset_inf', comp_inf'_eq_inf'_comp, prodMk_inf'_inf', Nat.cast_finsetInf', ContinuousAt.finset_inf'_apply, lt_inf'_iff, ContinuousWithinAt.finset_inf', inclusion_exclusion_sum_biUnion, liminf_finset_inf', inf'_biUnion, inf'_image, inf_le_centerMass, le_inf', mem_inf', Filter.Tendsto.finset_inf'_nhds, inf'_le_iff, inf'_comp_eq_map, CompactlySupportedContinuousMap.coe_finsetInf', Continuous.finset_inf'_apply, inf'_imageβ_left, ofDual_inf', inf'_induction, Seminorm.closedBall_finset_sup', inf'_mono, inf'_id_eq_csInf, inf'_neg, inf'_singleton, inf'_eq_csInf_image, InfClosed.finsetInf'_mem, isBoundedUnder_ge_finset_inf', inf'_sup_distrib_left, inf'_eq_inf, inf'_le_of_le, Topology.IsLocallyConstructible.finsetInf', finsetInf'_mem_infClosure, isGLB_inf', ConvexOn.inf_le_of_mem_convexHull, inf'_eq_of_forall, inf'_apply, inf'_mul_le_mul_inf'_of_nonneg, Seminorm.ball_finset_sup', inf'_insert, inf'_union, min'_eq_inf', exists_mem_eq_inf', inf'_le, toDual_sup', truncatedInf_of_mem
|
sup π | CompOp | 284 mathmath: SchwartzMap.norm_toLp_le_seminorm, AddMonoidAlgebra.sup_support_list_prod_le, sup_one, Seminorm.isBounded_const, sup_add_sup, sup_singleton_eq_self, comp_sup_eq_sup_comp_of_is_total, Seminorm.le_finset_sup_apply, sup_product_right, Finpartition.combine_parts, ContinuousAt.finset_sup, bind_def, Seminorm.finset_sup_apply, WithSeminorms.mem_nhds_iff, CompleteLattice.isCompactElement_finsetSup, Ideal.sum_eq_sup, sup_le_of_le_directed, Pi.norm_def', sup_add_le, comp_sup_eq_sup_comp, Continuous.finset_sup, sup_insert, Nonempty.sup_eq_top_iff, compl_inf, CategoryTheory.Limits.CompleteLattice.finite_coproduct_eq_finset_sup, mem_sup, isWF_sup, ofDual_inf, sup_coe, MvPolynomial.degreeOf_sum_le, compl_sup, sup_induction, MvPolynomial.totalDegree_eq, sup_div_right, sup_erase_bot, WithSeminorms.tendsto_nhds', sup_singleton, MvPolynomial.degrees_def, TopologicalSpace.NoetherianSpace.exists_finset_irreducible, support_sum_subset, sup_set_eq_biUnion, sup_div_le, sup_univ_eq_ciSup, Multiset.sup_powerset_len, SeminormFamily.finset_sup_comp, CategoryTheory.Subobject.finset_sup_factors, sup_Ioc_disjointed_of_monotone, Submodule.finiteDimensional_finset_sup, seq_def, Fintype.sup_disjointed, inf_sup, OrderIso.supIrredLowerSet_symm_apply, isLUB_sup_id, exists_supIrred_decomposition, Set.definable_finset_sup, le_sup_dite_pos, Subgroup.FG.finset_sup, Multiset.finset_sum_eq_sup_iff_disjoint, inf_himp_right, sup_inf_distrib_left, sup_mul_le, max_eq_sup_coe, Filter.Tendsto.finset_sup_nhds, sup_product_left, AddMonoidAlgebra.sup_support_multiset_prod_le, partialSups_eq_sup_range, Polynomial.natDegree_sum_eq_of_disjoint, CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup, Seminorm.finset_sup_apply_lt, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_ΞΉ_app, MeasureTheory.preVariation.Finset.sup_measurableSetSubtype_eq_biUnion, subset_range_sup_succ, Submonoid.FG.finset_sup, BoxIntegral.Prepartition.distortion_biUnionTagged, sup_Iic, coe_sup', Seminorm.bound_of_continuous, SupIndep.disjoint_sup_sup, disjoint_sup_left, sup_empty, sup_sub_right, sup_attach, MonomialOrder.degree_sum_le, ContinuousOn.finset_sup_apply, sup_const, Seminorm.closedBall_finset_sup, TopologicalSpace.Opens.coe_finset_sup, CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup, Polynomial.degree_sum_le, mem_sup_support_iff, sup_eq_top_iff, sup_const_le, nilpotencyClass_pi, sup_inf_distrib_right, WithSeminorms.isOpen_iff_mem_balls, coe_sup_of_nonempty, sup_prodMap, exists_sup_ge, NNReal.mul_finset_sup, sup_sub_le, sup_lt_iff, Pi.nnnorm_def', max_eq_sup_withBot, sup_le, Submodule.fg_finset_sup, sup_zero, TopologicalSpace.Clopens.exists_finset_eq_sup_prod, SimpleGraph.extremalNumber_of_fintypeCard_eq, NumberField.canonicalEmbedding.nnnorm_eq, SupIndep.le_sup_iff, BooleanSubalgebra.mem_closure_iff_sup_sdiff, sup_eq_biUnion, ENNReal.coe_finset_sup, Pi.norm_def, IsRetrocompact.finsetSup, image_subset_Iic_sup, ContinuousWithinAt.finset_sup, MvPolynomial.degrees_sum_le, Seminorm.exists_apply_eq_finset_sup, MvPolynomial.schwartz_zippel_sup_sum, WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded, supIndep_product_iff, le_sup_iff, sup_sdiff_right, toDual_inf, sup_sub_left, TopologicalSpace.Compacts.coe_finset_sup, TopologicalSpace.CompactOpens.coe_finsetSup, sup_inf, exists_mem_eq_sup, PseudoMetric.IsUltra.finsetSup, Multiset.map_finset_sup, add_sup, nndist_pi_def, IsUltrametricDist.nnnorm_sum_eq_sup_of_pairwise_ne, IsUltrametricDist.nnnorm_prod_eq_sup_of_pairwise_ne, sup_union, SchwartzMap.eLpNorm_le_seminorm, ContinuousAt.finset_sup_apply, BoxIntegral.TaggedPrepartition.distortion_biUnionPrepartition, AddSubgroup.FG.finset_sup, supIndep_sigma_iff', sup_map, sup_eq_iSup, isPWO_sup, partiallyWellOrderedOn_sup, MvPolynomial.degreeOf_eq_sup, sup_disjSum, isLUB_sup, Multiset.mem_sup, AddMonoidAlgebra.sup_support_mul_le, sup_singleton_apply, le_sup_of_le, BoxIntegral.Prepartition.distortion_biUnion, TopologicalSpace.Closeds.coe_finset_sup, disjoint_sup_right, inf_sSup_eq_iSup_inf_sup_finset, ContinuousOn.finset_sup, supIndep_iff_disjoint_erase, sup_comm, sup_eq_bot_of_isEmpty, sup_mul_le_mul_sup_of_nonneg, isBoundedUnder_le_finset_sup, sup_image, TopologicalSpace.Clopens.surjective_finset_sup_prod, sup_mem_of_nonempty, ContinuousWithinAt.finset_sup_apply, sup_mono_fun, Multiset.count_finset_sup, Seminorm.zero_or_exists_apply_eq_finset_sup, toDual_sup, sup_sup, TopologicalSpace.Clopens.coe_finset_sup, sup_sdiff_left, Nat.sup_divisors_id, powersetCard_sup, AddMonoidAlgebra.sup_support_pow_le, Nat.cast_finsetSup, Pi.nnnorm_def, Submodule.finite_finset_sup, sup_mem, Seminorm.bound_of_shell_sup, Fintype.exists_disjointed_le, Filter.Tendsto.finset_sup_nhds_apply, sup_congr, sup_mono, sup_neg, sup_ite, WithSeminorms.image_isVonNBounded_iff_finset_seminorm_bounded, support_sum_eq, Seminorm.finset_sup_smul, dist_pi_def, Seminorm.isBounded_sup, Polynomial.degree_sum_eq_of_disjoint, apply_sup_le_sum, sup_eq_sSup_image, comp_sup_eq_sup_comp_of_nonempty, disjointed_apply, sup_cons, AddMonoidAlgebra.sup_support_add_le, lt_sup_iff, le_sup_dite_neg, Continuous.finset_sup_apply, SupClosed.finsetSup_mem, sup_eq_zero, nnnorm_sum_le_sup_nnnorm, edist_pi_def, sup_le_iff, sup_himp_right, PseudoMetric.coe_finsetSup, MvPolynomial.totalDegree_finset_sum, sup_inv, sup_apply, limsup_finset_sup, NNReal.finset_sup_mul, sup_inf_sup, wellFoundedOn_sup, sup_divβ, List.foldr_sup_eq_sup_toFinset, sup_def, sup_add_right, sup_div_left, LinearMap.mem_span_iff_bound, WithSeminorms.partial_sups, inf_sdiff_left, sup_add, CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup, AddMonoidAlgebra.sup_support_finset_prod_le, nnnorm_prod_le_sup_nnnorm, sup_biUnion, sup_bot, Seminorm.ball_finset_sup_eq_iInter, sup_eq_of_isMaxOn, sup_eq_of_max, sym_succ, sup_toFinset, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_cocone_pt, sup_mul_left, sup_univ_eq_iSup, sup_imageβ_le, subset_Iic_sup_id, SupPrime.le_finset_sup, Order.Ideal.finsetSup_mem_iff, Seminorm.ball_finset_sup, sup_sigma, PseudoMetric.finsetSup_apply, MeasureTheory.SimpleFunc.approx_apply, AddSubmonoid.FG.finset_sup, MeasureTheory.IsSetRing.finsetSup_mem, sup'_eq_sup, sup_imageβ_right, MeasureTheory.SimpleFunc.finset_sup_apply, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone_isColimit_desc, SeminormFamily.basisSets_mem, Finpartition.sup_parts, sup_eq_bot_iff, SeminormFamily.basisSets_iff, sup_id_eq_sSup, sup_himp_left, Finpartition.sum_combine, exists_sup_eq_iSup, SchwartzMap.one_add_le_sup_seminorm_apply, sup_id_set_eq_sUnion, ofDual_sup, Matrix.linfty_opNNNorm_def, WithSeminorms.hasBasis_ball, Seminorm.finset_sup_le_sum, sup_add_left, NumberField.mixedEmbedding.nnnorm_eq_sup_normAtPlace, Seminorm.finset_sup_apply_le, mul_supβ, sup_mul_right, Seminorm.closedBall_finset_sup_eq_iInter, Matrix.linfty_opNorm_def, sup_mulβ, Matrix.norm_eq_sup_sup_nnnorm, sup_of_mem, WithSeminorms.hasBasis_zero_ball, le_sup, NNReal.finset_sup_div, sup_imageβ_left, WithSeminorms.finset_sups, AddMonoidAlgebra.supDegree_sum_le, map_finset_sup
|
sup' π | CompOp | 112 mathmath: sup'_mul_le_mul_sup'_of_nonneg, partialSups_apply, Nonempty.norm_sum_le_sup'_norm, NumberField.mixedEmbedding.norm_eq_sup'_normAtPlace, sup'_add', sup'_product_left, sup'_imageβ_left, le_sup'_iff, MeasureTheory.smul_le_stoppedValue_hittingBtwn, measurable_range_sup'', partialSups_eq_sup'_range, IsNonarchimedean.apply_sum_le_sup_of_isNonarchimedean, lt_sup'_iff, sup'_Iic, le_sup'_of_le, prodMk_sup'_sup', sup'_prodMap, sup'_mem, ContinuousAt.finset_sup', Continuous.finset_sup'_apply, sup'_image, isBoundedUnder_le_finset_sup', map_finset_sup', sup'_mono, sup'_const, sup'_apply, sup'_inf_distrib_right, truncatedSup_of_mem, sup'_singleton, sup'_mulβ, sup'_pow, ContinuousOn.finset_sup', sup'_lt_iff, Nat.cast_finsetSup', sup'_mono_fun, coe_sup', sup'_eq_csSup_image, max'_eq_sup', sup'_insert, toDual_inf', ofDual_sup', measurable_range_sup', comp_sup'_eq_sup'_comp, sup'_eq_of_forall, sup'_comp_eq_map, sup'_inf_sup', MeasureTheory.smul_le_stoppedValue_hitting, SupClosed.finsetSup'_mem, IsUltrametricDist.norm_sum_eq_sup'_of_pairwise_ne, sup'_le_iff, ContinuousOn.finset_sup'_apply, Filter.Tendsto.finset_sup'_nhds, Polynomial.supNorm_def', sup'_comm, sup'_zero, isLUB_sup', nsmul_sup', sup'_map, centerMass_le_sup, sup'_le, mem_sup', IsRetrocompact.finsetSup', add_sup', Continuous.finset_sup', ContinuousMap.coe_sup', sup'_add, sup'_inf_distrib_left, ContinuousAt.finset_sup'_apply, mul_sup', sup'_induction, Nonempty.norm_prod_le_sup'_norm, Filter.Tendsto.finset_sup'_nhds_apply, ConvexOn.le_sup_of_mem_convexHull, exists_mem_eq_sup', sup'_id_eq_csSup, IsUltrametricDist.norm_prod_eq_sup'_of_pairwise_ne, sup'_cons, MeasureTheory.maximal_ineq, sup'_neg, PseudoMetric.coe_finsetSup, sup'_comp_eq_image, sup'_union, ofDual_inf', sup'_imageβ_le, Seminorm.closedBall_finset_sup', mulβ_sup', isCoboundedUnder_le_finset_sup', ContinuousWithinAt.finset_sup'_apply, measurable_sup', sup'_congr, sup'_one, CompactlySupportedContinuousMap.coe_finsetSup', sup'_product_right, PseudoMetric.finsetSup_apply, limsup_finset_sup', le_sup', sup'_eq_sup, sup'_mul, sup'_divβ, finsetSup'_mem_supClosure, sup'_univ_eq_ciSup, add_sup'', Seminorm.ball_finset_sup', sup'_imageβ_right, sup'_eq_zero, ContinuousWithinAt.finset_sup', sup'_inv, ContinuousMap.sup'_apply, CompactlySupportedContinuousMap.finsetSup'_apply, NumberField.house_eq_sup', toDual_sup', sup'_biUnion
|