| Name | Category | Theorems |
|---|
BddAbove 📖 | MathDef | 185 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.range_comp_of_nonneg, BddAbove.of_lowerClosure, BddAbove.range_add, bddAbove_union, Nat.not_bddAbove_setOf_prime, Cardinal.bddAbove_ord_image_iff, bddAbove_neg, Complex.HadamardThreeLines.F_BddAbove, MonotoneOn.map_bddAbove, BddBelow.image2_bddAbove, Seminorm.bddAbove_of_absorbent, Ordinal.not_bddAbove_isInitial, BddBelow.bddAbove_image2_of_bddAbove, BddAbove.add, bddAbove_inv, spectralValueTerms_bddAbove, AddAction.period_bounded_of_exponent_pos, Ordinal.bddAbove_range_add_one_iff, 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, ConvexOn.bddAbove_convexHull, 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.smul_of_nonneg, bddAbove_iff_subset_Iic, bddAbove_Iio, Set.BddAbove.mul, StrictMono.not_bddAbove_range_of_wellFoundedLT, Ordinal.not_bddAbove_setOf_isPrincipal, Urysohns.CU.bddAbove_range_approx, Seminorm.bddAbove_iff, MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto_aux, BddAbove.insert, 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, SchauderBasis.bddAbove_range_nnnorm_proj, not_isCofinal_iff_bddAbove, Cardinal.bddAbove_range, WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup, WithTop.iSup_coe_lt_top, BddAbove.bddAbove_image2_of_bddBelow, BddAbove.image2, not_bddAbove_Ici, not_bddAbove_univ, NormedSpace.equicontinuous_TFAE, PiTensorProduct.dualSeminorms_bounded, Set.nonempty_iInter_Ici_iff, Monotone.map_bddAbove, Ordinal.bddAbove_range, bddAbove_singleton, MeasureTheory.upperCrossingTime_lt_bddAbove, MulAction.period_bounded_of_exponent_pos, Cardinal.bddAbove_image, bddAbove_Ioc, ENNReal.iSup_coe_eq_top, bddAbove_empty, Cardinal.bddAbove_range_comp, Ordinal.mem_closure_tfae, MeasureTheory.Martingale.bddAbove_range_iff_bddBelow_range, Filter.isBoundedUnder_iff_eventually_bddAbove, Ordinal.bddAbove_of_small, bddAbove_Icc, bddBelow_inv, bddAbove_range_mul, Ordinal.bddAbove_iff_small, IsCompact.bddAbove_image, OrderIso.bddAbove_preimage, bddBelow_preimage_ofDual, BddBelow.dual, BddAbove.mul, bddAbove_range_pi, Set.finite_iff_bddAbove, BddAbove.closure, PowerSeries.IsRestricted.convergenceSet_BddAbove, Archimedean.ratLt_bddAbove, IsMaxOn.bddAbove, ENat.iSup_coe_eq_top, BddAbove.lowerClosure, 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, Complex.HadamardThreeLines.scale_bddAbove, BddAbove.range_iSup_of_iUnion_range, IsOrderBornology.isBounded_iff_bddBelow_bddAbove, not_bddAbove_iff, isBounded_iff_bddBelow_bddAbove, bddAbove_preimage_ofDual, Real.sSup_def, Set.BddAbove.add, UnconditionalSchauderBasis.bddAbove_range_nnnorm_proj, bddAbove_closure, ContinuousLinearMap.bddAbove_rayleighQuotient, StrictMono.not_bddBelow_range_of_isSuccArchimedean, Set.Nonempty.bddAbove_lowerBounds, Cardinal.bddAbove_of_small, BddAbove.union, not_bddAbove_iff', BddAbove.range_mono, BddBelow.range_inv, Set.PartiallyWellOrderedOn.bddAbove_preimage, BddAbove.inter_of_right, bddAbove_smul_iff_of_pos, Ordinal.bddAbove_range_comp, bddBelow_neg, StrictAnti.not_bddAbove_range_of_isSuccArchimedean, LinearOrderedField.cutMap_bddAbove, Antitone.map_bddBelow, Filter.Tendsto.bddAbove_range_of_cofinite, Set.Finite.bddAbove, bddAbove_def, Filter.bddAbove_range_of_tendsto_atTop_atBot, BddAbove.range_mul, Filter.IsBoundedUnder.bddAbove_range, Ordinal.not_bddAbove_compl_of_small, NNRat.bddAbove_coe, BddAbove.range_comp, bddAbove_Ioo, seminormFromBounded_bddAbove_range, Filter.IsBoundedUnder.bddAbove_range_of_cofinite, AntitoneOn.map_bddBelow, iUnion_Iio_eq_univ_iff, Ordinal.bddAbove_image, bddAbove_Ico, Bornology.IsBounded.bddAbove, bddAbove_range_partialSups, IsLUB.bddAbove, bddAbove_preimage_toDual, measurableSet_bddAbove_range, BddAbove.inter_of_left, NNReal.bddAbove_coe, bddAbove_smul_iff_of_neg, Continuous.bddAbove_range_of_hasCompactSupport, BddAbove.of_closure, bddAbove_Iic, CauchySeq.mul_norm_bddAbove, UpperSemicontinuousOn.bddAbove_of_isCompact, ENat.iSup_coe_lt_top, Ordinal.bddAbove_add_one_image_iff, BddAbove.mono, 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 | 132 mathmath: IsCompact.bddBelow, bddBelow_bddAbove_iff_subset_Icc, bddBelow_smul_iff_of_neg, BddBelow.upperClosure, BddAbove.image2_bddBelow, bddBelow_upperClosure, BddBelow.range_mono, bddBelow_insert, orderBornology_isBounded, Bornology.IsBounded.bddBelow, bddBelow_closure, Set.nonempty_iInter_Iic_iff, BddBelow.insert, BddBelow.closure, 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, BddAbove.bddBelow_image2_of_bddBelow, NNReal.bddBelow_coe, bddBelow_Ioi, BddBelow.of_upperClosure, BddBelow.bddBelow_image2_of_bddAbove, BddBelow.range_comp, Filter.bddBelow_range_of_tendsto_atTop_atTop, ContinuousAlternatingMap.bounds_bddBelow, BddBelow.add, BddBelow.inter_of_left, BddBelow.union, not_bddBelow_iff, bddBelow_preimage_toDual, BddAbove.range_neg, PiTensorProduct.bddBelow_projectiveSemiNormAux, BddBelow.range_add, 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, Continuous.bddBelow_range_of_hasCompactSupport, IsMinOn.bddBelow, LaurentSeries.Cauchy.coeff_support_bddBelow, NNRat.bddBelow_coe, ContinuousMultilinearMap.bounds_bddBelow, BddAbove.neg, BddAbove.range_inv, bddBelow_iff_exists_le, AntitoneOn.map_bddAbove, BddBelow.range_mul, LowerSemicontinuousOn.bddBelow_of_isCompact, Set.finite_iff_bddBelow, Set.Nonempty.bddBelow_upperBounds, Filter.Tendsto.bddBelow_range, BddBelow.of_closure, 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, BddBelow.mono, NonarchAddGroupSeminorm.add_bddBelow_range_add, BddBelow.range_iInf_of_iUnion_range, 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, Set.Finite.bddBelow_biUnion, bddBelow_Ioo, Set.finite_iff_bddBelow_bddAbove, Real.not_bddBelow_coe, MonotoneOn.map_bddBelow, StrictAnti.not_bddBelow_range_of_isPredArchimedean, smoothingSeminormSeq_bddBelow, bddBelow_Icc, BddBelow.image2, IsOrderBornology.isBounded_iff_bddBelow_bddAbove, BddAbove.smul_of_nonpos, Monotone.map_bddBelow, isBounded_iff_bddBelow_bddAbove, bddBelow_pi, Filter.isBoundedUnder_iff_eventually_bddBelow, bddAbove_preimage_ofDual, not_bddBelow_univ, iInter_Iic_eq_empty_iff, HahnSeries.forallLTEqZero_supp_BddBelow, bddBelow_smul_iff_of_pos, OrderBot.bddBelow, bddBelow_neg, ConcaveOn.bddBelow_convexHull, 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, BddBelow.mul, not_bddBelow_Iio, BddBelow.smul_of_nonneg, BddBelow.inter_of_right, 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 | 32 mathmath: Cardinal.unbounded_of_unbounded_sUnion, not_isCofinal_iff, GaloisConnection.map_isCofinal, IsCofinal.singleton_top, IsCofinal.of_not_bddAbove, OrderIso.map_isCofinal, isCofinal_singleton_iff, isCofinal_iff_iUnion_Iic_eq_univ, Set.Finite.exists_subsingleton_isCofinal, IsCofinal.trans, OrderIso.map_cofinal, not_bddAbove_iff_isCofinal, not_isCofinal_iff_bddAbove, IsCofinal.of_isEmpty, GaloisConnection.isCofinal_range, Order.cof_eq, isCofinal_empty_iff, Ordinal.ord_cof_eq, IsCofinal.image, isCofinal_of_isCofinal_sUnion, isCofinal_setOf_imp_lt, IsCofinal.univ, isCofinal_iff_iUnion_Iio_eq_univ, OrderIso.map_isCofinal_iff, Ordinal.cof_eq, IsCofinal.mono, GaloisConnection.map_cofinal, isCofinal_iff_top_mem, Ordinal.IsFundamentalSeq.isCofinal_range, Cardinal.unbounded_of_unbounded_iUnion, Order.Cofinal.isCofinal, isCofinal_of_isCofinal_iUnion
|
IsCofinalFor 📖 | MathDef | 10 mathmath: IsCofinalFor.of_subset, IsCofinalFor.image_of_monotone, DirectedOn.isCofinalFor_fst_image_prod_snd_image, IsCofinalFor.mono_right, IsCoinitialFor.image_of_antitone, HasSubset.Subset.iscofinalfor, HasSubset.Subset.isCofinalFor, IsCofinalFor.rfl, IsCofinalFor.mono_left, IsCofinalFor.trans
|
IsCoinitial 📖 | MathDef | — |
IsCoinitialFor 📖 | MathDef | 9 mathmath: HasSubset.Subset.isCoinitialFor, IsCoinitialFor.mono_right, IsCoinitialFor.image_of_monotone, HasSubset.Subset.iscoinitialfor, IsCoinitialFor.trans, IsCofinalFor.image_of_antitone, IsCoinitialFor.rfl, IsCoinitialFor.of_subset, IsCoinitialFor.mono_left
|
IsGLB 📖 | MathDef | 113 mathmath: isLUB_lowerBounds, Real.isGLB_of_tendsto_antitone_bddBelow, GaloisCoinsertion.isGLB_of_l_image, isGLB_empty_iff, OrderIso.isGLB_preimage', IsGLB.of_image, Filter.isGLB_sInf, OrderIso.isGLB_image', isGLB_infClosure, isGLB_image2_of_isGLB_isLUB, isGLB_inv', IsMinOn.isGLB, OrderIso.isGLB_image, IsGLB.mul_left, isGLB_Ioi, isGLB_Ico, isGLB_ciInf, IsGLB.of_subset_of_superset, isGLB_image2_of_isLUB_isGLB, 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, GaloisInsertion.isGLB_of_u_image, isGLB_upperBounds, isCoatomistic_iff, isGLB_Ici, IsGLB.isGLB_of_tendsto, IsGLB.mul, isLUB_inv', exists_countable_upperSemicontinuous_isGLB, CompleteSemilatticeInf.isGLB_sInf, IsGLB.div, isGLB_Icc, isGLB_iff_sInf_eq, CompleteLattice.isGLB_sInf, LinearLocallyFiniteOrder.succFn_spec, isLUB_neg, Dense.isGLB_inter_iff, IsGLB.sub, isGLB_ciInf_set, isGLB_of_mem_closure, isGLB_sInf, ConditionallyCompleteLattice.isGLB_csInf, 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.insert, IsGLB.range_of_tendsto, IsLUB.isGLB_of_tendsto, IsLUB.dual, isGLB_neg', GaloisConnection.isGLB_l, IsGLB.inter_Iic_of_mem, isGLB_iff_of_subset_of_subset_closure, Finset.isGLB_iff_isLeast, isGLB_image2_of_isGLB_isGLB, CategoryTheory.Pretopology.isGLB_sInf, IsGLB.union, IsCompact.exists_isGLB, isGLB_singleton, ConditionallyCompletePartialOrder.isGLB_csInf_of_directed, CategoryTheory.GrothendieckTopology.isGLB_sInf, SimpleGraph.isGLB_turanDensity, isGLB_Ioc, LinearLocallyFiniteOrder.isGLB_Ioc_of_isGLB_Ioi, ConditionallyCompletePartialOrderInf.isGLB_csInf_of_directed, GaloisConnection.isGLB_u_image, WithTop.isGLB_sInf', isGLB_univ, IsGLB.prod, isGLB_image2_of_isLUB_isLUB, Finset.isGLB_inf_id, isGLB_iUnion_iff_of_isLUB, isGLB_iInf, isGLB_prod, Directed.isGLB_ciInf, isGLB_congr, IsLUB.neg, Metric.isGLB_infDist, Finset.isGLB_inf', Real.isGLB_sInf, IsGLB.mul_right, Real.exists_isGLB, UniformSpace.isGLB_sInf, LieSubalgebra.sInf_glb, Subfield.isGLB_sInf, exists_glb_Ioi, ClosureOperator.closure_isGLB, isGLB_of_tendsto_atTop, DirectedOn.isGLB_csInf, Submodule.isGLB_sInf, Order.IsPredLimit.isGLB_Ioi, Preorder.isGLB_of_isLimit, IsGLB.add, isGLB_of_mem_nhds
|
IsGreatest 📖 | MathDef | 61 mathmath: GaloisConnection.isGreatest_u, IsometricContinuousFunctionalCalculus.isGreatest_nnnorm_spectrum, isGreatest_univ, sigNeg_isGreatest, IsGreatest.nnnorm_cfcₙ, Valuation.Integers.isPrincipal_iff_exists_isGreatest, isGreatest_union_iff, isGreatest_Ioc, NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum, IsLeast.isGreatest_image2, IsGreatest.insert, DirectedOn.maximal_iff_isGreatest, sigPos_isGreatest, MonotoneOn.map_isGreatest, IsLeast.dual, IsGreatest.isGreatest_iff_eq, IsGreatest.nnnorm_cfc_nnreal, IsGreatest.isGreatest_image2_of_isLeast, 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, IsLeast.isGreatest_image2_of_isGreatest, Antitone.map_isLeast, isGreatest_top_iff, IsAntichain.greatest_iff, isGreatest_compl, isGreatest_Iic, Monotone.map_isGreatest, IsClosed.isGreatest_csSup, OrderHom.isGreatest_gfp_le, StrictAnti.map_isGreatest, MeasureTheory.OuterMeasure.isGreatest_ofFunction, IsGreatest.image2, 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, LeftOrdContinuous.map_isGreatest, IsometricContinuousFunctionalCalculus.isGreatest_spectrum, isGreatest_singleton, Filter.cardinalGenerate_isGreatest, IsGreatest.union, Finset.isLUB_iff_isGreatest
|
IsLeast 📖 | MathDef | 62 mathmath: IsCompact.exists_isLeast, IsGreatest.isLeast_image2, IsLeast.image2, IsLeast.insert, isLeast_Icc, isLeast_csInf, Monotone.map_isLeast, 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, IsLeast.isLeast_image2_of_isGreatest, 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.isLeast_iff_eq, MonotoneOn.map_isLeast, isLeast_singleton, RightOrdContinuous.map_isLeast, 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, IsGreatest.isLeast_image2_of_isLeast, Nat.isLeast_nth_of_lt_card, ContinuousLinearMap.isLeast_opNorm, IsLeast.union, 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 | 93 mathmath: isLUB_lowerBounds, Monotone.mem_lowerBounds_image, mul_mem_lowerBounds_mul, mem_lowerBounds_image2, 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, lowerBounds_mono, 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, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds, 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, lowerPolar_le, 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_mono_mem, lowerBounds_iUnion, lowerBounds_insert, subset_lowerBounds_upperBounds, Set.Nonempty.bddAbove_lowerBounds, subset_lowerBounds_mul, Monotone.image_lowerBounds_subset_lowerBounds_image, AntitoneOn.mem_lowerBounds_image, add_mem_lowerBounds_add, 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, MonotoneOn.mem_lowerBounds_image_self, AntitoneOn.mem_lowerBounds_image_self, DedekindCut.image_left_subset_lowerBounds, DedekindCut.lowerBounds_right, 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, MonotoneOn.mem_lowerBounds_image
|
upperBounds 📖 | CompOp | 96 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, FirstOrder.Language.DirectLimit.exists_unify_eq, 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, upperBounds_mono, image2_upperBounds_upperBounds_subset, smul_upperBounds_subset_upperBounds_smul_of_nonneg, exists_between_of_forall_le, Order.IsNormal.mem_lowerBounds_upperBounds_of_isSuccLimit, mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds, isGLB_upperBounds, upperBounds_smul_of_neg, image2_lowerBounds_upperBounds_subset_lowerBounds_image2, AntitoneOn.image_upperBounds_subset_lowerBounds_image, upperPolar_le, Monotone.upperBounds_image_of_directedOn_prod, OrderTop.upperBounds_univ, mem_upperBounds_iff_subset_Iic, DedekindCut.upperBounds_left, StrictAnti.mem_lowerBounds_image, isLUB_le_iff, csInf_upperBounds_range, upperBounds_mono_mem, upperBounds_Icc, Set.Nonempty.bddBelow_upperBounds, image2_upperBounds_lowerBounds_subset_lowerBounds_image2, isLUB_lt_iff, Monotone.upperBounds_range_comp_tendsto_atTop, mul_mem_upperBounds_mul, 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, MonotoneOn.mem_upperBounds_image_self, AntitoneOn.mem_upperBounds_image_self, IsLUB.upperBounds_eq, Monotone.mem_upperBounds_image, 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, MonotoneOn.mem_upperBounds_image, 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, mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds, add_mem_upperBounds_add, MonotoneOn.image_upperBounds_subset_upperBounds_image, mem_upperBounds_image2, Dense.upperBounds_image, DedekindCut.image_right_subset_upperBounds, FirstOrder.Language.DirectLimit.comp_unify, 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
|