| Name | Category | Theorems |
|---|
BddAbove 📖 | MathDef | 153 mathmath: bddAbove_range_prod, not_bddAbove_Ioi, bddBelow_bddAbove_iff_subset_Icc, bddBelow_smul_iff_of_neg, BddBelow.neg, Filter.not_bddAbove_of_tendsto_atTop, Ordinal.not_bddAbove_fp_family, bddAbove_iff_exists_ge, Seminorm.bddAbove_range_iff, lowerClosure_eq_top_iff, orderBornology_isBounded, OrderIso.bddAbove_image, bddAbove_union, Nat.not_bddAbove_setOf_prime, Cardinal.bddAbove_ord_image_iff, bddAbove_neg, MonotoneOn.map_bddAbove, BddBelow.image2_bddAbove, Ordinal.not_bddAbove_isInitial, bddAbove_inv, spectralValueTerms_bddAbove, AddAction.period_bounded_of_exponent_pos, Ordinal.not_bddAbove_principal, bddAbove_pi, StrictMono.not_bddAbove_range_of_isSuccArchimedean, MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto, Finset.bddAbove, ENNReal.iSup_coe_lt_top, GaloisConnection.bddAbove_l_image, BoundedContinuousFunction.bddAbove_range_norm_comp, bddAbove_prod, Filter.Tendsto.bddAbove_range, Set.Finite.bddAbove_biUnion, bddAbove_slope_gt_of_mem_interior, bddBelow_preimage_toDual, WithSeminorms.isVonNBounded_iff_seminorm_bddAbove, OrderTop.bddAbove, memℓp_infty_iff, NNReal.bddAbove_range_agmSequences_fst, bddAbove_iff_subset_Iic, bddAbove_Iio, StrictMono.not_bddAbove_range_of_wellFoundedLT, Urysohns.CU.bddAbove_range_approx, Seminorm.bddAbove_iff, MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto_aux, Ordinal.not_bddAbove_fp, BddBelow.smul_of_nonpos, Set.Infinite.not_bddAbove, Set.bdd_below_bdd_above_iff_subset_uIcc, IsCompact.bddAbove, ENat.iSup_coe_ne_top, not_bddAbove_iff_isCofinal, BddAbove.of_not_isCofinal, not_isCofinal_iff_bddAbove, Cardinal.bddAbove_range, WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup, WithTop.iSup_coe_lt_top, not_bddAbove_Ici, not_bddAbove_univ, NormedSpace.equicontinuous_TFAE, PiTensorProduct.dualSeminorms_bounded, Set.nonempty_iInter_Ici_iff, Ordinal.bddAbove_range, bddAbove_singleton, MeasureTheory.upperCrossingTime_lt_bddAbove, MulAction.period_bounded_of_exponent_pos, SetTheory.PGame.bddAbove_of_small, bddAbove_Ioc, Surreal.bddAbove_range_of_small, ENNReal.iSup_coe_eq_top, bddAbove_empty, Ordinal.mem_closure_tfae, MeasureTheory.Martingale.bddAbove_range_iff_bddBelow_range, Filter.isBoundedUnder_iff_eventually_bddAbove, Ordinal.bddAbove_of_small, bddAbove_Icc, Nimber.not_bddAbove_compl_of_small, bddBelow_inv, Ordinal.bddAbove_iff_small, IsCompact.bddAbove_image, OrderIso.bddAbove_preimage, bddBelow_preimage_ofDual, BddBelow.dual, bddAbove_range_pi, Set.finite_iff_bddAbove, StrictAnti.not_bddBelow_range_of_isSuccArchimedean, PowerSeries.IsRestricted.convergenceSet_BddAbove, Archimedean.ratLt_bddAbove, IsMaxOn.bddAbove, SetTheory.Game.bddAbove_range_of_small, ENat.iSup_coe_eq_top, Finite.bddAbove_range, subset_sSup_def, Cardinal.bddAbove_iff_small, bddAbove_insert, Set.finite_iff_bddBelow_bddAbove, BddBelow.inv, IsGreatest.bddAbove, NNReal.bddAbove_natCast_image_iff, IsUpperSet.not_bddAbove, WithTop.iSup_coe_eq_top, Real.not_bddAbove_coe, IsOrderBornology.isBounded_iff_bddBelow_bddAbove, not_bddAbove_iff, isBounded_iff_bddBelow_bddAbove, bddAbove_preimage_ofDual, Real.sSup_def, bddAbove_closure, ContinuousLinearMap.bddAbove_rayleighQuotient, Set.Nonempty.bddAbove_lowerBounds, SetTheory.Game.bddAbove_of_small, SetTheory.PGame.bddAbove_range_of_small, Cardinal.bddAbove_of_small, not_bddAbove_iff', BddBelow.range_inv, Set.PartiallyWellOrderedOn.bddAbove_preimage, bddAbove_smul_iff_of_pos, bddBelow_neg, Surreal.bddAbove_of_small, LinearOrderedField.cutMap_bddAbove, Antitone.map_bddBelow, Filter.Tendsto.bddAbove_range_of_cofinite, Set.Finite.bddAbove, bddAbove_def, Filter.bddAbove_range_of_tendsto_atTop_atBot, Filter.IsBoundedUnder.bddAbove_range, Ordinal.not_bddAbove_compl_of_small, NNRat.bddAbove_coe, bddAbove_Ioo, seminormFromBounded_bddAbove_range, Filter.IsBoundedUnder.bddAbove_range_of_cofinite, AntitoneOn.map_bddBelow, iUnion_Iio_eq_univ_iff, bddAbove_Ico, Bornology.IsBounded.bddAbove, bddAbove_range_partialSups, IsLUB.bddAbove, bddAbove_preimage_toDual, measurableSet_bddAbove_range, NNReal.bddAbove_coe, bddAbove_smul_iff_of_neg, Continuous.bddAbove_range_of_hasCompactSupport, bddAbove_Iic, CauchySeq.mul_norm_bddAbove, UpperSemicontinuousOn.bddAbove_of_isCompact, ENat.iSup_coe_lt_top, NNReal.bddAbove_range_natCast_iff, BddBelow.range_neg, Memℓp.bddAbove, Archimedean.ratLt'_bddAbove, Continuous.bddAbove_range_of_hasCompactMulSupport, CauchySeq.norm_bddAbove, bddAbove_lowerClosure
|
BddBelow 📖 | MathDef | 116 mathmath: IsCompact.bddBelow, bddBelow_bddAbove_iff_subset_Icc, bddBelow_smul_iff_of_neg, BddAbove.image2_bddBelow, bddBelow_upperClosure, bddBelow_insert, orderBornology_isBounded, Bornology.IsBounded.bddBelow, bddBelow_closure, Set.nonempty_iInter_Iic_iff, bddBelow_Ici, bddAbove_neg, bddBelow_def, MeasureTheory.SignedMeasure.bddBelow_measureOfNegatives, bddBelow_range_pi, bddBelow_Ioc, bddAbove_inv, IsGLB.bddBelow, IsLowerSet.not_bddBelow, not_bddBelow_Iic, NNReal.bddBelow_coe, bddBelow_Ioi, Filter.bddBelow_range_of_tendsto_atTop_atTop, ContinuousAlternatingMap.bounds_bddBelow, not_bddBelow_iff, bddBelow_preimage_toDual, BddAbove.range_neg, PiTensorProduct.bddBelow_projectiveSemiNormAux, ContinuousLinearMap.bounds_bddBelow, OrderIso.bddBelow_preimage, StrictMono.not_bddBelow_range_of_isPredArchimedean, bddBelow_empty, AddGroupSeminorm.add_bddBelow_range_add, bddBelow_union, bddBelow_prod, Set.bdd_below_bdd_above_iff_subset_uIcc, BddAbove.inv, Filter.IsBoundedUnder.bddBelow_range, Surreal.bddBelow_range_of_small, Continuous.bddBelow_range_of_hasCompactSupport, IsMinOn.bddBelow, LaurentSeries.Cauchy.coeff_support_bddBelow, SetTheory.Game.bddBelow_of_small, NNRat.bddBelow_coe, ContinuousMultilinearMap.bounds_bddBelow, BddAbove.neg, BddAbove.range_inv, bddBelow_iff_exists_le, AntitoneOn.map_bddAbove, LowerSemicontinuousOn.bddBelow_of_isCompact, Set.finite_iff_bddBelow, Set.Nonempty.bddBelow_upperBounds, Filter.Tendsto.bddBelow_range, SetTheory.PGame.bddBelow_of_small, MeasureTheory.Martingale.bddAbove_range_iff_bddBelow_range, GaloisConnection.bddBelow_u_image, bddBelow_inv, Set.Finite.bddBelow, Filter.IsBoundedUnder.bddBelow_range_of_cofinite, Filter.Tendsto.bddBelow_range_of_cofinite, NormedAddGroupHom.bounds_bddBelow, bddBelow_preimage_ofDual, bddBelow_slope_lt_of_mem_interior, Filter.not_bddBelow_of_tendsto_atBot, NonarchAddGroupSeminorm.add_bddBelow_range_add, upperClosure_eq_bot_iff, Seminorm.bddBelow_range_add, Finite.bddBelow_range, GromovHausdorff.HD_below_aux2, bddBelow_iff_subset_Ici, Finset.bddBelow, bddBelow_Ico, BddAbove.dual, SetTheory.PGame.bddBelow_range_of_small, Set.Finite.bddBelow_biUnion, Surreal.bddBelow_of_small, bddBelow_Ioo, Set.finite_iff_bddBelow_bddAbove, Real.not_bddBelow_coe, MonotoneOn.map_bddBelow, StrictAnti.not_bddBelow_range_of_isPredArchimedean, smoothingSeminormSeq_bddBelow, bddBelow_Icc, IsOrderBornology.isBounded_iff_bddBelow_bddAbove, BddAbove.smul_of_nonpos, isBounded_iff_bddBelow_bddAbove, bddBelow_pi, Filter.isBoundedUnder_iff_eventually_bddBelow, bddAbove_preimage_ofDual, not_bddBelow_univ, SetTheory.Game.bddBelow_range_of_small, iInter_Iic_eq_empty_iff, HahnSeries.forallLTEqZero_supp_BddBelow, bddBelow_smul_iff_of_pos, OrderBot.bddBelow, bddBelow_neg, OrderIso.bddBelow_image, Continuous.bddBelow_range_of_hasCompactMulSupport, seminormFromConst_bddBelow, IsCompact.bddBelow_image, StrictMono.not_bddBelow_range_of_wellFoundedGT, bddBelow_singleton, measurableSet_bddBelow_range, subset_sInf_def, SimpleGraph.chromaticNumber_bddBelow, not_bddBelow_Iio, GroupSeminorm.mul_bddBelow_range_add, bddAbove_preimage_toDual, not_bddBelow_iff', bddAbove_smul_iff_of_neg, IsLeast.bddBelow, bddBelow_range_prod, GromovHausdorff.HD_below_aux1, HahnSeries.BddBelow_zero, Set.Infinite.not_bddBelow, Antitone.map_bddAbove
|
IsCofinal 📖 | MathDef | 11 mathmath: not_isCofinal_iff, IsCofinal.singleton_top, IsCofinal.of_not_bddAbove, not_bddAbove_iff_isCofinal, not_isCofinal_iff_bddAbove, IsCofinal.of_isEmpty, isCofinal_empty_iff, isCofinal_setOf_imp_lt, IsCofinal.univ, isCofinal_iff_top_mem, Order.Cofinal.isCofinal
|
IsCofinalFor 📖 | MathDef | 6 mathmath: IsCofinalFor.of_subset, DirectedOn.isCofinalFor_fst_image_prod_snd_image, IsCoinitialFor.image_of_antitone, HasSubset.Subset.iscofinalfor, HasSubset.Subset.isCofinalFor, IsCofinalFor.rfl
|
IsCoinitial 📖 | MathDef | — |
IsCoinitialFor 📖 | MathDef | 5 mathmath: HasSubset.Subset.isCoinitialFor, HasSubset.Subset.iscoinitialfor, IsCofinalFor.image_of_antitone, IsCoinitialFor.rfl, IsCoinitialFor.of_subset
|
IsGLB 📖 | MathDef | 84 mathmath: isLUB_lowerBounds, Real.isGLB_of_tendsto_antitone_bddBelow, isGLB_empty_iff, OrderIso.isGLB_preimage', OrderIso.isGLB_image', isGLB_infClosure, isGLB_inv', IsMinOn.isGLB, OrderIso.isGLB_image, isGLB_Ioi, isGLB_Ico, isGLB_ciInf, isGLB_iff_le_iff, Finset.isGLB_inf, isLUB_inv, IsLeast.isGLB, IsLUB.inv, isLUB_neg', isGLB_empty, OrderIso.isGLB_preimage, isGLB_biInf, Order.isGLB_Ioi_iff_isPredPrelimit, DirectedOn.isGLB_ciInf_set, isGLB_inv, isGLB_Ioo, isGLB_neg, isGLB_pair, IsCoatomistic.isGLB_coatoms, Preorder.hasLimit_iff_hasGLB, isGLB_pi, isGLB_upperBounds, isCoatomistic_iff, isGLB_Ici, isLUB_inv', isGLB_Icc, isGLB_iff_sInf_eq, LinearLocallyFiniteOrder.succFn_spec, isLUB_neg, Dense.isGLB_inter_iff, isGLB_ciInf_set, isGLB_of_mem_closure, isGLB_sInf, Real.isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici, Order.IsPredPrelimit.isGLB_Ioi, IsCompact.isGLB_sInf, WithTop.isGLB_sInf, isGLB_csInf, isGLB_of_tendsto_atBot, IsGLB.range_of_tendsto, IsLUB.isGLB_of_tendsto, IsLUB.dual, isGLB_neg', GaloisConnection.isGLB_l, isGLB_iff_of_subset_of_subset_closure, Finset.isGLB_iff_isLeast, CategoryTheory.Pretopology.isGLB_sInf, IsCompact.exists_isGLB, isGLB_singleton, ConditionallyCompletePartialOrder.isGLB_csInf_of_directed, CategoryTheory.GrothendieckTopology.isGLB_sInf, isGLB_Ioc, ConditionallyCompletePartialOrderInf.isGLB_csInf_of_directed, WithTop.isGLB_sInf', isGLB_univ, isGLB_image2_of_isLUB_isLUB, Finset.isGLB_inf_id, isGLB_iInf, isGLB_prod, Directed.isGLB_ciInf, isGLB_congr, IsLUB.neg, Metric.isGLB_infDist, Finset.isGLB_inf', Real.isGLB_sInf, Real.exists_isGLB, LieSubalgebra.sInf_glb, Subfield.isGLB_sInf, exists_glb_Ioi, ClosureOperator.closure_isGLB, isGLB_of_tendsto_atTop, DirectedOn.isGLB_csInf, Order.IsPredLimit.isGLB_Ioi, Preorder.isGLB_of_isLimit, isGLB_of_mem_nhds
|
IsGreatest 📖 | MathDef | 50 mathmath: GaloisConnection.isGreatest_u, IsometricContinuousFunctionalCalculus.isGreatest_nnnorm_spectrum, isGreatest_univ, IsGreatest.nnnorm_cfcₙ, Valuation.Integers.isPrincipal_iff_exists_isGreatest, isGreatest_union_iff, isGreatest_Ioc, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum, IsLeast.isGreatest_image2, DirectedOn.maximal_iff_isGreatest, IsLeast.dual, IsGreatest.nnnorm_cfc_nnreal, StrictMono.map_isGreatest, NNReal.isGreatest_Lp, IsGreatest.norm_cfcₙ, IsGreatest.norm_cfc, IsGreatest.nnnorm_cfc, Filter.countableGenerate_isGreatest, IsGreatest.nnnorm_cfcₙ_nnreal, Finset.isGreatest_max', isGreatest_himp, BddAbove.exists_isGreatest_of_nonempty, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_norm_quasispectrum, Int.isGreatest_coe_greatestOfBdd, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnnorm_quasispectrum, Antitone.map_isLeast, isGreatest_top_iff, IsAntichain.greatest_iff, isGreatest_compl, isGreatest_Iic, IsClosed.isGreatest_csSup, OrderHom.isGreatest_gfp_le, StrictAnti.map_isGreatest, MeasureTheory.OuterMeasure.isGreatest_ofFunction, isAntichain_and_greatest_iff, isGreatest_pair, Polynomial.isGreatest_supNorm, OrderHom.isGreatest_gfp, StrictAnti.map_isLeast, isGreatest_univ_iff, maximal_iff_isGreatest, isGreatest_Icc, IsometricContinuousFunctionalCalculus.isGreatest_norm_spectrum, IsCompact.exists_isGreatest, AntitoneOn.map_isLeast, IsCompact.isGreatest_sSup, IsometricContinuousFunctionalCalculus.isGreatest_spectrum, isGreatest_singleton, Filter.cardinalGenerate_isGreatest, Finset.isLUB_iff_isGreatest
|
IsLeast 📖 | MathDef | 53 mathmath: IsCompact.exists_isLeast, IsGreatest.isLeast_image2, isLeast_Icc, isLeast_csInf, isLeast_sdiff, IsCompact.isLeast_sInf, Field.Emb.Cardinal.isLeast_leastExt, isAntichain_and_least_iff, ChainCompletePartialOrder.IsAdmissible.base_isLeast, isLeast_Ici, ContinuousMultilinearMap.isLeast_opNorm, IsGreatest.dual, isLeast_Ico, OrderHom.isLeast_lfp, Int.gcd_least_linear, minimal_iff_isLeast, Nat.isLeast_nth, ContinuousLinearMap.isLeast_opNNNorm, ContinuousAlternatingMap.isLeast_opNorm, Nat.isLeast_nth_of_infinite, BddBelow.exists_isLeast_of_nonempty, isLeast_pair, GaloisConnection.isLeast_l, ContinuousMultilinearMap.isLeast_opNNNorm, Subgroup.exists_isLeast_one_lt, Set.Nonempty.isLeast_natFind, Antitone.map_isGreatest, AntitoneOn.map_isGreatest, ContinuousAlternatingMap.isLeast_opNNNorm, isLeast_hnot, Convex.toCone_isLeast, StrictAnti.map_isGreatest, Finset.isGLB_iff_isLeast, convexHull_toCone_isLeast, isLeast_singleton, isLeast_univ_iff, AddSubgroup.isLeast_of_closure_iff_eq_abs, StrictAnti.map_isLeast, AddSubgroup.exists_isLeast_pos, Nat.isLeast_find, isLeast_bot_iff, IsAntichain.least_iff, isLeast_union_iff, Nat.isLeast_nth_of_lt_card, ContinuousLinearMap.isLeast_opNorm, IsClosed.isLeast_csInf, StrictMono.map_isLeast, Subgroup.isLeast_of_closure_iff_eq_mabs, OrderHom.isLeast_lfp_le, Int.isLeast_coe_leastOfBdd, isLeast_univ, Finset.isLeast_min', DirectedOn.minimal_iff_isLeast
|
lowerBounds 📖 | CompOp | 80 mathmath: isLUB_lowerBounds, Preorder.conePt_mem_lowerBounds, lowerBounds_smul_of_pos, mem_lowerBounds_image2_of_mem_upperBounds, IsLowerSet.lowerBounds_subset, IsGLB.mem_lowerBounds_of_tendsto, lowerBounds_singleton, Filter.sSup_lowerBounds, IsLUB.mem_lowerBounds_of_tendsto, lowerBounds_Ioc, StrictAnti.mem_upperBounds_image, union_lowerBounds_subset_lowerBounds_inter, NoBotOrder.lowerBounds_univ, image2_lowerBounds_lowerBounds_subset_lowerBounds_image2, gc_upperBounds_lowerBounds, isGLB_iff_le_iff, csSup_lowerBounds_eq_csInf, mem_lowerBounds, Antitone.lowerBounds_range_comp_tendsto_atTop, lowerBounds_union, GaloisConnection.lowerBounds_u_image, lowerBounds_mono_of_isCoinitialFor, lowerBounds_mono_set, exists_between_of_forall_le, Order.IsNormal.mem_lowerBounds_upperBounds_of_isSuccLimit, lowerBounds_upperClosure, lowerBounds_Ioo, upperBounds_smul_of_neg, image2_lowerBounds_upperBounds_subset_lowerBounds_image2, AntitoneOn.image_upperBounds_subset_lowerBounds_image, Monotone.lowerBounds_range_comp_tendsto_atBot, lowerBounds_Icc, StrictAnti.mem_lowerBounds_image, sSup_lowerBounds_eq_sInf, lowerBounds_prod, lowerBounds_infClosure, image2_upperBounds_lowerBounds_subset_lowerBounds_image2, StrictMono.mem_lowerBounds_image, IsLeast.lowerBounds_eq, smul_upperBounds_subset_lowerBounds_smul, le_csInf_iff', AntitoneOn.image_lowerBounds_subset_upperBounds_image, lowerBounds_smul_of_neg, Order.isNormal_iff', image2_upperBounds_upperBounds_subset_upperBounds_image2, bot_mem_lowerBounds, smul_lowerBounds_subset_lowerBounds_smul_of_nonneg, subset_upperBounds_lowerBounds, image2_upperBounds_lowerBounds_subset_upperBounds_image2, OrderIso.lowerBounds_image, zero_mem_lowerBounds_smoothingSeminormSeq_range, lowerBounds_Ico, smul_lowerBounds_subset_upperBounds_smul, le_isGLB_iff, mem_lowerBounds_iff_subset_Ici, image2_lowerBounds_lowerBounds_subset, lowerBounds_iUnion, lowerBounds_insert, subset_lowerBounds_upperBounds, Set.Nonempty.bddAbove_lowerBounds, subset_lowerBounds_mul, Monotone.image_lowerBounds_subset_lowerBounds_image, AntitoneOn.mem_lowerBounds_image, image2_lowerBounds_upperBounds_subset_upperBounds_image2, MonotoneOn.image_lowerBounds_subset_lowerBounds_image, Dense.lowerBounds_image, subset_lowerBounds_add, lt_isGLB_iff, lowerBounds_empty, lowerBounds_closure, Antitone.mem_lowerBounds_image, AntitoneOn.mem_lowerBounds_image_self, OrderBot.lowerBounds_univ, IsGLB.lowerBounds_eq, isLeast_union_iff, csSup_lowerBounds_range, Antitone.image_upperBounds_subset_lowerBounds_image, Antitone.image_lowerBounds_subset_upperBounds_image, lowerBounds_Ici, lowerBounds_Ioi
|
upperBounds 📖 | CompOp | 81 mathmath: upperBounds_supClosure, Monotone.image_upperBounds_subset_upperBounds_image, upperBounds_mono_set, upperBounds_Iic, mem_upperBounds_image2_of_mem_lowerBounds, isGreatest_union_iff, isLUB_iff_le_iff, union_upperBounds_subset_upperBounds_inter, upperBounds_empty, upperBounds_iUnion, Preorder.coconePt_mem_upperBounds, ENNReal.coe_mem_upperBounds, StrictAnti.mem_upperBounds_image, image2_lowerBounds_lowerBounds_subset_lowerBounds_image2, gc_upperBounds_lowerBounds, upperBounds_Ico, AntitoneOn.mem_upperBounds_image, upperBounds_Iio, Antitone.mem_upperBounds_image, subset_upperBounds_mul, IsGreatest.upperBounds_eq, image2_upperBounds_upperBounds_subset, smul_upperBounds_subset_upperBounds_smul_of_nonneg, exists_between_of_forall_le, Order.IsNormal.mem_lowerBounds_upperBounds_of_isSuccLimit, isGLB_upperBounds, upperBounds_smul_of_neg, image2_lowerBounds_upperBounds_subset_lowerBounds_image2, AntitoneOn.image_upperBounds_subset_lowerBounds_image, Monotone.upperBounds_image_of_directedOn_prod, OrderTop.upperBounds_univ, mem_upperBounds_iff_subset_Iic, StrictAnti.mem_lowerBounds_image, isLUB_le_iff, csInf_upperBounds_range, upperBounds_Icc, Set.Nonempty.bddBelow_upperBounds, image2_upperBounds_lowerBounds_subset_lowerBounds_image2, isLUB_lt_iff, Monotone.upperBounds_range_comp_tendsto_atTop, upperBounds_union, upperBounds_mono_of_isCofinalFor, smul_upperBounds_subset_lowerBounds_smul, upperBounds_lowerClosure, upperBounds_Ioc, OrderIso.upperBounds_image, AntitoneOn.image_lowerBounds_subset_upperBounds_image, lowerBounds_smul_of_neg, Order.isNormal_iff', image2_upperBounds_upperBounds_subset_upperBounds_image2, AntitoneOn.mem_upperBounds_image_self, IsLUB.upperBounds_eq, upperBounds_range_partialSups, subset_upperBounds_lowerBounds, image2_upperBounds_lowerBounds_subset_upperBounds_image2, upperBounds_insert, NoTopOrder.upperBounds_univ, smul_lowerBounds_subset_upperBounds_smul, GaloisConnection.upperBounds_l_image, IsUpperSet.upperBounds_subset, subset_upperBounds_add, csInf_upperBounds_eq_csSup, top_mem_upperBounds, upperBounds_Ioo, upperBounds_closure, StrictMono.mem_upperBounds_image, subset_lowerBounds_upperBounds, upperBounds_prod, Antitone.upperBounds_range_comp_tendsto_atBot, upperBounds_singleton, sInf_upperBounds_eq_csSup, sInf_upperBounds_eq_sSup, image2_lowerBounds_upperBounds_subset_upperBounds_image2, MonotoneOn.image_upperBounds_subset_upperBounds_image, Dense.upperBounds_image, Antitone.image_upperBounds_subset_lowerBounds_image, upperBounds_smul_of_pos, Antitone.image_lowerBounds_subset_upperBounds_image, mem_upperBounds, IsLUB.mem_upperBounds_of_tendsto, IsGLB.mem_upperBounds_of_tendsto
|