Defs

📁 Source: Mathlib/Order/ConditionallyCompleteLattice/Defs.lean

Statistics

Metric	Count
Definitions ConditionallyCompleteLattice, toInfSet, toLattice, toSupSet, ConditionallyCompleteLinearOrder, toConditionallyCompleteLattice, toDecidableEq, toDecidableLE, toDecidableLT, toOrd, ConditionallyCompleteLinearOrderBot, toConditionallyCompleteLinearOrder, toOrderBot, conditionallyCompleteLinearOrderBot, conditionallyCompleteLatticeOfLatticeOfsInf, conditionallyCompleteLatticeOfLatticeOfsSup, conditionallyCompleteLatticeOfsInf, conditionallyCompleteLatticeOfsSup	18
Theorems isGLB_csInf, isLUB_csSup, compare_eq_compareOfLessAndEq, csInf_of_not_bddBelow, csSup_of_not_bddAbove, le_total, csSup_empty	7
Total	25

ConditionallyCompleteLattice

Definitions

Name	Category	Theorems
toInfSet 📖	CompOp	15 math math: Int.csInf_mem, Int.csInf_eq_least_of_bdd, ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow, le_csInf, csInf_le_of_le, Int.csInf_eq_leastOfBdd, Int.csInf_of_not_bddBelow, IsGLB.csInf_eq, isGLB_csInf, csInf_le_iff, isGLB_csInf, csInf_le, csInf_le_csInf, Int.csInf_of_not_bdd_below, Int.csInf_empty
toLattice 📖	CompOp	1225 math math: NonUnitalSubalgebra.coe_starClosure, MeasureTheory.Measure.MeasureDense.approx, Submodule.finrank_sup_add_finrank_inf_eq, Subalgebra.LinearDisjoint.inf_eq_bot, Nat.iInf_le_succ', AlgebraicGeometry.WeaklyEtale.weaklyEtale_eq_flat_inf_diagonal_flat, csSup_pair, LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, AlgebraicGeometry.descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact', AffineSubspace.direction_inf, Set.Iic.coe_sInf, AffineSubspace.direction_sup_eq_sup_direction, Module.length_compositionSeries, OrderEmbedding.supIrredLowerSet_apply, Module.End.isSemisimple_restrict_iff, continuous_sup_rng_right, Nat.iSup_lt_succ', Submodule.supIndep_torsionBySet_ideal, Algebra.lift_cardinalMk_adjoin_le, complementedLattice_of_complementedLattice_Iic, SymmetricAlgebra.rank_eq, Subgroup.sup_eq_closure_mul, continuousMul_inf, TopCat.Sheaf.interUnionPullbackCone_snd, Set.Finite.einfsep, IntermediateField.LinearDisjoint.iff_inf_eq_bot, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter, IntermediateField.normal_inf, Cardinal.powerlt_max, AlgebraicGeometry.descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact, LinearMap.map_le_map_iff, StarSubalgebra.map_inf, RootPairing.instNontrivialSubtypeSubmoduleMemSublatticeInvtRootSubmodule, AlgebraicGeometry.RingedSpace.basicOpen_res, Finpartition.isPartition_parts, Set.einfsep_of_fintype, AddGroupTopology.toTopologicalSpace_inf, Ordinal.max_zero_left, IntermediateField.extendScalars_sup, Cardinal.mk_list_eq_max_mk_aleph0, Submodule.toConvexCone_inf, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, Cardinal.mk_list_le_max, Module.End.mem_invtSubmodule, CategoryTheory.ObjectProperty.HasCardinalLT.sup, Subalgebra.LinearDisjoint.sup_free_of_free, NonUnitalStarAlgebra.mem_sup_right, AffineSubspace.direction_inf_of_mem, continuous_sup_dom, IntermediateField.relrank_comap_comap_eq_relrank_inf, Filter.bliminf_inf_not, Finset.inf'_univ_eq_ciInf, Filter.blimsup_and_le_inf, IsCompactlyGenerated.BooleanGenerators.complementedLattice_of_sSup_eq_top, StarSubalgebra.mem_sup_left, MeasureTheory.measureReal_symmDiff_le, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_W, Cardinal.mk_multiset_of_nonempty, RootPairing.Base.forall_mem_support_invtSubmodule_iff, LinearMap.IsProj.mem_invtSubmodule_iff, Submodule.mem_sup', MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt, MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetRing, MeasureTheory.hittingAfter_bot_le_iff, TopologicalSpace.Opens.mem_sup, LinearMap.IsIdempotentElem.commute_iff, LinearPMap.domain_supSpanSingleton, CompleteLattice.isCompactElement_finsetSup, Ideal.sum_eq_sup, Subalgebra.comap_map_eq, Subalgebra.finrank_sup_eq_finrank_right_mul_finrank_of_free, Opens.pretopology_toGrothendieck, CompleteSublattice.isComplemented_iff, CategoryTheory.ObjectProperty.instHasInducedTStructureMinOfIsClosedUnderIsomorphisms, ciSup_partialSups_eq', Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, MeasureTheory.hittingBtwn_univ, AlgebraicGeometry.IsAffineOpen.isCompact_pullback_inf, Submodule.isOrtho_sup_right, OrderEmbedding.infIrredUpperSet_surjective, induced_inf, ClosedSubmodule.toSubmodule_sup, GroupTopology.toTopologicalSpace_inf, Submodule.fst_sup_snd, IsCompactlyGenerated.BooleanGenerators.sSup_inter, NonUnitalAlgebra.mem_sup_left, FirstOrder.Language.Substructure.map_sup, DualNumber.range_lift, NonUnitalAlgebra.coe_inf, Ideal.primaryComponent_sup, Cardinal.mul_le_max_of_aleph0_le_right, LocallyConvexSpace.inf, AlgebraicGeometry.isAffineHom_diagonal_iff, PointedCone.dual_sup, Module.End.invtSubmodule.disjoint_mk_iff, LinearEquiv.map_mem_invtSubmodule_conj_iff, Filter.cardinalInterFilter_sup, Cardinal.sum_pow_le_max_aleph0, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMax, StarSubalgebra.inf_toSubalgebra, RootPairing.invtRootSubmodule.eq_span_root, Submodule.sup_eq_sup_smul_of_le_smul_of_le_jacobson, MonoidAlgebra.cardinalMk_of_infinite, Module.End.genEigenspace_mem_invtSubmodule, ConvexCone.coe_inf, csInf_insert, Submodule.mem_invtSubmodule_reflection_of_mem, RootPairing.invtRootSubmodule.bot_mem, Measurable.sup_of_right, RootPairing.invtRootSubmodule.eq_top_iff, Filter.bliminf_sup_le_and, AddSubgroup.normal_add, MeasureTheory.measure_symmDiff_eq_top, Cardinal.mul_eq_max_of_aleph0_le_right, cbiSup_eq_of_not_forall, Topology.IsLower.toContinuousInf, NNReal.segment_eq_uIcc, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin_1, continuous_inf_dom_left₂, AlgebraicGeometry.isPullback_opens_inf, LieSubalgebra.span_union, ENNReal.iInf_ennreal, Subalgebra.rank_sup_eq_rank_left_mul_rank_of_free, Finset.isWF_sup, Cardinal.mk_finsupp_lift_of_infinite, Submodule.coe_sup, ExpGrowth.expGrowthSup_add, ConditionallyCompleteLinearOrderedField.toZeroLEOneClass, TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul, Subfield.map_sup, biUnion_range_succ_disjointed, AddSubgroup.add_normal, Ideal.mul_sup_eq_of_coprime_right, AlgebraicGeometry.isImmersion_eq_inf, TopologicalSpace.Opens.infLELeft_apply_mk, Subgroup.mul_normal, Ideal.comap_finsetInf, Submodule.colon_finsetInf, AlgebraicGeometry.Scheme.IdealSheafData.support_mul, Representation.invtSubmodule.nontrivial_iff, Nat.iInf_lt_succ', ConditionallyCompleteLinearOrder.compare_eq_compareOfLessAndEq, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom, Subfield.cardinalMk_closure_le_max, Subgroup.coe_mul_of_left_le_normalizer_right, AlgebraicGeometry.descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact, Subalgebra.LinearDisjoint.inf_eq_bot_of_commute, Cardinal.mul_eq_left_iff, NumberField.isTotallyReal_sup, continuousAdd_inf, Algebra.map_sup, CategoryTheory.GrothendieckTopology.arrow_intersect, AddSubmonoid.sup_mul, CategoryTheory.GrothendieckTopology.intersection_covering_iff, continuous_inf_dom_right₂, TopCat.Sheaf.interUnionPullbackCone_fst, Ideal.pow_sup_eq_top, Module.End.mem_invtSubmodule_iff_mapsTo, NonUnitalSubalgebra.prod_inf_prod, AlgebraicGeometry.IsSeparated.eq_valuativeCriterion, generateFrom_union, exists_mem_uIcc_isFixedPt, iSup_partialSups_eq, isFiniteLength_iff_exists_compositionSeries, isOpen_sup, Submodule.comap_smul_top_of_surjective, Sylow.normalizer_sup_eq_top', NonUnitalAlgebra.mem_sup_right, Subalgebra.unop_sup, AlgebraicGeometry.IsClosedImmersion.eq_proper_inf_monomorphisms, LinearMap.range_domRestrict_eq_range_iff, Ideal.pow_sup_pow_eq_top, TopologicalSpace.Closeds.instContinuousSup, Subalgebra.prod_inf_prod, Submodule.comap_map_sup_of_comap_le, LieIdeal.toInvtRootSubmodule_mono, TopCat.pullback_topology, LinearMap.span_singleton_sup_orthogonal_eq_top, IntermediateField.inf_toSubalgebra, OrderIso.infIrredUpperSet_symm_apply, Projectivization.Subspace.span_sup, MeasureTheory.measureReal_symmDiff_eq, IsSemisimpleModule.toComplementedLattice, Algebraic.cardinalMk_le_max, FirstOrder.Language.Substructure.map_sup_comap_of_surjective, TopologicalSpace.NoetherianSpace.exists_finset_irreducible, UniformContinuous.sup_closeds, ConditionallyCompleteLinearOrderedField.toPosMulStrictMono, CategoryTheory.MorphismProperty.IsLocalAtSource.inf, NonUnitalAlgebra.mem_inf, AddSubmonoid.smul_sup, SSet.Subcomplex.degenerate_eq_top_iff, Ideal.smul_sup, CompleteSublattice.sSupClosed', Algebra.IsAlgebraic.cardinalMk_le_max, hasCardinalLT_subtype_max, Ideal.isPrimary_finsetInf, FirstOrder.Language.Substructure.comap_sup_map_of_injective, Subgroup.normalizer_le_normalizer_sup_normal, Submodule.neg_sup, Submodule.sup_eq_range, topologicalGroup_inf, LieSubmodule.lie_top_eq_of_span_sup_eq_top, Submodule.sub_mem_sup, Set.Finset.coe_einfsep, Filter.inf_limsup, Algebra.adjoin_union, topologicalAddGroup_inf, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, Ideal.mem_sup_left, SSet.Subcomplex.preimage_min, Ideal.prod_le_inf, PrimitiveSpectrum.hull_kernel_of_isClosed, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app, AddSubgroup.relIndex_map_map, ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule, AffineSubspace.direction_affineSpan_insert, Finset.sup_univ_eq_ciSup, AffineSubspace.vectorSpan_union_of_mem_of_mem, IntermediateField.inf_relrank_right, beattySeq'_symmDiff_beattySeq_pos, IsAddFoelner.tendsto_meas_vadd_symmDiff_vadd, RootPairing.mem_invtRootSubmodule_iff, MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff', PrimeSpectrum.basicOpen_mul, Ordinal.card_omega0_opow, Submodule.smul_sup', HahnEmbedding.ArchimedeanStrata.ball_sup_stratum_eq, continuousNeg_inf, IntermediateField.sup_toSubalgebra_of_isAlgebraic_left, TopCat.prod_topology, Subrepresentation.toSubmodule_sup, IntermediateField.restrictScalars_sup, Submodule.finiteDimensional_finset_sup, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin, NNReal.image_coe_uIcc, le_csInf, Submodule.submoduleOf_sup_of_le, IsFoelner.tendsto_meas_smul_symmDiff, Dynamics.coverEntropyEntourage_union, MeasurableSpace.generateFrom_sup_generateFrom, OrderIso.supIrredLowerSet_symm_apply, Submonoid.sup_eq_closure_mul, Ideal.IsPrime.inf_le', IsDedekindDomain.range_sup_range_eq_top_of_isCoprime_differentIdeal, Representation.invtSubmodule.coe_top, LieIdeal.rootSpan_mem_invtRootSubmodule, MeasureTheory.OuterMeasure.trim_sup, TopologicalSpace.Opens.mem_inf, Set.definable_finset_sup, Finite.ciSup_sup, AddSubgroup.relIndex_sup_left, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso, MeasureTheory.IsSetSemiring.isSetRing_supClosure, Nucleus.mem_toSublocale, AlgebraicGeometry.instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget, TopologicalSpace.IsTopologicalBasis.inf_induced, Submodule.finiteDimensional_sup, FreeAlgebra.cardinalMk_le_max, LinearMap.map_coprod_prod, Cardinal.aleph_add_aleph, AlgebraicGeometry.HasAffineProperty.affineAnd_eq_of_propertyIsLocal, AlgebraicGeometry.Etale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified, LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, Subgroup.FG.finset_sup, MeasureTheory.Measure.MeasureDense.fin_meas_approx, MeasureTheory.edist_indicatorConstLp_eq_enorm, MonoidAlgebra.cardinalMk_lift_of_infinite, Subfield.extendScalars_inf, csInf_le_of_le, AlgebraicGeometry.IsFinite.eq_proper_inf_locallyQuasiFinite, Subalgebra.LinearDisjoint.rank_sup_of_free, MeasureTheory.AddContent.supClosure_apply_finpartition, Ordinal.iSup_sum, Ideal.mul_left_self_sup, StarSubalgebra.mul_mem_sup, MeasureTheory.hittingBtwn_bot_le_iff, Subgroup.normalizer_le_normalizer_sup_of_normalizer_le_right, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app, WType.cardinalMk_le_max_aleph0_of_finite', MeasureTheory.IsSetSemiring.mem_supClosure_iff, CategoryTheory.ObjectProperty.IsLocal.inf, ConditionallyCompleteLinearOrderedField.toIsOrderedCancelAddMonoid, DirectedOn.sSup_inf_eq, Algebra.TensorProduct.map_ker, AddSubgroup.addConj_mem_sup_of_mem_inf_normalizer_of_mem_inf, Submodule.map_sup, MeasurableSpace.map_inf, Dynamics.coverEntropy_union, continuousInv_inf, Ideal.iInf_sup_eq_top, NonUnitalAlgebra.mul_mem_sup, Setoid.IsPartition.finpartition_parts, iSupIndep.supIndep', Filter.bliminf_or_le_inf, Ideal.isPrimary_finset_inf, FirstOrder.Language.card_functions_sum_skolem₁_le, PSet.rank_insert, iSupIndep.supIndep, Subalgebra.op_inf, AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom, LinearMap.comap_leq_ker_subToSupQuotient, ProbabilityTheory.condExpKernel_ae_eq_condExp', Submodule.map_mkQ_eq_top, IntermediateField.isCyclotomicExtension_lcm_sup, Submodule.eq_top_of_disjoint, IntermediateField.sup_toSubalgebra_of_isAlgebraic, SimpleGraph.chromaticNumber_sum, Module.End.invtSubmodule.isCompl_iff, AddSubmonoid.neg_sup, MeasureTheory.measure_symmDiff_le, Filter.bliminf_or_eq_inf, MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite, Filter.limsup_sup_filter, continuous_inf_dom_right, AffineSubspace.map_inf_eq, AddMonoidAlgebra.cardinalMk_of_infinite', Submonoid.smul_sup, CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup, MeasureTheory.dense_of_generateFrom_isSetSemiring, AffineSubspace.span_union, Cardinal.mul_eq_max, LinearMap.quotientInfEquivSupQuotient_apply_mk, Sublocale.coe_inf, AffineSubspace.coe_inf, Cardinal.mk_freeMonoid, Cardinal.mk_bounded_set_le, rel_sup_mul, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, OrderEmbedding.infIrredUpperSet_apply, AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux, MeasureTheory.measure_neg_vadd_symmDiff, RootPairing.invtRootSubmodule.le_ker_coroot', Algebra.map_inf, IsRetrocompact.finsetInf', Ideal.sup_pow_eq_top', IntermediateField.fg_sup, Submonoid.FG.finset_sup, MeasurableSpace.cardinal_generateMeasurableRec_le, complementedLattice_of_sSup_atoms_eq_top, IntermediateField.inf_relfinrank_right, Algebra.sup_toSubsemiring, LowerSet.supIrred_iff_of_finite, AddSubgroup.coe_add_of_left_le_normalizer_right, PrimitiveSpectrum.gc_closureOperator, beattySeq_symmDiff_beattySeq'_pos, Irrational.beattySeq_symmDiff_beattySeq_pos, Affine.Simplex.mongePlane_def, Subalgebra.mem_starClosure, Submodule.IsMinimalPrimaryDecomposition.inf_eq, ConvexCone.mem_inf, Subalgebra.finrank_right_dvd_finrank_sup_of_free, NumberField.Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, WType.cardinalMk_le_max_aleph0_of_finite, AlgebraicGeometry.Proj.basicOpen_mul, Subalgebra.mul_toSubmodule, IntermediateField.extendScalars_inf, Filter.liminf_sup_filter, Ideal.mul_sup, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, Polynomial.sup_aeval_range_eq_top_of_isCoprime, TopologicalSpace.Opens.functor_obj_map_obj, Finset.sup'_eq_csSup_image, AddSubgroup.index_map, CompleteSublattice.sInfClosed', Cardinal.mk_list_eq_max, IsSemisimpleModule.sup, exists_compositionSeries_of_isNoetherian_isArtinian, ContinuousOn.image_uIcc_eq_Icc, Finsupp.supported_union, EReal.min_neg_neg, Subgroup.relIndex_map_map, Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime, TopologicalSpace.Closeds.lipschitz_sup, Cardinal.mk_freeAddGroup, UpperSet.infIrred_Ici, pullbackTopology_def, Submodule.mul_sup, RootPairing.invtRootSubmodule.top_mem, intermediate_value_uIcc, IsDedekindDomain.inf_pow_eq_prod_of_prime, LinearMap.sup_range_inl_inr, cbiInf_eq_of_not_forall, Cardinal.mk_finsupp_nat, LinearMap.span_singleton_sup_ker_eq_top, Nucleus.coe_toSublocale, Nat.iInf_le_succ, Seminorm.closedBall_finset_sup, Topology.IsGeneratedBy.sup, Filter.blimsup_sup_not, TopologicalSpace.Opens.coe_finset_sup, MeasureTheory.IsSetSemiring.diff_mem_supClosure, MeasureTheory.OuterMeasure.le_add_caratheodory, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt, Topology.IsLocallyConstructible.finsetInf, TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.hom_ext_iff, Ideal.sup_mul_right_self, Submodule.comap_finsetInf, Submodule.comap_sup_map_of_injective, IntermediateField.lift_inf, Subalgebra.mulMap'_surjective, partialSups_eq_sUnion_image, AddSubgroup.closure_add_le, TopCat.Sheaf.interUnionPullbackConeLift_right, Submodule.coe_finsetInf, Subgroup.relIndex_sup_right, MeasurableSpace.comap_prodMk, MeasureTheory.le_measure_symmDiff, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin_1, TopologicalSpace.Closeds.coe_finset_inf, Module.End.invtSubmodule.one, IntermediateField.coe_inf, MeasurableSet.bihimp, CategoryTheory.ObjectProperty.instIsStableUnderShiftByMin, IntermediateField.restrictScalars_adjoin_eq_sup, Nucleus.toSublocale_le_toSublocale, AlgebraicGeometry.Scheme.basicOpen_add_le, csSup_empty, IsPGroup.to_sup_of_normal_left', MeasureTheory.measure_symmDiff_inv_smul, Algebra.mem_sup_left, LinearMap.quotientInfEquivSupQuotient_injective, isSemisimpleModule_iff, IntermediateField.mem_inf, IntermediateField.cardinalMk_adjoin_le, Submodule.dualAnnihilator_sup_eq, Submonoid.inv_sup, instIsModularLatticeSubgroup, AlgebraicGeometry.diagonal_isAffine_iff_forall_isAffineOpen_inf, MeasureTheory.OuterMeasure.sup_apply, Sublattice.setLike_mem_inf, Subgroup.toSubmonoid_zpowers, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse, Subalgebra.finrank_left_dvd_finrank_sup_of_free, Cardinal.mk_freeAddMonoid, NumberField.Units.regOfFamily_div_regulator, ProbabilityTheory.Kernel.IsProper.restrict_eq_indicator_smul', AddSubmonoid.mul_sup, CategoryTheory.MorphismProperty.HasCardinalLT.sup, Submodule.dualCoannihilator_sup_eq, QuotientAddGroup.comap_map_mk', OrderIso.supIrredLowerSet_apply, Cardinal.mul_le_max_of_aleph0_le_left, Cardinal.powerlt_min, iSupIndep_comp_coe_iff_supIndep, Cardinal.power_nat_le_max, iSupIndep_iff_supIndep_of_injOn, AffineIndependent.inf_affineSpan_eq_affineSpan_inter, Submodule.sup_span_singleton_eq_top_iff, Subalgebra.mul_toSubmodule_le, AffineSubspace.direction_sup, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv, AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated, Algebra.IsAlgebraic.lift_cardinalMk_le_max, SSet.skeleton_succ, Sublattice.ext_mem_iff, TopologicalSpace.IsTopologicalBasis.inf, TopologicalSpace.Opens.coe_finset_inf, AddSubgroup.coe_add_of_right_le_normalizer_left, complementedLattice_of_isAtomistic, RootPairing.corootSpan_mem_invtSubmodule_coreflection, FirstOrder.Language.ClosedUnder.inf, FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup, R1Space.inf, NumberField.IsCMField.closure_realFundSystem_sup_torsion, RootPairing.invtRootSubmodule.eq_bot_iff, Module.Basis.flag_succ, IntermediateField.LinearDisjoint.finrank_sup, MonoidAlgebra.cardinalMk_of_infinite', LinearGrowth.linearGrowthSup_sup, Sublattice.mem_subtype, AlgebraicGeometry.Scheme.grothendieckTopology_eq_inf, MeasureTheory.Measure.inf_apply, Module.End.isFinitelySemisimple_iff, Subgroup.FG.sup, ENNReal.iSup_ennreal, IntermediateField.restrictScalars_inf, partialSups_eq_biSup, dist_mulIndicator, Submodule.fg_finset_sup, Algebra.TensorProduct.productMap_range, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sup, LinearGrowth.linearGrowthInf_inf, Relation.cutExpand_le_invImage_lex, HahnSeries.cardSupp_div_le, NonUnitalAlgebra.map_sup, AddSubgroup.ofAddUnits_inf, InfiniteGalois.restrict_fixedField, Ideal.mul_sup_eq_of_coprime_left, Ideal.Filtration.sup_N, OpenAddSubgroup.toOpens_inf, isFoelner_iff, TopCat.Presheaf.IsSheaf.isSheafPreservesLimitPairwiseIntersections, EReal.coe_toENNReal_eq_max, Submodule.sup_smul, Ordinal.max_eq_zero, Subgroup.ofUnits_inf, Module.End.restrict_eigenspace, NumberField.Units.closure_fundSystem_sup_torsion_eq_top, Filter.sup_limsup, MeasureTheory.StronglyMeasurable.integral_condExpKernel', IsFoelner.tendsto_meas_smul_symmDiff_smul, FirstOrder.Language.Substructure.closure_insert, Cardinal.mk_freeRing, Ideal.mem_span_singleton_sup, LieSubmodule.sup_toSubmodule, Ideal.finset_inf_span_singleton, KaehlerDifferential.kerTotal_map, Module.End.invtSubmodule.sup_mem, ProbabilityTheory.condExp_ae_eq_integral_condExpKernel', Cardinal.add_eq_max', IsRetrocompact.finsetSup, Ordinal.card_opow_le_of_omega0_le_right, AddMonoidAlgebra.cardinalMk_eq_max_lift_of_infinite', Algebra.inf_toSubmodule, IntermediateField.sup_def, ciSup_or', CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂MinOfIsClosedUnderIsomorphisms, IsPGroup.to_sup_of_normal_right, MeasurableSpace.CountablyGenerated.sup, VonNeumannAlgebra.IsIdempotentElem.mem_iff, TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk, Cardinal.mul_mk_eq_max, MeasureTheory.IsStoppingTime.measurableSpace_min, LSeries.abscissaOfAbsConv_binop_le, MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero, IntermediateField.finrank_sup_le, Set.Iic.coe_iInf, nhds_inf, Ideal.map_sup_comap_of_surjective, Cardinal.aleph_max, LSeries.abscissaOfAbsConv_add_le, ciSup_of_empty, Module.End.invtSubmodule.mk_eq_top_iff, ContinuousOn.image_uIcc, OreLocalization.cardinalMk_le_max, OrderEmbedding.supIrredLowerSet_surjective, separableClosure_inf_perfectClosure, Subgroup.normal_mul, Subalgebra.unop_inf, biUnion_Iic_disjointed, ExpGrowth.expGrowthInf_inf, Ordinal.card_opow_omega0, Cardinal.add_eq_max, le_csSup_iff, AlgebraicGeometry.HasRingHomProperty.inf, TopologicalSpace.Compacts.coe_finset_sup, NonUnitalStarAlgebra.mul_mem_sup, Ideal.map_sup, MeasureTheory.hitting_bot_le_iff, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_of_inj, FirstOrder.Language.Substructure.CG.sup, AffineSubspace.nonempty_sup_left, LinearMap.range_coprod, Subalgebra.finrank_sup_eq_finrank_left_mul_finrank_of_free, NumberField.Units.regOfFamily_div_regOfFamily, Cardinal.preAleph_max, Set.Iic.coe_biInf, Subalgebra.finrank_sup_le_of_free, Ideal.comap_map_quotientMk, MeasureTheory.IsSetRing.partialSups_mem, Subalgebra.starClosure_toSubalgebra, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom, Module.End.invtSubmodule.inf_mem, Submodule.comap_map_mkQ, OpenAddSubgroup.toAddSubgroup_sup, Directed.iSup_inf_eq, isPreconnected_uIcc, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, iSup_fin_three, ProbabilityTheory.condExpKernel_def, nndist_mulIndicator, MeasureTheory.eLpNorm_indicator_sub_indicator, NonUnitalStarAlgebra.mem_sup_left, Module.End.invtSubmodule.map_subtype_mem_of_mem_invtSubmodule, ciSup_partialSups_eq, le_analyticOrderAt_sub, le_analyticOrderAt_add, ProjectiveSpectrum.basicOpen_mul, AlexandrovDiscrete.sup, ExpGrowth.le_expGrowthInf_add, Submodule.inf_orthogonal, IntermediateField.relfinrank_inf_mul_relfinrank, LSeries.abscissaOfAbsConv_convolution_le, VonNeumannAlgebra.IsStarProjection.mem_iff, Polynomial.cardinalMk_eq_max, TopologicalSpace.Closeds.coe_inf, Language.IsRegular.inf, IntermediateField.LinearDisjoint.inf_eq_bot, AlgebraicGeometry.isOpenImmersion_eq_inf, ClosedSubmodule.mem_sup, Submodule.IsMinimalPrimaryDecomposition.minimal, AlgebraicGeometry.Scheme.Hom.preimage_sup, MeasurableSet.symmDiff, Nat.iInf_lt_succ, Subalgebra.finite_sup, Submodule.isPrimary_decomposition_pairwise_ne_radical, IsAlgClosed.cardinal_le_max_transcendence_basis', Ideal.comap_map_of_surjective, AddSubmonoid.coe_sup, TopCat.Sheaf.interUnionPullbackConeLift_left, Ideal.quotientInfEquivQuotientProd_snd, AddSubgroup.sup_normal, AlgebraicGeometry.IsClosedImmersion.eq_inf, AddSubgroup.FG.finset_sup, continuousSMul_inf, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_assoc, IntermediateField.map_comap_eq, Submodule.restrictScalars_sup, iSupIndep.sup_indep_univ, isGLB_csInf, IsDedekindDomain.inf_prime_pow_eq_prod, NonUnitalStarSubalgebra.prod_inf_prod, DiffeologicalSpace.generateFrom_union, MeasureTheory.IsStoppingTime.measurableSpace_min_const, TopologicalSpace.Closeds.coe_sup, csSup_insert, CategoryTheory.MorphismProperty.pretopology_inf, Subalgebra.rank_sup_eq_rank_right_mul_rank_of_free, AlgebraicGeometry.Scheme.IdealSheafData.mul_inf, AlgebraicGeometry.targetAffineLocally_affineAnd_eq_affineLocally, Finset.isPWO_sup, Submodule.topologicalClosure_mem_invtSubmodule, Finset.partiallyWellOrderedOn_sup, exists_sSupIndep_disjoint_sSup_atoms, FirstOrder.Language.Term.card_sigma, CategoryTheory.Precoverage.sup_mem_coverings, LinearMap.eqOn_sup, Subgroup.normalizer_le_normalizer_sup_of_normalizer_le_left, csInf_le_iff, Submodule.add_mem_sup, Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection, Algebra.TensorProduct.map_range, Cardinal.mk_bounded_subset_le, AlgebraicGeometry.Scheme.basicOpen_appLE, MeasurableSpace.inf_le_invariants_comp, DeltaGeneratedSpace.sup, Submodule.sup_dualAnnihilator_le_inf, RegularSpace.inf, OrderIso.infIrredUpperSet_apply, CategoryTheory.Precoverage.IsStableUnderSup.sup_mem_coverings, Submonoid.closure_mul_le, AlgebraicGeometry.HasAffineProperty.descendsAlong_of_affineAnd, IntermediateField.sup_toSubalgebra_of_left, Submodule.supIndep_torsionBy, Ideal.pow_sup_eq_top', SSet.Subcomplex.BicartSq.isPushout, Units.topology_eq_inf, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app, isGLB_csInf, Projectivization.Subspace.sup_span, le_csSup_of_le, LinearMap.IsIdempotentElem.range_mem_invtSubmodule, Submodule.smul_sup, ClosedSubmodule.coe_inf, Cardinal.add_mk_eq_max, PrimitiveSpectrum.closedsGC_closureOperator, Module.AEval.mem_mapSubmodule_symm_apply, AlgebraicGeometry.isPreimmersion_eq_inf, EReal.max_neg_neg, LinearPMap.domain_sup, DFA.acceptsFrom_inter, IntermediateField.LinearDisjoint.rank_sup, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_left_of_inj, AlgebraicGeometry.IsOpenImmersion.ΓIso_inv, TopologicalSpace.Closeds.coe_finset_sup, MeasureTheory.measure_inv_smul_symmDiff, HomogeneousIdeal.toIdeal_sup, IntermediateField.rank_sup_le_of_isAlgebraic, Ideal.sup_mul_eq_of_coprime_right, AlgebraicGeometry.isProper_eq, Sublocale.inf_mem, Subalgebra.FG.sup, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom, instIsModularLatticeAddSubgroup, Ideal.pow_sup_pow_eq_top', Submodule.isQuotientEquivQuotientPrime_iff, inf_sSup_eq_iSup_inf_sup_finset, AffineSubspace.map_inf_le, Subalgebra.LinearDisjoint.finrank_sup_of_free, ZFSet.rank_insert, Subgroup.smul_sup, FirstOrder.Language.Substructure.closure_union, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt, Submodule.span_union, IsRetrocompact.finsetSup', Submonoid.coe_sup, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom, AddSubmonoid.closure_add_le, AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact, SaturatedAddSubmonoid.sup_def, AffineSubspace.finiteDimensional_sup, StarSubalgebra.map_sup, CategoryTheory.GrothendieckTopology.intersection_covering, AlgebraicGeometry.HasRingHomProperty.descendsAlong, Submodule.rank_add_le_rank_add_rank, Submodule.sup_mul, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom, Module.End.mem_invtSubmodule_symm_iff_le_map, DualNumber.range_inlAlgHom_sup_adjoin_eps, Submodule.spanRank_sup_le_sum_spanRank, Cardinal.mk_freeGroup, FirstOrder.Language.Substructure.FG.sup, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, Module.End.invtSubmodule.isCompl_mk_iff, IntermediateField.relfinrank_mul_relfinrank_eq_inf_relfinrank, Ideal.decomposition_erase_inf, OpenSubgroup.toOpens_inf, TopologicalSpace.Opens.functor_map_eq_inf, Ordinal.card_opow_eq_of_omega0_le_right, PrimitiveSpectrum.isOpen_iff, Ideal.sup_iInf_eq_top, AlgebraicGeometry.universallyClosed_eq_universallySpecializing, MeasurableSpace.cardinal_measurableSet_le, RootPairing.root_mem_submodule_iff_of_add_mem_invtSubmodule, Subgroup.relIndex_sup_left, MeasurableSpace.cardinal_generateMeasurable_le, IsAlgClosed.cardinal_le_max_transcendence_basis, CategoryTheory.Pretopology.mem_inf, completelyRegularSpace_inf, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, Polynomial.sup_ker_aeval_le_ker_aeval_mul, AlgebraicGeometry.RingedSpace.basicOpen_mul, Module.End.span_orbit_mem_invtSubmodule, AlgebraicGeometry.Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact, MeasureTheory.Filtration.coeFn_sup, AffineSubspace.nonempty_sup_right, IntermediateField.relfinrank_inf_mul_relfinrank_of_le, Ideal.ofList_append, AlgebraicGeometry.IsProper.eq_valuativeCriterion, Module.End.invtSubmodule.codisjoint_iff, Filter.inf_liminf, Topology.IsUpper.toContinuousInf, AlgebraicGeometry.IsClosedImmersion.eq_isFinite_inf_mono, AlgebraicGeometry.Scheme.basicOpen_mul, Algebra.EssFiniteType.aux, Subgroup.closure_mul_le, Subgroup.normalizer_inf_normalizer_le_normalizer_sup, AddSubmonoid.sup_eq_closure_add, MeasurableSpace.comap_sup, Submodule.sup_orthogonal_of_hasOrthogonalProjection, ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff, IntermediateField.relrank_inf_mul_relrank_of_le, Measurable.sup_of_left, partialSups_eq_ciSup_Iic, MeasureTheory.MeasuredSets.dist_def, Subalgebra.rank_sup_le_of_free, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom, AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, Representation.invtSubmodule.top_mem, ConditionallyCompleteLinearOrder.le_total, limsup_max, Algebra.isIntegral_sup, QuotientGroup.comap_map_mk', disjointed_eq_inf_compl, Cardinal.aleph_mul_aleph, dist_indicator, LinearMap.comap_eq_sup_ker_of_disjoint, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_of_inj, liminf_finset_inf', Sublocale.toNucleus_le_toNucleus, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, Subalgebra.op_sup, ContinuousLinearMap.IsIdempotentElem.commute_iff, SSet.Subcomplex.preimage_max, Submodule.finite_finset_sup, Set.partialSups_eq_accumulate, IsPGroup.to_sup_of_normal_right', TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff, SaturatedSubmonoid.sup_def, Submodule.finrank_add_le_finrank_add_finrank, Ordinal.card_opow_le_of_omega0_le_left, Ideal.mem_quotient_iff_mem_sup, Subalgebra.LinearDisjoint.val_mulMap_tmul, AlgebraicGeometry.isomorphisms_eq_isOpenImmersion_inf_surjective, AlgebraicGeometry.IsAffineOpen.inf, Subgroup.sup_normal, Subalgebra.mulMap_range, Submodule.lt_sup_iff_notMem, PrimitiveSpectrum.kernel_hull, Set.Mapsto.mem_invtSubmodule, CategoryTheory.ObjectProperty.instIsStableUnderShiftMin, ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule, Module.End.mem_invtSubmodule_iff_forall_mem_of_mem, Subfield.extendScalars_sup, FirstOrder.Language.Term.card_le, Submodule.sup_torsionBySet_ideal_eq_torsionBySet_inf, cauchy_davenport_minOrder_add, Ideal.IsMaximal.coprime_of_ne, Ideal.add_eq_sup, RootPairing.coe_bot, Module.End.invtSubmodule.top_mem, AlgebraicGeometry.Scheme.Hom.preimage_inf, Ordinal.card_opow_eq_of_omega0_le_left, PrimitiveSpectrum.isClosed_iff, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_right_of_inj, NonUnitalAlgebra.inf_toSubmodule, nucleusIsoSublocale.eq_toSublocale, IntermediateField.isSeparable_sup, StarSubalgebra.coe_inf, Submonoid.FG.sup, MeasureTheory.upperCrossingTime_zero', Submodule.IsLattice.sup, Submodule.complementedLattice, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup, AffineSubspace.sup_direction_le, CompleteSublattice.mk'_carrier, continuousVAdd_inf, AlgebraicGeometry.geometrically_inf, Submodule.map₂_sup_left, Submodule.sup_eq_top_iff, LinearMap.ker_sup_ker_le_ker_comp_of_commute, coinduced_sup, LinearMap.range_ofIsCompl, Subalgebra.centralizer_coe_sup, csInf_union, MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff, Cardinal.add_mk_eq_max', DirectedOn.inf_sSup_eq, CategoryTheory.PreZeroHypercover.presieve₀_sum, MvPolynomial.cardinalMk_le_max_lift, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom, Subalgebra.coe_starClosure, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_apply, MeasureTheory.measure_symmDiff_eq, Ideal.ofList_cons_smul, Ideal.sup_mul_eq_of_coprime_left, DiffeologicalSpace.isPlot_inf_iff, Sylow.normalizer_sup_eq_top, Finset.sup'_id_eq_csSup, AlgebraicGeometry.IsFinite.eq_isProper_inf_isAffineHom, Subring.smul_sup, Module.End.eigenspace_mem_invtSubmodule, max_aleph0_card_le_rank_fun_nat, FreeAlgebra.cardinalMk_le_max_lift, NonUnitalStarAlgebra.coe_inf, IntermediateField.lift_cardinalMk_adjoin_le, AddSubgroup.normalizer_le_normalizer_sup_normal, MeasureTheory.SignedMeasure.of_symmDiff_compl_positive_negative, LinearMap.coe_quotientInfToSupQuotient, Subfield.closure_union, RootPairing.isIrreducible_iff_invtRootSubmodule, NonUnitalStarAlgebra.map_sup, AffineSubspace.direction_inf_of_mem_inf, Directed.inf_iSup_eq, nucleusIsoSublocale.symm_eq_toNucleus, csSup_inter_le, AffineSubspace.map_sup, Submodule.map_sup_comap_of_surjective, UpperSet.infIrred_iff_of_finite, ProbabilityTheory.condExpKernel_eq, le_csInf_inter, Set.mabs_mulIndicator_symmDiff, Module.End.mem_invtSubmodule_adjoint_iff, Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, LSeries.abscissaOfAbsConv_sub_le, AlgebraicGeometry.Scheme.basicOpen_res, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, Nucleus.restrict_toSublocale, AddSubgroup.ofAddUnits_sup_addUnits, RootPairing.rootSpan_mem_invtSubmodule_reflection, Subalgebra.map_comap_eq, Submodule.span_sup, Cardinal.powerlt_aleph0_le, Ideal.quotientInfEquivQuotientProd_fst, EMetric.Closeds.lipschitz_sup, MonoidAlgebra.cardinalMk_lift_of_infinite', MeasureTheory.AddContent.supClosure_apply_of_mem, Algebra.mem_sup_right, TopologicalSpace.Opens.coe_sup, Projectivization.Subspace.span_union, IntermediateField.rank_sup_le, AddSubgroup.toAddSubmonoid_zmultiples, LieAlgebra.IsKilling.lieIdealOrderIso_right_inv, Filter.bliminf_not_inf, MeasureTheory.ae_eq_set_symmDiff, MeasureTheory.measure_symmDiff_neg_vadd, generateFrom_union_isOpen, LinearMap.coprod_map_prod, CompleteSublattice.comap_carrier, Cardinal.add_eq_left_iff, RootPairing.coe_top, ConditionallyCompleteLinearOrderBot.csSup_empty, Seminorm.closedBall_finset_sup', LinearMap.rank_comp_le, Finset.inf'_id_eq_csInf, TopologicalSpace.Closeds.uniformContinuous_sup, Cardinal.mk_finsupp_of_infinite, isArtinian_sup, Subsemiring.smul_sup, Algebra.coe_inf, nndist_indicator, limsup_finset_sup, AddSubmonoid.saturation_sup, Module.End.isSemisimple_iff', Subgroup.coe_mul_of_right_le_normalizer_left, Filter.limsup_piecewise, MeasureTheory.OuterMeasure.isCaratheodory_partialSups, SSet.stdSimplex.face_inter_face, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMin, AddSubgroup.normalizer_le_normalizer_sup_of_normalizer_le_left, Cardinal.mul_eq_max_of_aleph0_le_left, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_left_of_inj, DiffeologicalSpace.toPlots_inf, IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_inf, IsAddFoelner.tendsto_meas_vadd_symmDiff, Finset.wellFoundedOn_sup, UniformSpace.toTopologicalSpace_inf, complementedLattice_iff_isAtomistic, TensorProduct.map_ker, CompleteLatticeHom.toOrderIsoRangeOfInjective_apply, Ideal.eq_inf_of_isPrime_inf, TopologicalSpace.Opens.infLELeft_apply, Sublocale.infClosed, IntermediateField.adjoin_union, IntermediateField.inf_toSubfield, IsCompactlyGenerated.BooleanGenerators.finitelyAtomistic, Ordinal.omega_max, AddMonoidAlgebra.cardinalMk_eq_max_lift_of_infinite, AddSubgroup.normalizer_inf_normalizer_le_normalizer_sup, AlgebraicGeometry.IsLocalAtTarget.descendsAlong_inf_quasiCompact, Polynomial.cardinalMk_le_max, Submodule.sup_toAddSubmonoid, StarSubalgebra.mem_sup_right, Submodule.mem_finsetInf, ciSup_false, AffineSubspace.mem_inf_iff, ConditionallyCompleteLinearOrderedField.toIsStrictOrderedRing, BooleanSubalgebra.map_sup, Finset.inf'_eq_csInf_image, LinearMap.map_eq_top_iff, liminf_finset_inf, PrimitiveSpectrum.hull_sSup, isNoetherian_sup, Submodule.mem_sup, NonUnitalStarAlgebra.map_inf, IntermediateField.lift_sup, CategoryTheory.MorphismProperty.precoverage_inf, Algebra.cardinalMk_adjoin_le, Filter.blimsup_sup_le_or, Ideal.multiset_prod_le_inf, Algebra.mul_mem_sup, AlgebraicGeometry.Scheme.IdealSheafData.inf_mul, Ideal.le_comap_sup, Nat.iSup_lt_succ, MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring, le_csSup, CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup, NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex, Opens.toPretopology_grothendieckTopology, Filter.blimsup_not_sup, Submodule.instIsModularLattice, StarSubalgebra.mem_inf, Ideal.ofList_cons, LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff, CategoryTheory.ObjectProperty.instIsTriangulatedMinOfIsClosedUnderIsomorphisms, Sublattice.le_comap_sup, Ideal.isPrimary_decomposition_pairwise_ne_radical, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin, AddSubgroup.sup_eq_closure_add, Submodule.exists_mem_sup, Subalgebra.val_mulMap'_tmul, MeasureTheory.SimpleFunc.iSup_approx_apply, IntermediateField.sup_toSubalgebra_of_right, Submodule.span_insert, Ideal.comap_map_of_surjective', Cardinal.sum_pow_eq_max_aleph0, AlgHom.eqOn_sup, AlgebraicGeometry.isomorphisms_eq_stalkwise, DFA.accepts_inter, Submodule.FG.sup, iSupIndep_iff_supIndep, Set.definable_finset_inf, isLUB_csSup, IntermediateField.le_sup_toSubalgebra, LinearMap.quotientInfEquivSupQuotient_symm_apply_left, Sublocale.range_toNucleus, partialSups_eq_biUnion_range, AlgebraicGeometry.IsFinite.eq_inf, Filter.cardinalInterFilter_inf, Ideal.sup_pow_eq_top, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, ZFSet.rank_pair, BooleanSubalgebra.le_comap_sup, IsPGroup.to_sup_of_normal_left, AlgebraicGeometry.GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible, ExpGrowth.expGrowthSup_sup, Filter.blimsup_or_eq_sup, iSupIndep_iff_supIndep_univ, PrimitiveSpectrum.hull_iSup, IntermediateField.map_inf, TopologicalSpace.Opens.coe_inf, Module.End.invtSubmodule.zero, Subgroup.index_map, DiffeologicalSpace.generateFrom_union_toPlots, iSupIndep_fin_three, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃_W, Topology.IsLocallyConstructible.finsetInf', Cardinal.mul_eq_max', Ideal.fst_comp_quotientInfEquivQuotientProd, IntermediateField.sup_toSubfield, Module.End.invtSubmodule.id, IntermediateField.relfinrank_comap_comap_eq_relfinrank_inf, Ideal.span_union, AddSubmonoid.addSubmonoid_smul_sup, LinearEquiv.map_mem_invtSubmodule_iff, IntermediateField.sup_toSubalgebra_of_isAlgebraic_right, continuous_sup_rng_left, CompleteSublattice.map_carrier, IntermediateField.inf_relfinrank_left, Ideal.IsHomogeneous.sup, continuous_inf_rng, Ordinal.max_zero_right, IntermediateField.map_sup, AlgebraicGeometry.IsAffineOpen.sup_of_disjoint, IsTranscendenceBasis.lift_cardinalMk_eq_max_lift, IsTranscendenceBasis.lift_rank_eq_max_lift, Submodule.rank_sup_add_rank_inf_eq, csSup_le_csSup, MvRatFunc.rank_eq_max_lift, Seminorm.ball_finset_sup, cauchy_davenport_minOrder_mul, IntermediateField.inf_relrank_left, Submodule.finite_sup, Representation.invtSubmodule.coe_bot, MvPolynomial.cardinalMk_le_max, Representation.invtSubmodule.instNontrivialSubtypeSubmoduleMemSublattice, Submodule.mem_sup_left, Cardinal.mk_freeCommRing, Cardinal.mk_freeAbelianGroup, csInf_le, limsup_finset_sup', AlgebraicGeometry.isPullback_opens_inf_le, MeasurableSet.exists_isOpen_symmDiff_lt, IntermediateField.relrank_inf_mul_relrank, Ideal.radical_finset_inf, Algebra.mem_inf, MeasureTheory.Filtration.coeFn_inf, MeasureTheory.MeasurePreserving.measure_symmDiff_preimage_iterate_le, Submodule.mem_sup_right, PointedCone.ofSubmodule_sup, Submodule.sup_set_smul, AddSubmonoid.FG.finset_sup, MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite', LinearMap.IsIdempotentElem.ker_mem_invtSubmodule, MeasureTheory.IsSetRing.finsetSup_mem, Submodule.sup_span, NonUnitalSubalgebra.starClosure_toNonUnitalSubalgebra, MeasureTheory.IsSetSemiring.exists_finpartition_diff, LinearPMap.supSpanSingleton_apply_mk, HahnSeries.cardSupp_hsum_powers_le, AlgebraicGeometry.Scheme.IdealSheafData.support_sup, Ideal.mem_sup_right, Sublocale.toNucleus_apply, Ideal.sup_mul, Set.abs_indicator_symmDiff, EuclideanGeometry.orthogonalProjection_sup_of_orthogonalProjection_eq, Module.End.invtSubmodule.mk_eq_bot_iff, Cardinal.add_le_max, Algebra.sup_def, Ideal.snd_comp_quotientInfEquivQuotientProd, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_right_of_inj, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor, LieSubalgebra.lie_mem_sup_of_mem_normalizer, Nat.iSup_le_succ', ConditionallyCompleteLinearOrderedField.toMulPosStrictMono, Module.End.invtSubmodule.comp, LieSubalgebra.add_eq_sup, Submodule.map_add_le, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄_W, TopCat.Sheaf.interUnionPullbackCone_pt, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso, Filter.liminf_piecewise, Submodule.covBy_span_singleton_sup, AddSubgroup.normalizer_le_normalizer_sup_of_normalizer_le_right, Ordinal.card_opow_le, MeasureTheory.MeasuredSets.edist_def, ClosedSubmodule.coe_sup, RootPairing.invtSubmodule_reflection_of_invtSubmodule_coreflection, Sublattice.setLike_mem_coe, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt, Ideal.sup_mul_left_self, MeasureTheory.measure_symmDiff_eq_zero_iff, Subgroup.IsComplement'.sup_eq_top, Cardinal.mk_finsupp_lift_of_infinite', Submodule.wcovBy_span_singleton_sup, AlgebraicGeometry.IsIntegralHom.eq_universallyClosed_inf_isAffineHom, Finset.sup'_univ_eq_ciSup, Module.End.invtSubmodule.bot_mem, AddSubgroup.FG.sup, ContinuousLinearMap.orthogonal_mem_invtSubmodule, IntermediateField.relrank_mul_relrank_eq_inf_relrank, IsRetrocompact.finsetInf, Submodule.decomposition_erase_inf, csInf_le_csInf, Module.End.mem_invtSubmodule_iff_map_le, Module.End.invtSubmodule.codisjoint_mk_iff, NonUnitalAlgebra.adjoin_union, ContinuousLinearMap.range_coprod, generateFrom_inter, Ideal.mul_right_self_sup, MeasureTheory.AddContent.supClosure_apply, Submodule.prod_sup_prod, AlgebraicGeometry.Scheme.pretopology_eq_inf, Subgroup.conj_mem_sup_of_mem_inf_normalizer_of_mem_inf, MeasurableSpace.measurableSet_inf, Submodule.sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson, AddSubmonoid.FG.sup, LinearMap.quotientInfEquivSupQuotient_symm_apply_right, Module.AEval.mem_mapSubmodule_apply, Seminorm.ball_finset_sup', Cardinal.mul_le_max, exists_uIoo_isExtrOn_uIcc, CategoryTheory.ObjectProperty.shift_sup, LowerSet.supIrred_Iic, MeasurableSpace.measurableSet_sup, Sublattice.setLike_mem_sup, AddOreLocalization.cardinalMk_le_max, HahnSeries.cardSupp_inv_le, Filter.sup_liminf, Submodule.add_eq_sup, csSup_le, PolynormableSpace.inf, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W, Subspace.dualAnnihilator_inf_eq, TrivSqZeroExt.range_inlAlgHom_sup_adjoin_range_inr, Representation.mem_invtSubmodule, KaehlerDifferential.kerTotal_map', IntermediateField.normal_sup, Algebra.inf_toSubsemiring, ENNReal.image_coe_uIcc, edist_indicator, AddMonoidAlgebra.cardinalMk_of_infinite, AddSubgroup.relIndex_sup_right, Submodule.sup_toAddSubgroup, CategoryTheory.PreZeroHypercover.presieve₀_add, NonUnitalAlgebra.inf_toNonUnitalSubsemiring, Ordinal.lsub_sum, Submodule.mem_invtSubmodule_reflection_iff, CategoryTheory.MorphismProperty.IsLocalAtTarget.inf, MeasureTheory.OuterMeasure.map_sup, MeasureTheory.NullMeasurableSet.symmDiff, liminf_min, isAddFoelner_iff, PrimitiveSpectrum.gc, LinearMap.quotientInfEquivSupQuotient_surjective, csInf_pair, IsCyclotomicExtension.lcm_sup, SequentialSpace.sup, isLUB_csSup, AffineSubspace.sup_direction_lt_of_nonempty_of_inter_empty, Ideal.span_insert, FreeAlgebra.cardinalMk_eq_max, Submodule.map₂_sup_right, ZFSet.rank_union, CompleteSublattice.subtype_apply, Module.End.invtSubmodule.disjoint_iff, Module.End.isSemisimple_iff, AddUnits.topology_eq_inf, csSup_union, IntermediateField.finiteDimensional_sup, Submodule.isOrtho_sup_left, ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, Submodule.isPrimary_finsetInf, Ordinal.preOmega_max, ContinuousLinearMap.mem_invtSubmodule_adjoint_iff, NonUnitalSubalgebra.mem_starClosure, IntermediateField.fixingSubgroup_sup, AlgebraicGeometry.ValuativeCriterion.eq, MeasureTheory.dist_indicatorConstLp_eq_norm, Cardinal.add_eq_right_iff, OpenSubgroup.toSubgroup_sup, Subgroup.ofUnits_sup_units, LieSubmodule.instIsModularLattice, Finite.ciInf_inf, DiffeologicalSpace.generateFrom_inter_toPlots, Cardinal.mk_finsupp_of_infinite', MvPolynomial.cardinalMk_eq_max_lift, continuous_inf_dom_left, NonUnitalAlgebra.map_inf, Submodule.comap_sup_of_injective, LinearMap.range_add_le, FirstOrder.Language.Substructure.lift_card_closure_le, Sublattice.map_sup, IntermediateField.isPurelyInseparable_sup, NonUnitalStarAlgebra.mem_inf, Submodule.small_sup, PSet.rank_pair, analyticOrderAt_add_of_ne, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.sup_W, FreeAlgebra.cardinalMk_eq_max_lift, AlgebraicGeometry.descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact, LinearMap.prod_eq_sup_map, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.sup_P, Nat.iSup_le_succ, Affine.Simplex.altitude_def, TrivSqZeroExt.range_liftAux, SSet.skeletonOfMono_succ, LinearMap.lift_rank_comp_le, LinearMap.surjective_domRestrict_iff, AffineSubspace.comap_inf, MvPolynomial.cardinalMk_eq_max, Representation.invtSubmodule.bot_mem, edist_mulIndicator, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, Algebra.Subalgebra.restrictScalars_adjoin, AlgebraicGeometry.descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact, Algebraic.cardinalMk_lift_le_max, FirstOrder.Language.BoundedFormula.card_le, NonUnitalStarAlgebra.inf_toNonUnitalSubalgebra, LinearMap.IsSymmetric.orthogonalComplement_mem_invtSubmodule, ProbabilityTheory.condExpKernel_apply_eq_condDistrib, Algebra.rank_adjoin_le, Submonoid.saturation_sup, LinearMap.ker_comp_eq_of_commute_of_disjoint_ker, TopologicalSpace.Opens.mk_inf_mk, IsDedekindDomain.HeightOneSpectrum.inf_pow_eq_prod, LinearMap.BilinForm.span_singleton_sup_orthogonal_eq_top, rel_sup_add, setOf_isOpen_sup, Submodule.comap_map_eq
toSupSet 📖	CompOp	16 math math: ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove, Int.csSup_eq_greatestOfBdd, le_csSup_iff, le_csSup_of_le, Int.csSup_of_not_bddAbove, Int.csSup_eq_greatest_of_bdd, IsLUB.csSup_eq, Int.csSup_mem, ConditionallyCompleteLinearOrderBot.csSup_empty, le_csSup, isLUB_csSup, Int.csSup_of_not_bdd_above, csSup_le_csSup, csSup_le, isLUB_csSup, Int.csSup_empty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGLB_csInf 📖	mathematical	Set.Nonempty BddBelow Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup toLattice	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup toLattice InfSet.sInf toInfSet	—	—
isLUB_csSup 📖	mathematical	Set.Nonempty BddAbove Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup toLattice	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup toLattice SupSet.sSup toSupSet	—	—

ConditionallyCompleteLinearOrder

Definitions

Name	Category	Theorems
toConditionallyCompleteLattice 📖	CompOp	1553 math math: Ordinal.iSup_eq_iSup, LinearGrowth.linearGrowthSup_zero, IsClosed.sSup_mem, LinearGrowth.linearGrowthSup_top, Ordinal.iSup_eq_bsup, ENat.sub_iInf, tendsto_zero_iff_meromorphicOrderAt_pos, ProbabilityTheory.bayesRisk_of_subsingleton, Measurable.limsup, Filter.Tendsto.limsup_eq, ENNReal.iInf_div_of_ne, Order.IsNormal.apply_of_isSuccLimit, IsClosed.Icc_subset_of_forall_mem_nhdsWithin, Ordinal.lift_card_iSup_le_sum_card, liminf_const_sub, Acc.rank_eq, Cardinal.mk_sUnion_le, Ordinal.iSup_pow_natCast, Ordinal.cof_iSup_add_one_le, ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_symm, Module.rank_def, SummationFilter.summable_symmetricIco_of_summable_symmetricIcc, Filter.HasBasis.liminf_eq_ite, MeasureTheory.lintegral_def, Continuous.strictMono_of_inj_boundedOrder', Algebra.lift_cardinalMk_adjoin_le, List.iSup_mem_map_of_exists_sSup_empty_le, Ordinal.sup_eq_lsub_iff_lt_sup, SymmetricAlgebra.rank_eq, isSaddlePointOn_value, Ordinal.cof_iSup_le_lift, Set.Finite.einfsep, MeasureTheory.iInf_mul_le_lintegral, Cardinal.powerlt_max, Measurable.biSup, EMetric.hausdorffEdist_iUnion_le, ENNReal.add_sInf, ENat.sSup_eq_top_of_infinite, EisensteinSeries.hasSum_e2Summand_symmetricIcc, iSup_eq_of_tendsto, dimH_sUnion, csInf_of_not_bddBelow, Ordinal.sInf_compl_lt_lift_ord_succ, MeasureTheory.hittingBtwn_apply_mono_right, IsMinOn.iInf_eq, lowerSemicontinuous_ciSup, Set.einfsep_of_fintype, MeasureTheory.hittingBtwn_mono_left, RootPairing.Base.not_nonneg_iff_neg_of_sum_mem_range_root, Antitone.map_limsup_of_continuousAt, tendsto_atBot_of_antitone, lowerSemicontinuousOn_biSup, Pi.Lex.sSup_apply_le, MeasureTheory.lintegral_iSup', ENNReal.le_liminf_mul, Cardinal.lift_iSup_le_lift_iSup, Monotone.leftLim_eq_sSup, MeasureTheory.le_hitting_of_exists, Filter.eventually_lt_of_lt_liminf, Ordinal.max_zero_left, Cardinal.mk_list_eq_max_mk_aleph0, LinearGrowth.linearGrowthInf_add_le', ConditionallyCompleteLinearOrderedField.inducedMap_mono, ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm, Cardinal.mk_list_le_max, EReal.liminf_add_top_of_ne_bot, ContinuousOn.le_sSup_image_Icc, LinearGrowth.le_linearGrowthSup_add, csSup_le', CategoryTheory.ObjectProperty.HasCardinalLT.sup, NNReal.iSup_of_not_bddAbove, Ordinal.sup_eq_lsub_iff_succ, FormalMultilinearSeries.radius_pi_eq_iInf, ENNReal.ofNNReal_limsup, SummationFilter.tsum_symmetricIcc_eq_tsum_symmetricIco, AntitoneOn.map_sSup_of_continuousWithinAt, Padic.withValUniformEquiv_norm_le_one_iff, tendsto_cobounded_iff_meromorphicOrderAt_neg, Rat.padicValuation_cast, lowerSemicontinuousWithinAt_iSup, Set.Finite.lt_csInf_iff, NNReal.mul_iSup_le, ENat.iInf_mul_of_ne, Cardinal.mk_multiset_of_nonempty, ENat.smul_sSup, ModuleCat.injectiveDimension_eq_iSup_localizedModule_prime, Ordinal.cof_iSup_Iio, MeasureTheory.setLIntegral_le_iSup_mul, Ordinal.iSup_typein_succ, LinearGrowth.linearGrowthSup_add_le, MeasureTheory.hittingAfter_bot_le_iff, MeasureTheory.hittingBtwn_mem_set_of_hittingBtwn_lt, Metric.exists_isLocalMin_mem_ball, upperSemicontinuousAt_biInf, Metric.hausdorffEDist_def, csInf_mem, banach_steinhaus_iSup_nnnorm, AntitoneOn.tendsto_nhdsGT, toCompactIccSpace, isPreconnected_iff_ordConnected, CategoryTheory.ObjectProperty.instHasInducedTStructureMinOfIsClosedUnderIsomorphisms, MeasureTheory.isTightMeasureSet_iff_inner_tendsto, ciSup_partialSups_eq', Cardinal.iSup_of_empty, MeasureTheory.hittingBtwn_univ, ENNReal.limsup_const_mul_of_ne_top, sSup_Iio_eq_self_iff_isSuccPrelimit, IsOpen.measure_eq_iSup_isClosed, Cardinal.iSup_lt_of_isRegular, ContinuousLinearMap.nnnorm_def, Metric.hausdorffEDist_iUnion_le, ENat.iSup_add_iSup_of_monotone, ENNReal.iSup_pow_of_ne_zero, ENat.iSup_zero, Monotone.map_liminf_of_continuousAt, Nat.tendsto_iSup_of_tendsto_limsup, Monotone.leftLim, Padic.instCompatibleWithZeroMultiplicativeIntMulValuation, MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top, MeasureTheory.le_hitting, isPreconnected_Ici, Real.limsup_of_not_isBoundedUnder, Cardinal.mul_le_max_of_aleph0_le_right, NNReal.coe_sSup, MeasureTheory.lintegral_iSup_ae, MeasureTheory.IsStoppingTime.iInf, isLeast_csInf, Antitone.le_leftLim, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective, Int.padicValuation_lt_one_iff, SummationFilter.HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc, MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt, Filter.cardinalInterFilter_sup, Cardinal.sum_pow_le_max_aleph0, Ordinal.sup_succ_le_lsub, ContinuousOn.image_Icc_of_antitoneOn, MonoidAlgebra.cardinalMk_of_infinite, exists_eq_iInf_of_not_isPredPrelimit, LowerSemicontinuousOn.le_liminf, Ordinal.iSup_le_lsub, Ordinal.card_iSup_Iio_le_sum_card, MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top, ENat.iInf_toNat, IsClosed.upperClosure, le_limsup_add, meas_essSup_lt, NNReal.limsInf_of_not_isCobounded, Finset.ciSup_eq_max'_image, Cardinal.iSup_lt_of_lt_cof_ord, Cardinal.mul_eq_max_of_aleph0_le_right, ENNReal.ofReal_iInf, MeasureTheory.OuterMeasure.coe_iSup, Cardinal.sum_le_mk_mul_iSup, Int.csInf_mem, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone, ENat.iInf_add_iInf, MeasureTheory.hittingBtwn_mem_Icc, cbiSup_eq_of_not_forall, NNReal.segment_eq_uIcc, MeasureTheory.lintegral_iSup_directed, ENat.iInf_sum, ProbabilityTheory.bayesRisk_of_subsingleton', isConnected_Ioc, Ideal.sup_primeHeight_eq_ringKrullDim, RootPairing.coe_chainBotCoeff_eq_sSup, ENNReal.iSup_add_iSup_le, setOf_liouvilleWith_subset_aux, Pi.Colex.le_sSup_apply, Set.Nonempty.eq_Icc_iff_int, LinearGrowth.le_linearGrowthSup_add', ENNReal.limsup_mul_le, Directed.measure_iUnion, Cardinal.mk_finsupp_lift_of_infinite, MeasureTheory.lowerCrossingTime_le, Submodule.spanRank_toENat_eq_iInf_encard, ExpGrowth.expGrowthSup_add, ConditionallyCompleteLinearOrderedField.toZeroLEOneClass, MeasureTheory.hittingAfter_mono, ENat.exists_eq_iSup_of_lt_top, IsCompact.sSup_mem, exists_lt_of_ciInf_lt, LinearGrowth.linearGrowthInf_bot, NNReal.coe_iSup, AEMeasurable.iInf, Order.IsNormal.le_iff_le_sSup, compare_eq_compareOfLessAndEq, Int.padicValuation_eq_one_iff, IsCompact.isLeast_sInf, MonotoneOn.tendsto_nhdsLT, MeasureTheory.Measure.mkMetric_apply, ENNReal.mul_iInf, ENNReal.limsup_const_mul, RootPairing.setOf_root_add_zsmul_mem_eq_Icc, LinearOrderedField.lt_inducedMap_iff, MeasureTheory.Measure.iInf_IicSnd_gt, Subfield.cardinalMk_closure_le_max, MeasureTheory.biSup_measure_Iic, Cardinal.mul_eq_left_iff, MeasureTheory.hitting_le_of_mem, ENNReal.toNNReal_sSup, Monotone.rightLim_le_leftLim, Ordinal.iSup_lt_of_lt_cof, MeasureTheory.lintegral_iInf_ae, Ordinal.sSup_add_one_lt_of_lt_cof, ENNReal.inv_sSup, csInf_lt_iff, MeasureTheory.lintegral_iInf', Int.csInf_eq_least_of_bdd, Cardinal.lift_iInf, ENNReal.limsup_liminf_le_liminf_limsup, exists_mem_uIcc_isFixedPt, limsInf_eq_of_le_nhds, MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum, spectrum.spectralRadius_le_liminf_pow_nnnorm_pow_one_div, CategoryTheory.ObjectProperty.shiftClosure_eq_iSup, lt_csSup_iff, exists_mem_Icc_isFixedPt, LinearGrowth.linearGrowthSup_bot, ContinuousLinearMap.sSup_sphere_eq_nnnorm, MeasureTheory.SimpleFunc.iSup_coe_eapprox, LinearOrderedField.inducedOrderRingIso_self, Filter.exists_lt_of_limsup_le, Rat.padicValuation_self, WithTop.coe_sSup, ENNReal.liminf_toReal_eq, MeasurableSet.measure_eq_iSup_isCompact_of_ne_top, Algebraic.cardinalMk_le_max, IsCompact.sSup_lt_iff_of_continuous, Antitone.map_limsSup_of_continuousAt, lowerSemicontinuousOn_iSup, lowerSemicontinuous_iff_le_liminf, LinearGrowth.linearGrowthInf_biInf, Order.IsSuccLimit.iSup_Iio, tendsto_atBot_of_monotone, upperSemicontinuous_biInf, ConditionallyCompleteLinearOrderedField.toPosMulStrictMono, ENat.mul_iSup, ENat.sSup_eq_zero, RootPairing.Base.pos_or_neg_of_sum_smul_root_mem, IsClosed.sInf_mem, ae_lt_of_lt_essInf, csSup_eq_top_of_top_mem, MeasureTheory.Measure.LebesgueDecomposition.iSup_succ_eq_sup, NNReal.iSup_eq_zero, Matroid.cRank_eq_iSup_cardinalMk_indep, exists_isLocalExtr_Ioo, Ordinal.card_sInf_range_compl_le_lift, MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE, Ordinal.iSup_le, Pi.Colex.sSup_apply, ENNReal.le_iInf₂_add_iInf₂, NNReal.natCast_iInf, Algebra.IsAlgebraic.cardinalMk_le_max, hasCardinalLT_subtype_max, ExpGrowth.expGrowthSup_def, intermediate_value_Icc', Cardinal.sum_eq_lift_iSup_of_lift_mk_le_lift_iSup, MeasureTheory.limsup_lintegral_le, intermediate_value_Ioo', MeasureTheory.OuterMeasure.iInf_apply', Ordinal.iSup_succ, Ordinal.Principal.sSup, Set.Finset.coe_einfsep, egauge_univ_pi, Eventually.le_linearGrowthInf, MeasureTheory.hittingBtwn_mem_set, Set.Finite.ciInf_mem_image, Ordinal.lift_cof_iSup_add_one, ProbabilityTheory.bayesRisk_eq_iInf_measure_of_subsingleton, ValuativeRel.nonempty_orderIso_withZeroMul_int_iff, ENNReal.iInf_div, MeasureTheory.stoppedValue_hitting_mem, ExpGrowth.expGrowthSup_biSup, Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_strictMono, MeasureTheory.eLpNormEssSup_eq_iSup, exists_isExtrOn_Ioo_of_tendsto, Finite.map_iInf_of_monotone, MeasureTheory.exists_isSigmaFiniteSet_measure_ge, Filter.HasBasis.limsup_eq_ite, ENat.biSup_add', Finset.sup_univ_eq_ciSup, ENat.sum_iSup, MeasureTheory.Measure.mkMetric_le_liminf_tsum, csSup_le_csSup', ENNReal.biSup_add, MeasureTheory.measure_sigmaFiniteSetGE_le, ENat.iInf_mul', ENNReal.sSup_div, ENNReal.essSup_add_le, csInf_of_not_bddBelow, Real.liminf_of_not_isBoundedUnder, Measurable.iSup, Pi.Lex.sInf_apply, Ordinal.card_omega0_opow, Ordinal.iSup_pow, EMetric.diam_insert, Cardinal.lift_iSup, Padic.norm_eq_zpow_log_mulValuation, AntitoneOn.tendsto_nhdsWithin_Ioo_right, Ordinal.deriv_limit, isConnected_Iio, ENNReal.iInf_sum, ENNReal.coe_sSup, liminf_eq_top, NNReal.image_coe_uIcc, EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero, MeasureTheory.hittingBtwn_mono, MeasureTheory.isStoppingTime_of_measurableSet_lt_of_isRightContinuous, iUnion_Iic_eq_Iio_of_lt_of_tendsto, MeasureTheory.stoppedValue_hittingBtwn_mem, Pi.Lex.sInf_apply_le, Dynamics.coverEntropyEntourage_union, MonotoneOn.map_csInf_of_continuousWithinAt, Ordinal.card_sInf_range_compl_le, LinearGrowth.linearGrowthInf_top, MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le, Ordinal.iSup_add_one_lt_of_lt_cof, ENNReal.biSup_add_biSup_le, csSup_of_not_bddAbove, le_ciSup_iff', MeasureTheory.hitting_le_iff_of_exists, csSup_le_iff', Real.limsSup_of_not_isCobounded, meromorphicOrderAt_add, Monotone.rightLim_eq_sInf, EisensteinSeries.G2_eq_tsum_symmetricIco, Ordinal.sSup_eq_bsup, ciInf_of_not_bddBelow, EReal.limsup_neg, ContinuousOn.strictMonoOn_of_injOn_Icc', Cardinal.lift_sSup, MeasureTheory.upperCrossingTime_mono, Monotone.tendsto_nhdsLT, FreeAlgebra.cardinalMk_le_max, Int.csSup_eq_greatestOfBdd, Cardinal.aleph_add_aleph, isPreconnected_Iic, Ordinal.iSup_add_nat, Filter.liminf_le_iff', ENNReal.essSup_const_mul, MeasureTheory.hittingBtwn_apply_anti, Cardinal.mk_biUnion_le_lift, ENNReal.iSup_coe_lt_top, IsCompact.isLUB_sSup, LinearGrowth.linearGrowthInf_const_mul_self, Order.krullDim_le_of_krullDim_preimage_le, LeftOrdContinuous.continuousWithinAt_Iic, MeasureTheory.lintegral_le_iSup_mul, MonoidAlgebra.cardinalMk_lift_of_infinite, RootPairing.setOf_root_sub_zsmul_mem_eq_Icc, Cardinal.lift_iSup_le, Int.cofinite_eq, Set.Nonempty.ordConnected_iff_of_bdd', LowerSemicontinuousWithinAt.le_liminf, Ordinal.iSup_sum, MeasureTheory.hittingAfter_mem_set, MeasureTheory.hittingBtwn_bot_le_iff, ConditionallyCompleteLinearOrderedField.coe_inducedOrderRingIso, MeasureTheory.Adapted.isStoppingTime_hittingBtwn, ENNReal.ofReal_limsup_toReal, ENat.iInf_coe_lt_top, ProbabilityTheory.avgRisk_le_iSup_risk, WType.cardinalMk_le_max_aleph0_of_finite', Set.Finite.csSup_lt_iff, ENNReal.iSup_natCast, IsConnected.Ioo_csInf_csSup_subset, CategoryTheory.ObjectProperty.IsLocal.inf, exists_eq_ciInf_of_finite, ConditionallyCompleteLinearOrderedField.toIsOrderedCancelAddMonoid, MeasureTheory.hitting_mem_Icc, ENat.iInf_mul, Topology.IsUpper.isTopologicalSpace_basis, ENNReal.ofReal_limsup, Monotone.map_csSup_of_continuousAt, tendsto_intCast_atBot_sup_atTop_cobounded, ENat.add_iInf, limsup_const_add, sInf_eq_argmin_on, PseudoMetricSpace.dist_ofPreNNDist, SummationFilter.multipliable_symmetricIco_of_multipliable_symmetricIcc, Dynamics.coverEntropy_union, limsup_eq_bot, MvPowerSeries.le_order_subst, MeasureTheory.essSup_trim, Ordinal.lift_cof_iSup, ENat.add_iSup, ciInf_le', NNReal.iSup_mul_iSup_le, FirstOrder.Language.card_functions_sum_skolem₁_le, MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ, ENNReal.iInf_add_iInf, AEMeasurable.biInf, PSet.rank_insert, MeasureTheory.OuterMeasure.trim_eq_iInf', MeasureTheory.isStoppingTime_of_measurableSet_lt_of_isRightContinuous', Antitone.map_ciInf_of_continuousAt, MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure, SimpleGraph.chromaticNumber_eq_iInf, Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub, ENat.mul_sSup, LinearGrowth.linearGrowthInf_zero, SimpleGraph.chromaticNumber_sum, SummationFilter.hasSum_symmetricIoc_int_iff, Antitone.tendsto_nhdsGT, upperSemicontinuousOn_iInf, MeasurableSet.measure_eq_iSup_isCompact, ciInf_eq_univ_of_not_bddBelow, Ordinal.sup_succ_eq_lsub, MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite, IsCompact.sInf_mem, LowerSemicontinuousAt.le_liminf, isConnected_Ici, AnalyticAt.meromorphicOrderAt_nonneg, Ordinal.sSup_ord, ContinuousOn.sInf_image_Icc_le, MeasureTheory.le_hittingBtwn, Int.ball_eq_Ioo, AddMonoidAlgebra.cardinalMk_of_infinite', essSup_eq_sInf, Eventually.linearGrowthSup_le, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, MeasureTheory.Content.outerMeasure_eq_iInf, liminf_add_le, Cardinal.mul_eq_max, ENNReal.liminf_sub_const, MeasureTheory.hitting_eq_end_iff, EisensteinSeries.tendsto_e2Summand_atTop_nhds_zero, isConnected_Icc, Cardinal.mk_freeMonoid, Cardinal.mk_bounded_set_le, Ordinal.enumOrd_zero, ciInf_mem, ENNReal.smul_iSup, Order.krullDim_eq_iSup_coheight_of_nonempty, ENNReal.iSup_add, LinearGrowth.linearGrowthSup_le_of_eventually_le, ENat.coe_sSup, ENNReal.iInf_mul_of_ne, SummationFilter.hasSum_symmetricIcc_iff, MeasureTheory.measure_biUnion_eq_iSup, RootPairing.coe_chainTopCoeff_eq_sSup, MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge, Ordinal.iSup_mul_nat, MeasureTheory.hittingBtwn_le_of_mem, MonotoneOn.tendsto_nhdsGT, Filter.le_limsup_iff, ENNReal.tsum_iSup_eq, ENat.sInf_eq_zero, MeasurableSpace.cardinal_generateMeasurableRec_le, Order.krullDim_eq_iSup_length, Padic.mulValuation_toFun, Int.csInf_eq_leastOfBdd, Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim, Monotone.map_csInf, Finset.Nonempty.ciSup_mem_image, egauge_pi, WithTop.iInf_coe_eq_top, essSup_comp_quotientAddGroup_mk, ContinuousOn.strictMonoOn_of_injOn_Ioo, ENNReal.add_iInf, liminf_add_const, Set.Nonempty.ciSup_lt_iff, csInf_le', exists_isLocalExtr_Ioo_of_tendsto, NNReal.agm_eq_ciSup, RootPairing.setOf_root_add_zsmul_eq_Icc_of_linearIndependent, ENNReal.toNNReal_iSup, Padic.comap_mulValuation_eq_padicValuation, Antitone.measure_iUnion, MeasureTheory.lintegral_liminf_le, WType.cardinalMk_le_max_aleph0_of_finite, ae_le_essSup, upperSemicontinuousWithinAt_iff_limsup_le, ENNReal.tsum_eq_iSup_nat', Metric.ediam_eq_sSup, ENNReal.inv_iSup, isConnected_Ioo, Int.csInf_of_not_bddBelow, MeasureTheory.OuterMeasure.iInf_apply, UpperSemicontinuousWithinAt.limsup_le, Finite.map_iInf_of_monotoneOn, csSup_mem_of_not_isSuccPrelimit', tendsto_nhds_iff_meromorphicOrderAt_nonneg, MeasureTheory.isStoppingTime_hittingBtwn_isStoppingTime, Cardinal.mk_list_eq_max, ENat.sInf_add, lowerClosure_eq_Iic_csSup, isPreconnected_Icc, ContinuousOn.image_uIcc_eq_Icc, IsMaxOn.iSup_eq, EReal.min_neg_neg, MeasureTheory.limsup_measure_compl_le_of_le_liminf_measure, upperSemicontinuousOn_iff_limsup_le, LinearGrowth.linearGrowthSup_biSup, liminf_sub_const, Cardinal.mk_freeAddGroup, iInf_eq_of_tendsto, Ordinal.sup_le_lsub, ConditionallyCompleteLinearOrderedField.inducedOrderRingHom_toFun, upperSemicontinuous_ciInf, Cardinal.sum_eq_iSup_of_mk_le_iSup, ENNReal.liminf_mul_le, EReal.le_liminf_add, Ordinal.iSup_add_natCast, FormalMultilinearSeries.radius_inv_eq_limsup, EisensteinSeries.hasSum_e2Summand_symmetricIco, Set.einfsep_insert, MeasureTheory.hitting_le, Finite.map_iSup_of_antitone, ENat.add_sSup, ENNReal.tsum_eq_iSup_sum, Ordinal.IsNormal.map_iSup, intermediate_value_uIcc, NNReal.sSup_of_not_bddAbove, IsPreconnected.Iio_csSup_subset, ciSup_le_iff', Padic.AddValuation.map_add, Order.coheight_eq_iSup_head_eq, Ordinal.card_iSup_Iio_le_card_mul_iSup, ContinuousOn.image_Icc, cbiInf_eq_of_not_forall, Cardinal.mk_finsupp_nat, MeasureTheory.le_liminf_measure_open_of_forall_tendsto_measure, LinearGrowth.linearGrowthSup_inv, LinearGrowth.linearGrowthInf_const, LinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap, MeasureTheory.OuterMeasure.biInf_apply, ENNReal.essSup_piecewise, ENNReal.iInf_add, ProbabilityTheory.bayesRisk_const_of_nonempty, ENat.coe_iSup, ENat.smul_iSup, Finset.Nonempty.csSup_mem, Filter.exists_lt_of_le_liminf, AntitoneOn.map_csSup_of_continuousWithinAt, ENNReal.mul_iInf', EReal.liminf_add_le, MeasureTheory.hittingAfter_eq_top_iff, MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le, LinearGrowth.linearGrowthSup_le_iff, Cardinal.mul_ciSup, Filter.limsup_le_iff, Measurable.limsup', exists_seq_tendsto_sSup, IsCompact.lt_sInf_iff_of_continuous, Monotone.map_ciSup_of_continuousAt, meromorphicNFAt_iff_analyticAt_or, NNReal.iSup_pow_of_ne_zero, Order.krullDim_eq_iSup_height_of_nonempty, ExpGrowth.le_expGrowthInf_comp, ENNReal.liminf_const_sub, EMetric.infEdist_biUnion, Filter.eventually_lt_of_limsup_lt, MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral, ENNReal.iInf_add_iInf_of_monotone, MeasureTheory.tendsto_measure_norm_gt_of_isTightMeasureSet, Multiset.iSup_mem_map_of_exists_sSup_empty_le, Ordinal.sup_eq_bsup, LinearGrowth.linearGrowthSup_const_mul_self, Cardinal.ciSup_mul, intermediate_value_Ioo, MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto, Antitone.map_csInf_of_continuousAt, setOf_isPreconnected_eq_of_ordered, ciSup_le', Set.einfsep_insert_le, MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict, Ordinal.Principal.iSup, ENat.sub_iSup, ENat.iInf_eq_top_of_isEmpty, MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm, exists_eq_ciInf_of_not_isPredPrelimit, Set.Nonempty.csSup_mem, Cardinal.ord_eq_Inf, CategoryTheory.ObjectProperty.instIsStableUnderShiftByMin, ENNReal.biSup_add', MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto, le_ciInf_iff', csSup_empty, ENat.iInf_coe_eq_top, Ordinal.cof_iSup, WithTop.iSup_coe_lt_top, ENNReal.iSup_add_iSup, lowerSemicontinuous_iSup, IntermediateField.cardinalMk_adjoin_le, csInf_mem_of_not_isPredPrelimit, untrop_sum, ENNReal.coe_essSup, Cardinal.mk_freeAddMonoid, ENNReal.iSup_sub, ENNReal.tsum_eq_iSup_sum', limsSup_eq_of_le_nhds, MonotoneOn.map_sInf_of_continuousWithinAt, MeasureTheory.hittingBtwn_apply_mono_left, HasSum.hasSum_symmetricIco_of_hasSum_symmetricIcc, isPreconnected_Ioi, MeasureTheory.hittingBtwn_anti, MvPowerSeries.le_weightedOrder_subst, Cardinal.mul_le_max_of_aleph0_le_left, Cardinal.powerlt_min, Cardinal.power_nat_le_max, MeasureTheory.measure_sigmaFiniteSetWRT', le_limsup_mul, MonotoneOn.map_csSup_of_continuousWithinAt, ENat.exists_eq_iInf, Monotone.map_iInf_of_continuousAt, IsCompact.measure_eq_iInf_isOpen, ENNReal.sub_eq_sInf, Ordinal.opow_limit, Finset.Nonempty.csInf_eq_min', exists_Ioo_extr_on_Icc, MeasureTheory.OuterMeasure.ofFunction_eq_iInf_mem, Algebra.IsAlgebraic.lift_cardinalMk_le_max, Finite.map_iSup_of_monotoneOn, Cardinal.preAleph_limit, LinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self, Real.limsup_of_not_isCoboundedUnder, Antitone.map_csSup_of_continuousAt, csSup_of_not_bddAbove, Order.height_eq_iSup_lt_height, dimH_eq_iInf, ENNReal.le_iInf_mul, le_csSup_iff', ContinuousOn.strictMonoOn_of_injOn_Icc, MeasureTheory.isTightMeasureSet_range_iff_tendsto_limsup_inner, SummationFilter.multipliable_symmetricIco_of_multiplible_symmetricIcc, Filter.le_limsup_iff', Real.liminf_of_not_isCoboundedUnder, NormedSpace.equicontinuous_TFAE, MonoidAlgebra.cardinalMk_of_infinite', isTotallyDisconnected_iff_lt, LinearGrowth.linearGrowthSup_sup, IsOpen.measure_eq_iSup_isCompact, PiLp.nnnorm_eq_ciSup, Cardinal.lift_iSup_le_sum, MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd, MeasureTheory.limsup_trim, Monotone.measure_iInter, MeasureTheory.Measure.inf_apply, MeasureTheory.hittingAfter_apply_anti, ENNReal.essSup_liminf_le, Ordinal.cof_iSup_Iio_add_one, Pi.Colex.sSup_apply_le, Cardinal.ord_eq_iInf, Antitone.rightLim_le_leftLim, isPreconnected_Ico, UpperSemicontinuousOn.limsup_le, ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iff, MeasureTheory.integral_le_liminf_integral_of_forall_isOpen_measure_le_liminf_measure, LinearGrowth.linearGrowthInf_inf, Relation.cutExpand_le_invImage_lex, HahnSeries.cardSupp_div_le, upperSemicontinuous_iInf, RootPairing.Base.not_nonpos_iff_pos_of_sum_mem_range_root, WithTop.iInf_coe_lt_top, ENat.coe_iInf, dimH_bUnion, ciInf_eq_top_of_top_mem, isConnected_Ico, EReal.coe_toENNReal_eq_max, Cardinal.sum_le_lift_mk_mul_iSup, ConditionallyCompleteLinearOrderedField.to_archimedean, ENNReal.inv_iInf, Ordinal.max_eq_zero, Finset.ciInf_mem_image, Ordinal.bsup_eq_sup, ENat.mul_iInf_of_ne, eq_Icc_of_connected_compact, EMetric.infEdist_iUnion, Cardinal.mk_freeRing, tendsto_of_antitone, Multiset.iSup_mem_map_of_ne_zero, sInf_mem_closure, Ordinal.lift_iSup_add_one_lt_of_lt_cof, exists_eq_ciSup_of_not_isSuccPrelimit, ENNReal.toNNReal_iInf, Int.padicValuation_self, Cardinal.add_eq_max', MeasureTheory.eLpNormEssSup_eq_essSup_enorm, MeasureTheory.inducedOuterMeasure_eq_iInf, MeasureTheory.lintegral_iInf, MeasureTheory.le_iInf_lintegral, csInf_eq_bot_of_bot_mem, Ordinal.card_opow_le_of_omega0_le_right, NNReal.le_iInf_mul_iInf, ENNReal.le_iInf_mul_iInf, AddMonoidAlgebra.cardinalMk_eq_max_lift_of_infinite', LinearGrowth.linearGrowthSup_eventually_monotone, ciSup_or', Continuous.strictMonoOn_of_inj_rigidity, Ordinal.IsPrincipal.iSup, trdeg_eq_iSup_cardinalMk_isTranscendenceBasis, CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂MinOfIsClosedUnderIsomorphisms, IsClosed.Icc_subset_of_forall_exists_lt, lowerSemicontinuousWithinAt_ciSup, Cardinal.mul_mk_eq_max, Ordinal.iSup_mul_natCast, LowerSemicontinuous.le_liminf, Ordinal.mem_closure_iff_iSup, Antitone.map_liminf_of_continuousAt, Cardinal.sInf_eq_zero_iff, sInf_iUnion_Ici, ciSup_eq_univ_of_not_bddAbove, LinearGrowth.linearGrowthSup_const, Ordinal.sSup_le_sSup_add_one, NNReal.iSup_div, LSeries.abscissaOfAbsConv_binop_le, MeasureTheory.measure_iUnion_of_tendsto_zero, ENat.iSup_natCast, MeasureTheory.Lp.eLpNorm'_lim_eq_lintegral_liminf, Ordinal.iSup_lt_ord_lift, Cardinal.aleph_max, LSeries.abscissaOfAbsConv_add_le, Pi.Colex.sInf_apply_le, ciSup_of_empty, Filter.limsup_le_iff', CategoryTheory.ObjectProperty.HasCardinalLT.iSup, ProbabilityTheory.bayesRisk_le_iInf, ContinuousOn.image_uIcc, AntitoneOn.exists_antitone_extension, PiLp.edist_eq_iSup, OreLocalization.cardinalMk_le_max, ENat.iInf_add_iInf_of_monotone, Manifold.riemannianEDist_def, Finset.Nonempty.csSup_eq_max', LinearGrowth.linearGrowthInf_natCast_nonneg, ENNReal.tsum_eq_limsup_sum_nat, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone', IsOpen.measure_eq_biSup_integral_continuous, ExpGrowth.expGrowthInf_inf, Ordinal.card_opow_omega0, Ordinal.cof_eq_sInf_lsub, Cardinal.add_eq_max, Filter.le_liminf_iff', Pi.Lex.le_sInf_apply, eventually_liminf_le, MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup, UpperSemicontinuousAt.limsup_le, AntitoneOn.map_sInf_of_continuousWithinAt, EReal.le_limsup_mul, sInf_mem_of_not_isPredPrelimit, LinearOrderedField.inducedMap_mono, MeasureTheory.hitting_bot_le_iff, setOf_isPreconnected_subset_of_ordered, ENNReal.toReal_limsup, EReal.limsup_mul_le, Finset.ciInf_eq_min'_image, LinearGrowth.linearGrowthSup_comp_nonneg, spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius, Cardinal.preAleph_max, Order.krullDim_eq_iSup_coheight, ENNReal.add_iSup, OrderIso.map_ciSup', ENNReal.iSup_coe_eq_top, MonotoneOn.map_csInf, isPreconnected_Ioc, Monotone.rightLim_le, SimpleGraph.edist_eq_sInf, upperSemicontinuousAt_iff_limsup_le, MonotoneOn.tendsto_nhdsWithin_Ioo_right, Antitone.map_sSup_of_continuousAt, isPreconnected_uIcc, ENNReal.ofNNReal_liminf, intermediate_value_Ioc', EReal.le_liminf_mul, ENat.iSup_mul, Ordinal.mem_closure_tfae, Cardinal.iSup_lt_ord_lift_of_isRegular, isPreconnected_Ioo, MonotoneOn.tendsto_nhdsWithin_Ioo_left, SummationFilter.hasProd_symmetricIco_int_iff, MeasureTheory.hittingBtwn_mono_right, BoundedContinuousFunction.nndist_eq_iSup, eventually_le_limsup, SummationFilter.hasSum_symmetricIco_int_iff, le_analyticOrderAt_sub, le_analyticOrderAt_add, MeasureTheory.OuterMeasure.sSup_apply, NNReal.natCast_iSup, ExpGrowth.le_expGrowthInf_add, Measurable.liminf', SimpleGraph.ediam_eq_iSup_iSup_edist, Cardinal.iSup_lt_lift_of_isRegular, IsClosed.Icc_subset_of_forall_exists_gt, Ordinal.iSup'_eq_bsup, LSeries.abscissaOfAbsConv_convolution_le, Measurable.sInf, iUnion_Ici_eq_Ioi_of_lt_of_tendsto, Polynomial.cardinalMk_eq_max, Order.krullDim_eq_iSup_height, ContinuousLinearMap.sSup_unit_ball_eq_nnnorm, UniformOnFun.edist_def', Monotone.linearGrowthInf_nonneg, MeasureTheory.tendsto_measure_sigmaFiniteSetGE, IsClosed.csSup_mem, Topology.IsScott.instUnivSetOfIsUpper, IsAlgClosed.cardinal_le_max_transcendence_basis', MeasureTheory.Measure.hausdorffMeasure_le_liminf_tsum, hasCardinalLT_subtype_iSup, ENat.sSup_add, Cardinal.beth_limit, Filter.Tendsto.liminf_eq, ExpGrowth.expGrowthSup_comp_le, Ordinal.lt_iSup_add_one, trop_iInf, upperSemicontinuous_iff_limsup_le, Antitone.tendsto_rightLim_within, ENNReal.biSup_add_biSup_le', Cardinal.mk_biUnion_le, MeasureTheory.lintegral_iSup_directed_of_measurable, Set.Nonempty.ordConnected_iff_of_bdd, MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part, SummationFilter.tprod_symmetricIcc_eq_tprod_symmetricIco, Submodule.spanRank_toENat_eq_iInf_finset_card, isSaddlePointOn_iff', ClassGroup.norm_lt, Ordinal.iSup_sequence_lt_omega_one, ENNReal.mul_sSup, ENNReal.iSup_add_iSup_of_monotone, FirstOrder.Language.Term.card_sigma, ENNReal.mul_iInf_of_ne, Rat.padicValuation_eq_zero_iff, Ordinal.cof_lift_iSup_add_one_le, le_csInf_iff', exists_lt_of_lt_csSup, IsCompact.isGLB_sInf, MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE', Finset.untrop_sum, ENNReal.ofReal_essSup, ENat.coe_sInf, Cardinal.mk_bounded_subset_le, ENNReal.sSup_mul, eq_Icc_csInf_csSup_of_connected_bdd_closed, ENNReal.iSup_zero, MeasureTheory.hittingBtwn_isStoppingTime, ciInf_eq_bot_of_bot_mem, ENat.add_sInf, Set.einfsep_eq_iInf, IsWellFounded.rank_eq, Ordinal.iSup_typein_limit, ENat.iSup_eq_zero, essSup_comp_quotientGroup_mk, EReal.liminf_neg, Ordinal.iSup_lt_lift, Real.limsInf_of_not_isBounded, LinearGrowth.linearGrowthInf_eventually_monotone, MeasureTheory.lintegral_eq_nnreal, UniformFun.edist_def, Cardinal.mk_iUnion_le_lift, essInf_eq_sSup, WithTop.isGLB_sInf, Antitone.leftLim, ENNReal.iInf_mul_iInf, Monotone.map_limsSup_of_continuousAt, MeasureTheory.SimpleFunc.lintegral_restrict_iUnion_of_directed, ENat.biSup_add_biSup_le', NNReal.le_mul_iInf, ENNReal.limsup_eq_zero_iff, MeasureTheory.IsFundamentalDomain.essSup_measure_restrict, Cardinal.add_mk_eq_max, Antitone.tendsto_leftLim_within, ExpGrowth.expGrowthInf_iInf, isCompact_Icc, EReal.liminf_mul_le, Ordinal.derivFamily_limit, BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm, EReal.max_neg_neg, MeasureTheory.OuterMeasure.sInf_apply, MeasureTheory.iInf_le_lintegral, Int.csSup_of_not_bddAbove, AntitoneOn.map_csInf_of_continuousWithinAt, Finite.map_iInf_of_antitoneOn, ZFSet.rank_range, upperSemicontinuousOn_ciInf, MeasureTheory.hitting_eq_hitting_of_exists, iSup₂_iInf₂_le_iInf₂_iSup₂, Monotone.map_csInf_of_continuousAt, ENNReal.add_biSup', lowerSemicontinuousWithinAt_iff_le_liminf, Cardinal.succ_def, Monotone.expGrowthInf_comp_le, Int.csSup_eq_greatest_of_bdd, EisensteinSeries.tsum_tsum_symmetricIco_sub_eq, Ordinal.iSup_ord, exists_lt_of_lt_csSup', ENNReal.hasSum, ENat.iSup_add_iSup, ZFSet.rank_insert, ENat.iSup_add, Ordinal.sup_eq_sup, Monotone.map_limsInf_of_continuousAt, Ordinal.sSup_lt_of_lt_cof, Pi.Colex.le_sInf_apply, StieltjesFunction.length_eq, ENNReal.add_sSup, Ordinal.le_iSup, csInf_eq_univ_of_not_bddBelow, MeasureTheory.measure_eq_iInf', le_csInf_iff'', List.iInf_mem_map_of_exists_le_sInf_empty, ENNReal.iInf_mul', MeasureTheory.lintegral_iInf_directed_of_measurable, Ordinal.iSup_eq_zero_iff, LinearOrderedField.inducedOrderRingIso_symm, Filter.frequently_lt_of_liminf_lt, ENat.le_iInf_add_iInf, MeasureTheory.hitting_mono, Cardinal.sInf_empty, Measurable.liminf, Continuous.strictMono_of_inj, Metric.infEDist_iUnion, Order.IsNormal.map_iSup, Filter.liminf_le_limsup_of_frequently_le, Cardinal.mk_freeGroup, ENNReal.iSup_div, Finite.map_iSup_of_antitoneOn, intermediate_value_Ico', Set.Nonempty.ciSup_mem_image, LinearGrowth.linearGrowthInf_iInf, liminf_mul_le, lowerSemicontinuousAt_iff_le_liminf, UniformOnFun.edist_def, MeasureTheory.Measure.iInf_rat_gt_prod_Iic, IsClosed.isGreatest_csSup, MeasureTheory.OuterMeasure.boundedBy_apply, Ordinal.card_opow_eq_of_omega0_le_right, ENNReal.limsup_add_of_right_tendsto_zero, eVariationOn.eVariationOn_eq_strictMonoOn, ProbabilityTheory.iSup_bayesRisk_le_minimaxRisk, LinearGrowth.linearGrowthInf_monotone, Filter.frequently_lt_of_limsInf_lt, AntitoneOn.tendsto_nhdsLT, MeasurableSpace.cardinal_measurableSet_le, iSup_succ, Ordinal.sup_eq_bsup', Ordinal.succ_iSup_eq_lsub_iff, Filter.liminf_le_iff, MeasurableSpace.cardinal_generateMeasurable_le, ENat.mul_iInf, isConnected_Iic, SimpleGraph.diam_def, ENat.sSup_mul, Cardinal.sum_le_lift_mk_mul_iSup_lift, IsAlgClosed.cardinal_le_max_transcendence_basis, ENat.iSup_coe_eq_top, MeasureTheory.hittingAfter_mem_set_of_ne_top, Antitone.leftLim_le, Antitone.tendsto_nhdsLT, ProbabilityTheory.bayesRisk_le_iInf', ENat.iInf_add, ENNReal.toReal_essSup, BoundedContinuousFunction.edist_eq_iSup, RootPairing.Base.exists_root_eq_sum_int, Ordinal.sup_eq_lsub, ExpGrowth.expGrowthInf_biInf, LinearGrowth.linearGrowthSup_iSup, LinearGrowth.linearGrowthInf_comp_nonneg, ENNReal.essSup_mul_le, Ordinal.lift_card_sInf_compl_le, RootPairing.root_add_zsmul_mem_range_iff, iSup_Iio_eq_self_iff_isSuccPrelimit, Order.IsSuccLimit.sSup_Iio, Ordinal.iSup_eq_lsub_iff_lt_iSup, ENNReal.toReal_sSup, Filter.eventually_add_neg_lt_of_le_liminf, isPreconnected_Iio, ENNReal.sub_iSup, ContinuousMap.nnnorm_eq_iSup_nnnorm, Antitone.measure_iInter, IsClosed.Icc_subset_of_forall_mem_nhdsGT_of_Icc_subset, MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd, IsClosed.lowerClosure, ENNReal.liminf_add_of_right_tendsto_zero, Topology.IsScott.scott_eq_upper_of_completeLinearOrder, MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup, exists_lt_of_lt_ciSup, EisensteinSeries.tendsto_double_sum_S_act, Ordinal.IsNormal.map_iSup_of_bddAbove, SummationFilter.symmetricIcc_eq_symmetricIoo_int, Cardinal.preBeth_limit, IsCompact.continuous_sInf, ProbabilityTheory.bayesRisk_const_of_neZero, Antitone.le_rightLim, le_total, MeasureTheory.measure_eq_iInf, limsup_max, MeasureTheory.hitting_lt_iff, MeasureTheory.hittingBtwn_le, ENNReal.limsup_mul_le', MeasureTheory.le_iInf₂_lintegral, upperSemicontinuousOn_biInf, MeasureTheory.Measure.iSup_restrict_spanningSets, ContinuousMap.nndist_eq_iSup, NNReal.limsSup_of_not_isBounded, ENNReal.le_iInf_add_iInf, Monotone.tendsto_leftLim_within, Order.IsNormal.le_iff_le_sSup', MeasureTheory.lintegral_iSup, Int.closedBall_eq_Icc, Ordinal.lt_iSup_iff, Cardinal.aleph_mul_aleph, ENNReal.iInf_mul, liminf_finset_inf', Ordinal.IsNormal.map_sSup_of_bddAbove, Order.IsNormal.preimage_Iic, ENNReal.toReal_iInf, MeasureTheory.hittingAfter_isStoppingTime, Ordinal.iSup_add_one_le_iff, EisensteinSeries.summable_e2Summand_symmetricIcc, MeasureTheory.lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure, ENNReal.iSup_eq_zero, ENNReal.sInf_add, Ordinal.card_opow_le_of_omega0_le_left, Ordinal.bsup'_eq_iSup, Ordinal.IsNormal.apply_omega0, MeasurableSet.measure_eq_iSup_isClosed_of_ne_top, ENNReal.iInf_coe_lt_top, Cardinal.lift_iSup_lt_of_lt_cof_ord, ModuleCat.projectiveDimension_eq_iSup_localizedModule_maximal, CategoryTheory.ObjectProperty.instIsStableUnderShiftMin, Ordinal.iSup_add_one, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, MeasureTheory.eLpNormEssSup_count, ProbabilityTheory.bayesRisk_const, intermediate_value_Icc, Padic.comap_mulValuation_eq_int_padicValuation, Ordinal.iSup_Iio_eq_bsup, ContinuousOn.image_Icc_of_monotoneOn, WithTop.iSup_coe_eq_top, NNReal.coe_iInf, MeasureTheory.OuterMeasure.iUnion_of_tendsto_zero, limsup_add_le, Antitone.map_iSup_of_continuousAt, Ordinal.iSup_Iio_add_one, FirstOrder.Language.Term.card_le, AEMeasurable.iSup, cauchy_davenport_minOrder_add, WithTop.isLUB_sSup, ENNReal.smul_sSup, Antitone.map_iInf_of_continuousAt, MeasureTheory.hittingBtwn_le_iff_of_lt, EReal.limsup_const_mul_of_nonneg_of_ne_top, SimpleGraph.chromaticNumber_eq_biInf, Ordinal.iSup_eq_of_range_eq, MeasureTheory.hittingBtwn_eq_end_iff, Int.csSup_mem, Ordinal.card_opow_eq_of_omega0_le_left, Monotone.map_iSup_of_continuousAt, ZFSet.rank_iUnion, ciSup_of_not_bddAbove, ENNReal.sSup_add, Ordinal.IsNormal.map_sSup, LinearGrowth.le_linearGrowthInf_iff, Topology.IsScott.isOpen_iff_Iic_compl_or_univ, MeasureTheory.upperCrossingTime_zero', MeasureTheory.iSup₂_lintegral_le, Order.krullDim_eq_iSup_height_add_coheight_of_nonempty, Ordinal.iSup_sequence_lt_omega1, Filter.frequently_lt_of_lt_limsup, FiberBundle.exists_trivialization_Icc_subset, ENNReal.tsum_eq_iSup_nat, AlgebraicGeometry.geometrically_inf, Antitone.rightLim, ENNReal.iInf₂_add, Ordinal.bsup_eq_iSup, LinearOrderedField.inducedMap_nonneg, upperSemicontinuousWithinAt_biInf, SimpleGraph.ediam_def, Ordinal.lsub_le_succ_iSup, Cardinal.add_mk_eq_max', NNReal.limsup_of_not_isBoundedUnder, ENNReal.essSup_indicator_eq_essSup_restrict, Cardinal.ciSup_mul_ciSup, Cardinal.lift_sInf, AEMeasurable.biSup, MeasureTheory.OuterMeasure.top_apply', MvPolynomial.cardinalMk_le_max_lift, ExpGrowth.expGrowthInf_def, Real.limsInf_of_not_isCobounded, Measurable.iInf, LinearGrowth.linearGrowthInf_le_of_eventually_le, Finite.map_iSup_of_monotone, RightOrdContinuous.continuousWithinAt_Ici, ENNReal.tsum_eq_liminf_sum_nat, LinearGrowth.linearGrowthInf_le_iff, NNReal.iSup_empty, EReal.le_limsup_add, Monotone.le_rightLim, IsUltrametricDist.nnnorm_tprod_le, MeasureTheory.Measure.hausdorffMeasure_apply, LinearGrowth.linearGrowthSup_comp_le, Monotone.linearGrowthInf_comp_le, Cardinal.sSup_lt_of_lt_cof_ord, max_aleph0_card_le_rank_fun_nat, FreeAlgebra.cardinalMk_le_max_lift, IntermediateField.lift_cardinalMk_adjoin_le, ProbabilityTheory.bayesRisk_discard, ENNReal.iSup_pow, Ideal.sup_height_eq_ringKrullDim, Monotone.linearGrowthInf_comp_mul, isSaddlePointOn_iff, Ordinal.mem_iff_iSup_of_isClosed, NNReal.mul_iSup, EMetric.hausdorffEdist_def, MeasureTheory.le_measure_compl_liminf_of_limsup_measure_le, ENNReal.sub_iInf, ENNReal.essSup_restrict_eq_of_support_subset, LinearOrderedField.coe_inducedOrderRingIso, MeasureTheory.lowerCrossingTime_mono, Cardinal.add_ciSup, MeasureTheory.hitting_mem_set, HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc, Continuous.strictMono_of_inj_boundedOrder, MeasureTheory.hittingAfter_le_iff, ciInf_lt_iff, Set.measure_eq_iInf_isOpen, LSeries.abscissaOfAbsConv_sub_le, MeasureTheory.Measure.mkMetric_le_liminf_sum, Ordinal.sInf_compl_lt_ord_succ, MeasureTheory.lintegral_enorm_le_liminf_of_tendsto, tendsto_iSup_of_tendsto_limsup, ENNReal.iSup_lt_eq_self, MeasureTheory.OuterMeasure.sInf_apply', EReal.liminf_const_mul_of_nonpos_of_ne_bot, Continuous.strictAnti_of_inj_boundedOrder, Cardinal.powerlt_aleph0_le, BoundedContinuousFunction.nndist_eq, ENNReal.finsetSum_iSup_of_monotone, IsCompact.measure_eq_biInf_integral_hasCompactSupport, MonoidAlgebra.cardinalMk_lift_of_infinite', NNReal.liminf_of_not_isCoboundedUnder, MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf, exists_eq_ciSup_of_finite, MeasureTheory.SimpleFunc.iSup_eapprox_apply, MeasureTheory.ae_eq_set_symmDiff, Dense.ciInf', ENat.toENNReal_iSup, Ordinal.isClosed_iff_iSup, MeasureTheory.upperCrossingTime_le, MeasureTheory.isStoppingTime_hitting_isStoppingTime, Ordinal.bsup_eq_sup', Cardinal.add_eq_left_iff, LinearOrderedField.coe_lt_inducedMap_iff, Filter.frequently_lt_of_lt_limsSup, ConditionallyCompleteLinearOrderBot.csSup_empty, Ordinal.lift_iSup_lt_of_lt_cof, LinearMap.rank_comp_le, isConnected_Ioi, Cardinal.mk_finsupp_of_infinite, MeasureTheory.hittingAfter_apply_mono, NNReal.sInf_empty, le_liminf_add, IsCompact.continuous_sSup, limsup_finset_sup, dimH_iUnion, NNReal.mul_iInf, NNReal.toReal_limsup, upperSemicontinuousAt_ciInf, MeasureTheory.StronglyAdapted.isStoppingTime_leastGE, EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq, Monotone.measure_iUnion, MeasureTheory.le_hittingAfter, ciInf_le_of_le', LinearGrowth.linearGrowthInf_add_le, Cardinal.mul_eq_max_of_aleph0_le_left, limsInf_nhds, NNReal.iInf_mul, Frequently.linearGrowthInf_le, Antitone.rightLim_le, MeasureTheory.tendsto_measure_compl_closedBall_of_isTightMeasureSet, Cardinal.lift_iSup_le_lift_iSup', MeasureTheory.hitting_mem_set_of_hitting_lt, untrop_sum_eq_sInf_image, Ordinal.sup_typein_limit, Rat.HeightOneSpectrum.valuation_equiv_padicValuation, Order.IsSuccPrelimit.sSup_Iio, Antitone.map_ciSup_of_continuousAt, ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_self, Ordinal.omega_max, AddMonoidAlgebra.cardinalMk_eq_max_lift_of_infinite, sSup_mem_of_not_isSuccPrelimit, MeasureTheory.hittingBtwn_of_lt, ENat.add_iInf₂, le_liminf_mul, Polynomial.cardinalMk_le_max, List.iSup_mem_map_of_ne_nil, ENNReal.iSup_mul_le, Monotone.linearGrowthInf_comp, ENat.add_biSup, NNReal.iInf_empty, IsClosed.csInf_mem, ciSup_false, ConditionallyCompleteLinearOrderedField.toIsStrictOrderedRing, ENNReal.liminf_add_of_left_tendsto_zero, Padic.norm_rat_le_one_iff_padicValuation_le_one, liminf_finset_inf, MeasureTheory.hittingBtwn_lt_iff, tendsto_atTop_of_antitone, Antitone.leftLim_le_rightLim, MeasureTheory.OuterMeasure.sInfGen_def, EisensteinSeries.summable_e2Summand_symmetricIco, Finset.Nonempty.csInf_mem, tendsto_of_monotone, Directed.measure_iInter, RootPairing.root_sub_zsmul_mem_range_iff, Rat.surjective_padicValuation, Monotone.leftLim_le, ENat.mul_iInf', Algebra.cardinalMk_adjoin_le, EMetric.diam_eq_sSup, ENat.sum_iSup_of_monotone, NNReal.le_iInf_add_iInf, Measurable.sSup, MeasureTheory.isTightMeasureSet_iff_tendsto_measure_norm_gt, Ordinal.sup_eq_lsub_or_sup_succ_eq_lsub, MeasureTheory.hittingAfter_le_of_mem, Cardinal.iInf_eq_zero_iff, CategoryTheory.ObjectProperty.instIsTriangulatedMinOfIsClosedUnderIsomorphisms, csInf_eq_csInf_of_forall_exists_le, MeasureTheory.measure_iUnion_eq_iSup_accumulate, exists_seq_tendsto_sInf, lowerSemicontinuousAt_iSup, ae_essInf_le, Cardinal.lift_iSup_le_iff, csSup_mem_closure, csSup_eq_univ_of_not_bddAbove, Cardinal.sum_pow_eq_max_aleph0, Monotone.linearGrowthSup_nonneg, ENNReal.hasProd_iInf_prod, Pi.Colex.sInf_apply, meas_lt_essInf, SummationFilter.symmetricIcc_eq_map_Icc_nat, Measurable.biInf, lt_ciSup_iff, sSup_iUnion_Iic, ENat.iInf_eq_zero, Metric.ediam_iUnion_mem_option, Monotone.linearGrowthSup_comp_mul, MeasureTheory.limsup_measure_le_of_le_liminf_measure_compl, Filter.cardinalInterFilter_inf, MeasureTheory.hitting_of_le, ZFSet.rank_pair, Monotone.le_linearGrowthSup_comp, isPreconnected_Icc_aux, Set.Finite.ciSup_mem_image, ExpGrowth.expGrowthSup_sup, Order.coheight_eq, Ordinal.IsPrincipal.sSup, tendsto_intCast_atTop_cobounded, Cardinal.aleph_limit, MeasureTheory.hitting_of_lt, Monotone.map_sSup_of_continuousAt, EReal.liminf_add_gt_of_gt, SummationFilter.hasProd_symmetricIcc_iff, Topology.IsLower.isTopologicalSpace_basis, bsupr_limsup_dimH, ConditionallyCompleteLinearOrderedField.inducedMap_nonneg, ENNReal.limsup_const_sub, ENNReal.add_iInf₂, Cardinal.mul_eq_max', lowerSemicontinuousOn_ciSup, MeasureTheory.iSup_lintegral_le, Pi.Lex.le_sSup_apply, upperSemicontinuousAt_iInf, upperSemicontinuousWithinAt_iInf, MeasureTheory.OuterMeasure.biInf_apply', CategoryTheory.ObjectProperty.instIsStableUnderShiftISupShiftOfIsClosedUnderIsomorphisms, Finset.Nonempty.ciSup_eq_max'_image, IsCompact.exists_sInf_image_eq, ENNReal.le_limsup_mul, Ordinal.iSup_le_iSup_add_one, Ordinal.iSup_le_iff, Cardinal.iSup_lt_ord_of_isRegular, Int.csSup_of_not_bdd_above, Ordinal.iSup_eq_lsub, csInf_le_csInf', Ordinal.max_zero_right, Summable.tendsto_zero_of_even_summable_symmetricIcc, ENNReal.limsup_add_le, IsTranscendenceBasis.lift_cardinalMk_eq_max_lift, IsTranscendenceBasis.lift_rank_eq_max_lift, tendsto_atTop_of_monotone, Filter.eventually_lt_add_pos_of_limsup_le, MvRatFunc.rank_eq_max_lift, MeasureTheory.lintegral_liminf_le', Monotone.linearGrowthSup_comp, Int.padicValuation_le_one, Ordinal.iSup_add_one_le, MeasureTheory.OuterMeasure.iSup_apply, ENNReal.iSup_mul, cauchy_davenport_minOrder_mul, Ordinal.iSup_eq_lsub_iff, IsCompact.exists_sSup_image_eq, lowerSemicontinuousWithinAt_biSup, ENat.sSup_eq_zero', ENat.le_iInf₂_add_iInf₂, MvPolynomial.cardinalMk_le_max, Cardinal.ciSup_add_ciSup, ENNReal.limsup_sub_const, ENNReal.inv_liminf, NNReal.agm_eq_ciInf, Cardinal.mk_freeCommRing, ENNReal.finsetSum_iSup, MeasureTheory.isTightMeasureSet_range_iff_tendsto_limsup_measure_norm_gt, Pi.Lex.sSup_apply, Ordinal.cof_iSup_add_one, Ordinal.iSup_natCast, lowerSemicontinuousAt_biSup, ENNReal.iInf_gt_eq_self, Cardinal.mk_freeAbelianGroup, Monotone.tendsto_rightLim_within, limsup_finset_sup', ENNReal.eventually_le_limsup, ENNReal.inv_limsup, ClassGroup.norm_le, Ordinal.iSup_iterate_eq_nfp, EReal.limsup_add_bot_of_ne_top, Monotone.le_leftLim, ENat.biSup_add_biSup_le, lt_csSup_iff', Int.instIsOrderBornology, Monotone.map_sInf_of_continuousAt, NNReal.toReal_liminf, Ordinal.lt_iSup_add_one_iff, MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite', Real.limsSup_of_not_isBounded, MeasureTheory.hittingBtwn_of_le, Set.einfsep_iUnion_mem_option, Set.chainHeight_eq_iSup, ENNReal.toNNReal_sInf, IsCompact.isGreatest_sSup, exists_mem_Icc_isFixedPt_of_mapsTo, ENat.exists_eq_iSup₂_of_lt_top, exists_lt_of_lt_ciSup', HahnSeries.cardSupp_hsum_powers_le, ConditionallyCompleteLinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap, Cardinal.add_le_max, MeasureTheory.OuterMeasure.trim_eq_iInf, ZLattice.sum_piFinset_Icc_rpow_le, ContinuousMap.enorm_eq_iSup_enorm, ENNReal.inv_sInf, ENNReal.coe_iInf, Ordinal.apply_omega0_of_isNormal, sInf_within_of_ordConnected, MeasureTheory.isTightMeasureSet_iff_tendsto_measure_compl_closedBall, ENat.iSup_add_iSup_le, ConditionallyCompleteLinearOrderedField.toMulPosStrictMono, Order.height_eq_iSup_last_eq, ENat.toENNReal_iInf, BoundedContinuousFunction.enorm_eq_iSup_enorm, ExpGrowth.expGrowthSup_iSup, Ordinal.card_opow_le, ENNReal.limsup_toReal_eq, dimH_def, NNReal.le_iInf_mul, Cardinal.mk_finsupp_lift_of_infinite', ciSup_mono', upperSemicontinuousWithinAt_ciInf, Order.coheight_eq_iSup_gt_coheight, IsPreconnected.mem_intervals, LinearGrowth.linearGrowthSup_monotone, ModuleCat.projectiveDimension_eq_iSup_localizedModule_prime, tendsto_intCast_atBot_cobounded, IsClosed.isLeast_csInf, NNReal.iSup_mul, MeasureTheory.IsStoppingTime.biInf, ae_lt_of_essSup_lt, LinearGrowth.linearGrowthInf_le_linearGrowthSup_of_frequently_le, Monotone.rightLim, Filter.HasBasis.limsup_eq_ciInf_ciSup, Filter.le_liminf_iff, LinearGrowth.le_linearGrowthInf_comp, Ordinal.IsFundamentalSeq.iSup_add_one_eq, ENNReal.tprod_eq_iInf_prod, Ordinal.lsub_le_sup_succ, MeasureTheory.lpNorm_exponent_top_eq_essSup, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_P, MonotoneOn.exists_monotone_extension, csInf_mem_closure, Antitone.map_sInf_of_continuousAt, MeasureTheory.AECover.iSup_lintegral_eq_of_countably_generated, MeasureTheory.OuterMeasure.ofFunction_apply, Cardinal.mul_le_max, exists_uIoo_isExtrOn_uIcc, CategoryTheory.ObjectProperty.shift_sup, ModuleCat.injectiveDimension_eq_iSup_localizedModule_maximal, ProbabilityTheory.bayesRisk_const', Pell.IsFundamental.y_strictMono, Order.IsSuccPrelimit.iSup_Iio, Dense.ciSup', NNReal.iSup_pow, limsup_sub_const, Ordinal.succ_iSup_le_lsub_iff, AddOreLocalization.cardinalMk_le_max, HahnSeries.cardSupp_inv_le, LinearGrowth.le_linearGrowthSup_iff, MeasureTheory.hittingBtwn_le_iff_of_exists, MeasureTheory.hittingAfter_anti, Finset.ciSup_mem_image, MeasureTheory.setLIntegral_iUnion_of_directed, Monotone.tendsto_nhdsGT, MeasureTheory.lintegral_eq_iSup_eapprox_lintegral, MeasureTheory.hitting_le_iff_of_lt, ENNReal.coe_iSup, lt_ciSup_iff', isLUB_csSup', ENNReal.image_coe_uIcc, AddMonoidAlgebra.cardinalMk_of_infinite, FormalMultilinearSeries.radius_eq_liminf, SummationFilter.hasProd_symmetricIoc_int_iff, Ordinal.IsNormal.apply_of_isSuccLimit, ENNReal.iInf_div', ENNReal.limsup_add_of_left_tendsto_zero, ProbabilityTheory.IdentDistrib.essSup_eq, Ordinal.lsub_sum, Ordinal.iSup_lt_ord, Order.IsNormal.map_sSup, Monotone.map_ciInf_of_continuousAt, csSup_mem_of_not_isSuccPrelimit, Int.csInf_of_not_bdd_below, liminf_min, MeasureTheory.hittingAfter_lt_iff, EReal.liminf_const_mul_of_nonneg_of_ne_top, ENat.add_biSup', EReal.limsup_const_mul_of_nonpos_of_ne_bot, lowerSemicontinuousAt_ciSup, Filter.HasBasis.liminf_eq_ciSup_ciInf, ENNReal.essSup_eq_zero_iff, lowerSemicontinuousOn_iff_le_liminf, limsup_mul_le, EReal.limsup_add_le_of_le, Filter.lt_mem_sets_of_limsSup_lt, Ordinal.cof_iSup_le, MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto, FreeAlgebra.cardinalMk_eq_max, ENNReal.ae_le_essSup, ZFSet.rank_union, limsup_const_sub, ENat.biSup_add, ENNReal.iInf_coe_eq_top, ENNReal.iSup₂_pow_of_ne_zero, Set.Finite.ciSup_lt_iff, Cardinal.mk_iUnion_le, EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act, exists_eq_ciSup_of_not_isSuccPrelimit', ENat.iInf₂_add, Monotone.map_limsup_of_continuousAt, Ordinal.preOmega_max, Int.csSup_empty, trop_sInf_image, MonotoneOn.map_sSup_of_continuousWithinAt, Cardinal.iSup_le_sum, Order.krullDim_le_of_krullDim_preimage_le', CategoryTheory.ObjectProperty.shift_iSup, intermediate_value_Ioc, Cardinal.add_eq_right_iff, limsup_add_const, intermediate_value_Ico, SimpleGraph.eccent_def, Cardinal.iSup_mk_le_mk_iUnion, iSup_limsup_dimH, LinearGrowth.le_linearGrowthInf_add, ZFSet.iSup_card_le_card_iUnion, Ordinal.card_iSup_le_sum_card, Cardinal.mk_finsupp_of_infinite', MvPolynomial.cardinalMk_eq_max_lift, UpperSemicontinuous.limsup_le, Cardinal.ciSup_add, Ordinal.iSup_lt, ENNReal.coe_sInf, Set.Finite.lt_ciInf_iff, Antitone.ciInf_comp_tendsto_atTop_of_linearOrder, MeasureTheory.iInf_mul_le_setLIntegral, Monotone.ciInf_comp_tendsto_atBot_of_linearOrder, MeasureTheory.measure_sigmaFiniteSetGE_ge, ContinuousMap.edist_eq_iSup, Int.padicValuation_eq_zero_iff, FirstOrder.Language.Substructure.lift_card_closure_le, ENat.iSup_coe_lt_top, Metric.infEDist_biUnion, PSet.rank_pair, MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime, EReal.limsup_add_le, analyticOrderAt_add_of_ne, NNReal.iSup_mul_le, egauge_pi', MeasureTheory.OuterMeasure.iSup_sInfGen_nonempty, FreeAlgebra.cardinalMk_eq_max_lift, IsPreconnected.Ioi_csInf_subset, ENNReal.toReal_iSup, AntitoneOn.tendsto_nhdsWithin_Ioo_left, IsCompact.exists_sSup_image_eq_and_ge, Cardinal.sum_eq_iSup_of_lift_mk_le_iSup, NNReal.iInf_const_zero, Antitone.map_limsInf_of_continuousAt, lowerSemicontinuous_biSup, Finite.map_iInf_of_antitone, Monotone.ciSup_comp_tendsto_atTop_of_linearOrder, ClassGroup.exists_mem_finset_approx', sSup_mem_closure, Ordinal.IsFundamentalSeq.iSup_eq, WithTop.coe_sInf, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.sup_P, ENat.sSup_mem_of_nonempty_of_lt_top, IsUltrametricDist.nnnorm_tsum_le, Antitone.ciSup_comp_tendsto_atBot_of_linearOrder, ENNReal.add_biSup, Metric.ediam_insert, MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm', ConditionallyCompleteLinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self, ContinuousOn.strictAntiOn_of_injOn_Icc, LinearMap.lift_rank_comp_le, ClassGroup.exists_mem_finsetApprox, Multiset.iInf_mem_map_of_exists_le_sInf_empty, Rat.padicValuation_le_one_iff, PiLp.nndist_eq_iSup, MeasureTheory.le_hittingBtwn_of_exists, MeasureTheory.hitting_isStoppingTime, MeasureTheory.Adapted.isStoppingTime_hittingAfter, Set.Nonempty.csInf_mem, upperClosure_eq_Ici_csInf, MvPolynomial.cardinalMk_eq_max, sSup_within_of_ordConnected, Ordinal.sInf_empty, Frequently.le_linearGrowthSup, Ordinal.sup_typein_succ, exists_eq_iSup_of_not_isSuccPrelimit, MeasureTheory.Measure.iSup_restrict_spanningSets_of_measurableSet, MeasureTheory.lintegral_le_iSup, Algebraic.cardinalMk_lift_le_max, FirstOrder.Language.BoundedFormula.card_le, MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le, MeasureTheory.hittingBtwn_eq_hittingBtwn_of_exists, IsCompact.exists_sInf_image_eq_and_le, SimpleGraph.radius_eq_iInf_iSup_edist, ENNReal.mul_iSup, Algebra.rank_adjoin_le, EMetric.diam_iUnion_mem_option, Int.cobounded_eq, Filter.gt_mem_sets_of_limsInf_gt, csSup_eq_csSup_of_forall_exists_le, LinearGrowth.linearGrowthInf_neg, ConditionallyCompleteLinearOrderedField.lt_inducedMap_iff, NNReal.coe_sInf, limsSup_nhds, Monotone.le_expGrowthSup_comp, exists_lt_of_csInf_lt, ENNReal.toReal_sInf, Int.csInf_empty, EisensteinSeries.tsum_symmetricIco_tsum_sub_eq, Ordinal.succ_lt_iSup_of_ne_iSup, liminf_const_add, Monotone.leftLim_le_rightLim
toDecidableEq 📖	CompOp	1 math math: compare_eq_compareOfLessAndEq
toDecidableLE 📖	CompOp	—
toDecidableLT 📖	CompOp	1 math math: compare_eq_compareOfLessAndEq
toOrd 📖	CompOp	1 math math: compare_eq_compareOfLessAndEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compare_eq_compareOfLessAndEq 📖	mathematical	—	toOrd Preorder.toLT PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice toConditionallyCompleteLattice toDecidableLT toDecidableEq	—	—
csInf_of_not_bddBelow 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice toConditionallyCompleteLattice	InfSet.sInf ConditionallyCompleteLattice.toInfSet toConditionallyCompleteLattice Set Set.instEmptyCollection	—	—
csSup_of_not_bddAbove 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice toConditionallyCompleteLattice	SupSet.sSup ConditionallyCompleteLattice.toSupSet toConditionallyCompleteLattice Set Set.instEmptyCollection	—	—
le_total 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice toConditionallyCompleteLattice	—	—

ConditionallyCompleteLinearOrderBot

Definitions

Name	Category	Theorems
toConditionallyCompleteLinearOrder 📖	CompOp	1020 math math: Ordinal.iSup_eq_iSup, LinearGrowth.linearGrowthSup_zero, IsClosed.sSup_mem, LinearGrowth.linearGrowthSup_top, Ordinal.iSup_eq_bsup, ENat.sub_iInf, ProbabilityTheory.bayesRisk_of_subsingleton, ENNReal.iInf_div_of_ne, Order.IsNormal.apply_of_isSuccLimit, Ordinal.lift_card_iSup_le_sum_card, Acc.rank_eq, Cardinal.mk_sUnion_le, Ordinal.iSup_pow_natCast, Ordinal.cof_iSup_add_one_le, Module.rank_def, MeasureTheory.lintegral_def, Algebra.lift_cardinalMk_adjoin_le, Ordinal.sup_eq_lsub_iff_lt_sup, SymmetricAlgebra.rank_eq, isSaddlePointOn_value, Ordinal.cof_iSup_le_lift, Set.Finite.einfsep, MeasureTheory.iInf_mul_le_lintegral, Cardinal.powerlt_max, EMetric.hausdorffEdist_iUnion_le, ENNReal.add_sInf, ENat.sSup_eq_top_of_infinite, iSup_eq_of_tendsto, dimH_sUnion, Ordinal.sInf_compl_lt_lift_ord_succ, Set.einfsep_of_fintype, lowerSemicontinuousOn_biSup, Pi.Lex.sSup_apply_le, MeasureTheory.lintegral_iSup', ENNReal.le_liminf_mul, Cardinal.lift_iSup_le_lift_iSup, Ordinal.max_zero_left, Cardinal.mk_list_eq_max_mk_aleph0, LinearGrowth.linearGrowthInf_add_le', ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm, Cardinal.mk_list_le_max, EReal.liminf_add_top_of_ne_bot, LinearGrowth.le_linearGrowthSup_add, csSup_le', CategoryTheory.ObjectProperty.HasCardinalLT.sup, NNReal.iSup_of_not_bddAbove, Ordinal.sup_eq_lsub_iff_succ, FormalMultilinearSeries.radius_pi_eq_iInf, ENNReal.ofNNReal_limsup, AntitoneOn.map_sSup_of_continuousWithinAt, lowerSemicontinuousWithinAt_iSup, NNReal.mul_iSup_le, ENat.iInf_mul_of_ne, Cardinal.mk_multiset_of_nonempty, ENat.smul_sSup, ModuleCat.injectiveDimension_eq_iSup_localizedModule_prime, Ordinal.cof_iSup_Iio, MeasureTheory.setLIntegral_le_iSup_mul, Ordinal.iSup_typein_succ, LinearGrowth.linearGrowthSup_add_le, MeasureTheory.hittingAfter_bot_le_iff, upperSemicontinuousAt_biInf, Metric.hausdorffEDist_def, banach_steinhaus_iSup_nnnorm, CategoryTheory.ObjectProperty.instHasInducedTStructureMinOfIsClosedUnderIsomorphisms, MeasureTheory.isTightMeasureSet_iff_inner_tendsto, Cardinal.iSup_of_empty, ENNReal.limsup_const_mul_of_ne_top, sSup_Iio_eq_self_iff_isSuccPrelimit, IsOpen.measure_eq_iSup_isClosed, Cardinal.iSup_lt_of_isRegular, ContinuousLinearMap.nnnorm_def, Metric.hausdorffEDist_iUnion_le, ENat.iSup_add_iSup_of_monotone, ENNReal.iSup_pow_of_ne_zero, ENat.iSup_zero, Nat.tendsto_iSup_of_tendsto_limsup, MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top, Cardinal.mul_le_max_of_aleph0_le_right, NNReal.coe_sSup, MeasureTheory.lintegral_iSup_ae, MeasureTheory.IsStoppingTime.iInf, Filter.cardinalInterFilter_sup, Cardinal.sum_pow_le_max_aleph0, Ordinal.sup_succ_le_lsub, MonoidAlgebra.cardinalMk_of_infinite, exists_eq_iInf_of_not_isPredPrelimit, LowerSemicontinuousOn.le_liminf, Ordinal.iSup_le_lsub, Ordinal.card_iSup_Iio_le_sum_card, MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top, ENat.iInf_toNat, NNReal.limsInf_of_not_isCobounded, Cardinal.iSup_lt_of_lt_cof_ord, Cardinal.mul_eq_max_of_aleph0_le_right, ENNReal.ofReal_iInf, MeasureTheory.OuterMeasure.coe_iSup, Cardinal.sum_le_mk_mul_iSup, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone, ENat.iInf_add_iInf, NNReal.segment_eq_uIcc, MeasureTheory.lintegral_iSup_directed, ENat.iInf_sum, ProbabilityTheory.bayesRisk_of_subsingleton', Ideal.sup_primeHeight_eq_ringKrullDim, ENNReal.iSup_add_iSup_le, Pi.Colex.le_sSup_apply, LinearGrowth.le_linearGrowthSup_add', ENNReal.limsup_mul_le, Directed.measure_iUnion, Cardinal.mk_finsupp_lift_of_infinite, MeasureTheory.lowerCrossingTime_le, Submodule.spanRank_toENat_eq_iInf_encard, ExpGrowth.expGrowthSup_add, ENat.exists_eq_iSup_of_lt_top, LinearGrowth.linearGrowthInf_bot, NNReal.coe_iSup, MeasureTheory.Measure.mkMetric_apply, ENNReal.mul_iInf, ENNReal.limsup_const_mul, MeasureTheory.Measure.iInf_IicSnd_gt, Subfield.cardinalMk_closure_le_max, MeasureTheory.biSup_measure_Iic, Cardinal.mul_eq_left_iff, ENNReal.toNNReal_sSup, Ordinal.iSup_lt_of_lt_cof, MeasureTheory.lintegral_iInf_ae, Ordinal.sSup_add_one_lt_of_lt_cof, ENNReal.inv_sSup, MeasureTheory.lintegral_iInf', Cardinal.lift_iInf, ENNReal.limsup_liminf_le_liminf_limsup, MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum, spectrum.spectralRadius_le_liminf_pow_nnnorm_pow_one_div, CategoryTheory.ObjectProperty.shiftClosure_eq_iSup, LinearGrowth.linearGrowthSup_bot, ContinuousLinearMap.sSup_sphere_eq_nnnorm, MeasureTheory.SimpleFunc.iSup_coe_eapprox, WithTop.coe_sSup, ENNReal.liminf_toReal_eq, MeasurableSet.measure_eq_iSup_isCompact_of_ne_top, Algebraic.cardinalMk_le_max, lowerSemicontinuousOn_iSup, lowerSemicontinuous_iff_le_liminf, LinearGrowth.linearGrowthInf_biInf, Order.IsSuccLimit.iSup_Iio, upperSemicontinuous_biInf, ENat.mul_iSup, ENat.sSup_eq_zero, IsClosed.sInf_mem, MeasureTheory.Measure.LebesgueDecomposition.iSup_succ_eq_sup, NNReal.iSup_eq_zero, Matroid.cRank_eq_iSup_cardinalMk_indep, Ordinal.card_sInf_range_compl_le_lift, MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE, Ordinal.iSup_le, Pi.Colex.sSup_apply, ENNReal.le_iInf₂_add_iInf₂, NNReal.natCast_iInf, Algebra.IsAlgebraic.cardinalMk_le_max, hasCardinalLT_subtype_max, ExpGrowth.expGrowthSup_def, Cardinal.sum_eq_lift_iSup_of_lift_mk_le_lift_iSup, MeasureTheory.limsup_lintegral_le, MeasureTheory.OuterMeasure.iInf_apply', Ordinal.iSup_succ, Ordinal.Principal.sSup, Set.Finset.coe_einfsep, egauge_univ_pi, Eventually.le_linearGrowthInf, Ordinal.lift_cof_iSup_add_one, ProbabilityTheory.bayesRisk_eq_iInf_measure_of_subsingleton, ENNReal.iInf_div, ExpGrowth.expGrowthSup_biSup, MeasureTheory.eLpNormEssSup_eq_iSup, MeasureTheory.exists_isSigmaFiniteSet_measure_ge, ENat.biSup_add', Finset.sup_univ_eq_ciSup, ENat.sum_iSup, MeasureTheory.Measure.mkMetric_le_liminf_tsum, csSup_le_csSup', ENNReal.biSup_add, MeasureTheory.measure_sigmaFiniteSetGE_le, ENat.iInf_mul', ENNReal.sSup_div, ENNReal.essSup_add_le, Pi.Lex.sInf_apply, Ordinal.card_omega0_opow, Ordinal.iSup_pow, EMetric.diam_insert, Cardinal.lift_iSup, Ordinal.deriv_limit, ENNReal.iInf_sum, ENNReal.coe_sSup, liminf_eq_top, NNReal.image_coe_uIcc, Pi.Lex.sInf_apply_le, Dynamics.coverEntropyEntourage_union, Ordinal.card_sInf_range_compl_le, LinearGrowth.linearGrowthInf_top, MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le, Ordinal.iSup_add_one_lt_of_lt_cof, ENNReal.biSup_add_biSup_le, le_ciSup_iff', csSup_le_iff', Ordinal.sSup_eq_bsup, EReal.limsup_neg, Cardinal.lift_sSup, MeasureTheory.upperCrossingTime_mono, FreeAlgebra.cardinalMk_le_max, Cardinal.aleph_add_aleph, Ordinal.iSup_add_nat, ENNReal.essSup_const_mul, Cardinal.mk_biUnion_le_lift, ENNReal.iSup_coe_lt_top, LinearGrowth.linearGrowthInf_const_mul_self, Order.krullDim_le_of_krullDim_preimage_le, MeasureTheory.lintegral_le_iSup_mul, MonoidAlgebra.cardinalMk_lift_of_infinite, Cardinal.lift_iSup_le, LowerSemicontinuousWithinAt.le_liminf, Ordinal.iSup_sum, MeasureTheory.hittingBtwn_bot_le_iff, ENNReal.ofReal_limsup_toReal, ENat.iInf_coe_lt_top, ProbabilityTheory.avgRisk_le_iSup_risk, WType.cardinalMk_le_max_aleph0_of_finite', ENNReal.iSup_natCast, CategoryTheory.ObjectProperty.IsLocal.inf, ENat.iInf_mul, Topology.IsUpper.isTopologicalSpace_basis, ENNReal.ofReal_limsup, ENat.add_iInf, PseudoMetricSpace.dist_ofPreNNDist, Dynamics.coverEntropy_union, limsup_eq_bot, MvPowerSeries.le_order_subst, MeasureTheory.essSup_trim, Ordinal.lift_cof_iSup, ENat.add_iSup, ciInf_le', NNReal.iSup_mul_iSup_le, FirstOrder.Language.card_functions_sum_skolem₁_le, MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ, ENNReal.iInf_add_iInf, PSet.rank_insert, MeasureTheory.OuterMeasure.trim_eq_iInf', MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure, SimpleGraph.chromaticNumber_eq_iInf, Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub, ENat.mul_sSup, LinearGrowth.linearGrowthInf_zero, SimpleGraph.chromaticNumber_sum, upperSemicontinuousOn_iInf, MeasurableSet.measure_eq_iSup_isCompact, Ordinal.sup_succ_eq_lsub, MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite, LowerSemicontinuousAt.le_liminf, Ordinal.sSup_ord, AddMonoidAlgebra.cardinalMk_of_infinite', Eventually.linearGrowthSup_le, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, MeasureTheory.Content.outerMeasure_eq_iInf, Cardinal.mul_eq_max, ENNReal.liminf_sub_const, Cardinal.mk_freeMonoid, Cardinal.mk_bounded_set_le, Ordinal.enumOrd_zero, ENNReal.smul_iSup, Order.krullDim_eq_iSup_coheight_of_nonempty, ENNReal.iSup_add, LinearGrowth.linearGrowthSup_le_of_eventually_le, ENat.coe_sSup, ENNReal.iInf_mul_of_ne, MeasureTheory.measure_biUnion_eq_iSup, MeasureTheory.limsup_measure_closed_le_iff_liminf_measure_open_ge, Ordinal.iSup_mul_nat, ENNReal.tsum_iSup_eq, ENat.sInf_eq_zero, MeasurableSpace.cardinal_generateMeasurableRec_le, Order.krullDim_eq_iSup_length, Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim, Finset.Nonempty.ciSup_mem_image, egauge_pi, WithTop.iInf_coe_eq_top, essSup_comp_quotientAddGroup_mk, ENNReal.add_iInf, Set.Nonempty.ciSup_lt_iff, csInf_le', NNReal.agm_eq_ciSup, ENNReal.toNNReal_iSup, Antitone.measure_iUnion, MeasureTheory.lintegral_liminf_le, WType.cardinalMk_le_max_aleph0_of_finite, upperSemicontinuousWithinAt_iff_limsup_le, ENNReal.tsum_eq_iSup_nat', Metric.ediam_eq_sSup, ENNReal.inv_iSup, MeasureTheory.OuterMeasure.iInf_apply, UpperSemicontinuousWithinAt.limsup_le, csSup_mem_of_not_isSuccPrelimit', Cardinal.mk_list_eq_max, ENat.sInf_add, EReal.min_neg_neg, MeasureTheory.limsup_measure_compl_le_of_le_liminf_measure, upperSemicontinuousOn_iff_limsup_le, LinearGrowth.linearGrowthSup_biSup, Cardinal.mk_freeAddGroup, iInf_eq_of_tendsto, Ordinal.sup_le_lsub, Cardinal.sum_eq_iSup_of_mk_le_iSup, ENNReal.liminf_mul_le, EReal.le_liminf_add, Ordinal.iSup_add_natCast, FormalMultilinearSeries.radius_inv_eq_limsup, Set.einfsep_insert, ENat.add_sSup, ENNReal.tsum_eq_iSup_sum, Ordinal.IsNormal.map_iSup, NNReal.sSup_of_not_bddAbove, ciSup_le_iff', Order.coheight_eq_iSup_head_eq, Ordinal.card_iSup_Iio_le_card_mul_iSup, Cardinal.mk_finsupp_nat, MeasureTheory.le_liminf_measure_open_of_forall_tendsto_measure, LinearGrowth.linearGrowthSup_inv, LinearGrowth.linearGrowthInf_const, MeasureTheory.OuterMeasure.biInf_apply, ENNReal.essSup_piecewise, ENNReal.iInf_add, ProbabilityTheory.bayesRisk_const_of_nonempty, ENat.coe_iSup, ENat.smul_iSup, ENNReal.mul_iInf', EReal.liminf_add_le, MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le, LinearGrowth.linearGrowthSup_le_iff, Cardinal.mul_ciSup, NNReal.iSup_pow_of_ne_zero, Order.krullDim_eq_iSup_height_of_nonempty, ExpGrowth.le_expGrowthInf_comp, ENNReal.liminf_const_sub, EMetric.infEdist_biUnion, MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral, ENNReal.iInf_add_iInf_of_monotone, MeasureTheory.tendsto_measure_norm_gt_of_isTightMeasureSet, Ordinal.sup_eq_bsup, LinearGrowth.linearGrowthSup_const_mul_self, Cardinal.ciSup_mul, MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto, ciSup_le', Set.einfsep_insert_le, MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict, Ordinal.Principal.iSup, ENat.sub_iSup, ENat.iInf_eq_top_of_isEmpty, MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm, Cardinal.ord_eq_Inf, CategoryTheory.ObjectProperty.instIsStableUnderShiftByMin, ENNReal.biSup_add', MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto, le_ciInf_iff', csSup_empty, ENat.iInf_coe_eq_top, Ordinal.cof_iSup, WithTop.iSup_coe_lt_top, ENNReal.iSup_add_iSup, lowerSemicontinuous_iSup, IntermediateField.cardinalMk_adjoin_le, ENNReal.coe_essSup, Cardinal.mk_freeAddMonoid, ENNReal.iSup_sub, ENNReal.tsum_eq_iSup_sum', MonotoneOn.map_sInf_of_continuousWithinAt, MvPowerSeries.le_weightedOrder_subst, Cardinal.mul_le_max_of_aleph0_le_left, Cardinal.powerlt_min, Cardinal.power_nat_le_max, MeasureTheory.measure_sigmaFiniteSetWRT', ENat.exists_eq_iInf, Monotone.map_iInf_of_continuousAt, IsCompact.measure_eq_iInf_isOpen, ENNReal.sub_eq_sInf, Ordinal.opow_limit, MeasureTheory.OuterMeasure.ofFunction_eq_iInf_mem, Algebra.IsAlgebraic.lift_cardinalMk_le_max, Cardinal.preAleph_limit, Order.height_eq_iSup_lt_height, dimH_eq_iInf, ENNReal.le_iInf_mul, le_csSup_iff', MeasureTheory.isTightMeasureSet_range_iff_tendsto_limsup_inner, NormedSpace.equicontinuous_TFAE, MonoidAlgebra.cardinalMk_of_infinite', LinearGrowth.linearGrowthSup_sup, IsOpen.measure_eq_iSup_isCompact, PiLp.nnnorm_eq_ciSup, Cardinal.lift_iSup_le_sum, MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd, MeasureTheory.limsup_trim, Monotone.measure_iInter, MeasureTheory.Measure.inf_apply, ENNReal.essSup_liminf_le, Ordinal.cof_iSup_Iio_add_one, Pi.Colex.sSup_apply_le, Cardinal.ord_eq_iInf, UpperSemicontinuousOn.limsup_le, LinearGrowth.linearGrowthInf_inf, Relation.cutExpand_le_invImage_lex, HahnSeries.cardSupp_div_le, upperSemicontinuous_iInf, WithTop.iInf_coe_lt_top, ENat.coe_iInf, dimH_bUnion, EReal.coe_toENNReal_eq_max, Cardinal.sum_le_lift_mk_mul_iSup, ENNReal.inv_iInf, Ordinal.max_eq_zero, Ordinal.bsup_eq_sup, ENat.mul_iInf_of_ne, EMetric.infEdist_iUnion, Cardinal.mk_freeRing, Multiset.iSup_mem_map_of_ne_zero, sInf_mem_closure, Ordinal.lift_iSup_add_one_lt_of_lt_cof, ENNReal.toNNReal_iInf, Cardinal.add_eq_max', MeasureTheory.eLpNormEssSup_eq_essSup_enorm, MeasureTheory.inducedOuterMeasure_eq_iInf, MeasureTheory.lintegral_iInf, MeasureTheory.le_iInf_lintegral, Ordinal.card_opow_le_of_omega0_le_right, NNReal.le_iInf_mul_iInf, ENNReal.le_iInf_mul_iInf, AddMonoidAlgebra.cardinalMk_eq_max_lift_of_infinite', LinearGrowth.linearGrowthSup_eventually_monotone, ciSup_or', Ordinal.IsPrincipal.iSup, trdeg_eq_iSup_cardinalMk_isTranscendenceBasis, CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂MinOfIsClosedUnderIsomorphisms, Cardinal.mul_mk_eq_max, Ordinal.iSup_mul_natCast, LowerSemicontinuous.le_liminf, Ordinal.mem_closure_iff_iSup, Cardinal.sInf_eq_zero_iff, LinearGrowth.linearGrowthSup_const, Ordinal.sSup_le_sSup_add_one, NNReal.iSup_div, LSeries.abscissaOfAbsConv_binop_le, MeasureTheory.measure_iUnion_of_tendsto_zero, ENat.iSup_natCast, MeasureTheory.Lp.eLpNorm'_lim_eq_lintegral_liminf, Ordinal.iSup_lt_ord_lift, Cardinal.aleph_max, LSeries.abscissaOfAbsConv_add_le, Pi.Colex.sInf_apply_le, ciSup_of_empty, CategoryTheory.ObjectProperty.HasCardinalLT.iSup, ProbabilityTheory.bayesRisk_le_iInf, PiLp.edist_eq_iSup, OreLocalization.cardinalMk_le_max, ENat.iInf_add_iInf_of_monotone, Manifold.riemannianEDist_def, LinearGrowth.linearGrowthInf_natCast_nonneg, ENNReal.tsum_eq_limsup_sum_nat, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone', IsOpen.measure_eq_biSup_integral_continuous, ExpGrowth.expGrowthInf_inf, Ordinal.card_opow_omega0, Ordinal.cof_eq_sInf_lsub, Cardinal.add_eq_max, Pi.Lex.le_sInf_apply, MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup, UpperSemicontinuousAt.limsup_le, AntitoneOn.map_sInf_of_continuousWithinAt, EReal.le_limsup_mul, sInf_mem_of_not_isPredPrelimit, MeasureTheory.hitting_bot_le_iff, ENNReal.toReal_limsup, EReal.limsup_mul_le, LinearGrowth.linearGrowthSup_comp_nonneg, spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius, Cardinal.preAleph_max, Order.krullDim_eq_iSup_coheight, ENNReal.add_iSup, OrderIso.map_ciSup', ENNReal.iSup_coe_eq_top, SimpleGraph.edist_eq_sInf, upperSemicontinuousAt_iff_limsup_le, Antitone.map_sSup_of_continuousAt, ENNReal.ofNNReal_liminf, EReal.le_liminf_mul, ENat.iSup_mul, Ordinal.mem_closure_tfae, Cardinal.iSup_lt_ord_lift_of_isRegular, BoundedContinuousFunction.nndist_eq_iSup, le_analyticOrderAt_sub, le_analyticOrderAt_add, MeasureTheory.OuterMeasure.sSup_apply, NNReal.natCast_iSup, ExpGrowth.le_expGrowthInf_add, SimpleGraph.ediam_eq_iSup_iSup_edist, Cardinal.iSup_lt_lift_of_isRegular, Ordinal.iSup'_eq_bsup, LSeries.abscissaOfAbsConv_convolution_le, Polynomial.cardinalMk_eq_max, Order.krullDim_eq_iSup_height, ContinuousLinearMap.sSup_unit_ball_eq_nnnorm, UniformOnFun.edist_def', Monotone.linearGrowthInf_nonneg, MeasureTheory.tendsto_measure_sigmaFiniteSetGE, Topology.IsScott.instUnivSetOfIsUpper, IsAlgClosed.cardinal_le_max_transcendence_basis', MeasureTheory.Measure.hausdorffMeasure_le_liminf_tsum, hasCardinalLT_subtype_iSup, ENat.sSup_add, Cardinal.beth_limit, ExpGrowth.expGrowthSup_comp_le, Ordinal.lt_iSup_add_one, upperSemicontinuous_iff_limsup_le, ENNReal.biSup_add_biSup_le', Cardinal.mk_biUnion_le, MeasureTheory.lintegral_iSup_directed_of_measurable, MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part, Submodule.spanRank_toENat_eq_iInf_finset_card, isSaddlePointOn_iff', Ordinal.iSup_sequence_lt_omega_one, ENNReal.mul_sSup, ENNReal.iSup_add_iSup_of_monotone, FirstOrder.Language.Term.card_sigma, ENNReal.mul_iInf_of_ne, Ordinal.cof_lift_iSup_add_one_le, MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE', ENNReal.ofReal_essSup, ENat.coe_sInf, Cardinal.mk_bounded_subset_le, ENNReal.sSup_mul, ENNReal.iSup_zero, ENat.add_sInf, Set.einfsep_eq_iInf, IsWellFounded.rank_eq, Ordinal.iSup_typein_limit, ENat.iSup_eq_zero, essSup_comp_quotientGroup_mk, EReal.liminf_neg, Ordinal.iSup_lt_lift, LinearGrowth.linearGrowthInf_eventually_monotone, MeasureTheory.lintegral_eq_nnreal, UniformFun.edist_def, Cardinal.mk_iUnion_le_lift, WithTop.isGLB_sInf, ENNReal.iInf_mul_iInf, MeasureTheory.SimpleFunc.lintegral_restrict_iUnion_of_directed, ENat.biSup_add_biSup_le', NNReal.le_mul_iInf, ENNReal.limsup_eq_zero_iff, MeasureTheory.IsFundamentalDomain.essSup_measure_restrict, Cardinal.add_mk_eq_max, ExpGrowth.expGrowthInf_iInf, EReal.liminf_mul_le, Ordinal.derivFamily_limit, BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm, EReal.max_neg_neg, MeasureTheory.OuterMeasure.sInf_apply, MeasureTheory.iInf_le_lintegral, ZFSet.rank_range, iSup₂_iInf₂_le_iInf₂_iSup₂, ENNReal.add_biSup', lowerSemicontinuousWithinAt_iff_le_liminf, Cardinal.succ_def, Monotone.expGrowthInf_comp_le, Ordinal.iSup_ord, exists_lt_of_lt_csSup', ENNReal.hasSum, ENat.iSup_add_iSup, ZFSet.rank_insert, ENat.iSup_add, Ordinal.sup_eq_sup, Ordinal.sSup_lt_of_lt_cof, Pi.Colex.le_sInf_apply, StieltjesFunction.length_eq, ENNReal.add_sSup, Ordinal.le_iSup, MeasureTheory.measure_eq_iInf', le_csInf_iff'', ENNReal.iInf_mul', MeasureTheory.lintegral_iInf_directed_of_measurable, Ordinal.iSup_eq_zero_iff, ENat.le_iInf_add_iInf, Cardinal.sInf_empty, Metric.infEDist_iUnion, Cardinal.mk_freeGroup, ENNReal.iSup_div, Set.Nonempty.ciSup_mem_image, LinearGrowth.linearGrowthInf_iInf, lowerSemicontinuousAt_iff_le_liminf, UniformOnFun.edist_def, MeasureTheory.Measure.iInf_rat_gt_prod_Iic, MeasureTheory.OuterMeasure.boundedBy_apply, Ordinal.card_opow_eq_of_omega0_le_right, ENNReal.limsup_add_of_right_tendsto_zero, eVariationOn.eVariationOn_eq_strictMonoOn, ProbabilityTheory.iSup_bayesRisk_le_minimaxRisk, LinearGrowth.linearGrowthInf_monotone, MeasurableSpace.cardinal_measurableSet_le, iSup_succ, Ordinal.sup_eq_bsup', Ordinal.succ_iSup_eq_lsub_iff, MeasurableSpace.cardinal_generateMeasurable_le, ENat.mul_iInf, SimpleGraph.diam_def, ENat.sSup_mul, Cardinal.sum_le_lift_mk_mul_iSup_lift, IsAlgClosed.cardinal_le_max_transcendence_basis, ENat.iSup_coe_eq_top, ProbabilityTheory.bayesRisk_le_iInf', ENat.iInf_add, ENNReal.toReal_essSup, BoundedContinuousFunction.edist_eq_iSup, Ordinal.sup_eq_lsub, ExpGrowth.expGrowthInf_biInf, LinearGrowth.linearGrowthSup_iSup, LinearGrowth.linearGrowthInf_comp_nonneg, ENNReal.essSup_mul_le, Ordinal.lift_card_sInf_compl_le, iSup_Iio_eq_self_iff_isSuccPrelimit, Order.IsSuccLimit.sSup_Iio, Ordinal.iSup_eq_lsub_iff_lt_iSup, ENNReal.toReal_sSup, ENNReal.sub_iSup, ContinuousMap.nnnorm_eq_iSup_nnnorm, Antitone.measure_iInter, MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd, ENNReal.liminf_add_of_right_tendsto_zero, Topology.IsScott.scott_eq_upper_of_completeLinearOrder, MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup, Ordinal.IsNormal.map_iSup_of_bddAbove, Cardinal.preBeth_limit, ProbabilityTheory.bayesRisk_const_of_neZero, MeasureTheory.measure_eq_iInf, ENNReal.limsup_mul_le', MeasureTheory.le_iInf₂_lintegral, upperSemicontinuousOn_biInf, MeasureTheory.Measure.iSup_restrict_spanningSets, ContinuousMap.nndist_eq_iSup, NNReal.limsSup_of_not_isBounded, ENNReal.le_iInf_add_iInf, MeasureTheory.lintegral_iSup, Ordinal.lt_iSup_iff, Cardinal.aleph_mul_aleph, ENNReal.iInf_mul, Ordinal.IsNormal.map_sSup_of_bddAbove, ENNReal.toReal_iInf, Ordinal.iSup_add_one_le_iff, MeasureTheory.lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure, ENNReal.iSup_eq_zero, ENNReal.sInf_add, Ordinal.card_opow_le_of_omega0_le_left, Ordinal.bsup'_eq_iSup, Ordinal.IsNormal.apply_omega0, MeasurableSet.measure_eq_iSup_isClosed_of_ne_top, ENNReal.iInf_coe_lt_top, Cardinal.lift_iSup_lt_of_lt_cof_ord, ModuleCat.projectiveDimension_eq_iSup_localizedModule_maximal, CategoryTheory.ObjectProperty.instIsStableUnderShiftMin, Ordinal.iSup_add_one, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, MeasureTheory.eLpNormEssSup_count, ProbabilityTheory.bayesRisk_const, Ordinal.iSup_Iio_eq_bsup, WithTop.iSup_coe_eq_top, NNReal.coe_iInf, MeasureTheory.OuterMeasure.iUnion_of_tendsto_zero, Antitone.map_iSup_of_continuousAt, Ordinal.iSup_Iio_add_one, FirstOrder.Language.Term.card_le, cauchy_davenport_minOrder_add, WithTop.isLUB_sSup, ENNReal.smul_sSup, Antitone.map_iInf_of_continuousAt, EReal.limsup_const_mul_of_nonneg_of_ne_top, SimpleGraph.chromaticNumber_eq_biInf, Ordinal.iSup_eq_of_range_eq, Ordinal.card_opow_eq_of_omega0_le_left, Monotone.map_iSup_of_continuousAt, ZFSet.rank_iUnion, ENNReal.sSup_add, Ordinal.IsNormal.map_sSup, LinearGrowth.le_linearGrowthInf_iff, Topology.IsScott.isOpen_iff_Iic_compl_or_univ, MeasureTheory.upperCrossingTime_zero', MeasureTheory.iSup₂_lintegral_le, Order.krullDim_eq_iSup_height_add_coheight_of_nonempty, Ordinal.iSup_sequence_lt_omega1, ENNReal.tsum_eq_iSup_nat, AlgebraicGeometry.geometrically_inf, ENNReal.iInf₂_add, Ordinal.bsup_eq_iSup, upperSemicontinuousWithinAt_biInf, SimpleGraph.ediam_def, Ordinal.lsub_le_succ_iSup, Cardinal.add_mk_eq_max', NNReal.limsup_of_not_isBoundedUnder, ENNReal.essSup_indicator_eq_essSup_restrict, Cardinal.ciSup_mul_ciSup, Cardinal.lift_sInf, MeasureTheory.OuterMeasure.top_apply', MvPolynomial.cardinalMk_le_max_lift, ExpGrowth.expGrowthInf_def, LinearGrowth.linearGrowthInf_le_of_eventually_le, ENNReal.tsum_eq_liminf_sum_nat, LinearGrowth.linearGrowthInf_le_iff, NNReal.iSup_empty, EReal.le_limsup_add, IsUltrametricDist.nnnorm_tprod_le, MeasureTheory.Measure.hausdorffMeasure_apply, LinearGrowth.linearGrowthSup_comp_le, Monotone.linearGrowthInf_comp_le, Cardinal.sSup_lt_of_lt_cof_ord, max_aleph0_card_le_rank_fun_nat, FreeAlgebra.cardinalMk_le_max_lift, IntermediateField.lift_cardinalMk_adjoin_le, ProbabilityTheory.bayesRisk_discard, ENNReal.iSup_pow, Ideal.sup_height_eq_ringKrullDim, Monotone.linearGrowthInf_comp_mul, isSaddlePointOn_iff, Ordinal.mem_iff_iSup_of_isClosed, NNReal.mul_iSup, EMetric.hausdorffEdist_def, MeasureTheory.le_measure_compl_liminf_of_limsup_measure_le, ENNReal.sub_iInf, ENNReal.essSup_restrict_eq_of_support_subset, MeasureTheory.lowerCrossingTime_mono, Cardinal.add_ciSup, Set.measure_eq_iInf_isOpen, LSeries.abscissaOfAbsConv_sub_le, MeasureTheory.Measure.mkMetric_le_liminf_sum, Ordinal.sInf_compl_lt_ord_succ, MeasureTheory.lintegral_enorm_le_liminf_of_tendsto, tendsto_iSup_of_tendsto_limsup, ENNReal.iSup_lt_eq_self, MeasureTheory.OuterMeasure.sInf_apply', EReal.liminf_const_mul_of_nonpos_of_ne_bot, Cardinal.powerlt_aleph0_le, BoundedContinuousFunction.nndist_eq, ENNReal.finsetSum_iSup_of_monotone, IsCompact.measure_eq_biInf_integral_hasCompactSupport, MonoidAlgebra.cardinalMk_lift_of_infinite', NNReal.liminf_of_not_isCoboundedUnder, MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf, MeasureTheory.SimpleFunc.iSup_eapprox_apply, MeasureTheory.ae_eq_set_symmDiff, ENat.toENNReal_iSup, Ordinal.isClosed_iff_iSup, MeasureTheory.upperCrossingTime_le, Ordinal.bsup_eq_sup', Cardinal.add_eq_left_iff, csSup_empty, Ordinal.lift_iSup_lt_of_lt_cof, LinearMap.rank_comp_le, Cardinal.mk_finsupp_of_infinite, NNReal.sInf_empty, dimH_iUnion, NNReal.mul_iInf, NNReal.toReal_limsup, MeasureTheory.StronglyAdapted.isStoppingTime_leastGE, Monotone.measure_iUnion, ciInf_le_of_le', LinearGrowth.linearGrowthInf_add_le, Cardinal.mul_eq_max_of_aleph0_le_left, NNReal.iInf_mul, Frequently.linearGrowthInf_le, MeasureTheory.tendsto_measure_compl_closedBall_of_isTightMeasureSet, Cardinal.lift_iSup_le_lift_iSup', Ordinal.sup_typein_limit, Order.IsSuccPrelimit.sSup_Iio, Ordinal.omega_max, AddMonoidAlgebra.cardinalMk_eq_max_lift_of_infinite, sSup_mem_of_not_isSuccPrelimit, ENat.add_iInf₂, Polynomial.cardinalMk_le_max, List.iSup_mem_map_of_ne_nil, ENNReal.iSup_mul_le, Monotone.linearGrowthInf_comp, ENat.add_biSup, NNReal.iInf_empty, ciSup_false, ENNReal.liminf_add_of_left_tendsto_zero, MeasureTheory.OuterMeasure.sInfGen_def, Directed.measure_iInter, ENat.mul_iInf', Algebra.cardinalMk_adjoin_le, EMetric.diam_eq_sSup, ENat.sum_iSup_of_monotone, NNReal.le_iInf_add_iInf, MeasureTheory.isTightMeasureSet_iff_tendsto_measure_norm_gt, Ordinal.sup_eq_lsub_or_sup_succ_eq_lsub, Cardinal.iInf_eq_zero_iff, CategoryTheory.ObjectProperty.instIsTriangulatedMinOfIsClosedUnderIsomorphisms, MeasureTheory.measure_iUnion_eq_iSup_accumulate, lowerSemicontinuousAt_iSup, Cardinal.lift_iSup_le_iff, Cardinal.sum_pow_eq_max_aleph0, Monotone.linearGrowthSup_nonneg, ENNReal.hasProd_iInf_prod, Pi.Colex.sInf_apply, ENat.iInf_eq_zero, Metric.ediam_iUnion_mem_option, Monotone.linearGrowthSup_comp_mul, MeasureTheory.limsup_measure_le_of_le_liminf_measure_compl, Filter.cardinalInterFilter_inf, ZFSet.rank_pair, Monotone.le_linearGrowthSup_comp, ExpGrowth.expGrowthSup_sup, Order.coheight_eq, Ordinal.IsPrincipal.sSup, Cardinal.aleph_limit, Monotone.map_sSup_of_continuousAt, EReal.liminf_add_gt_of_gt, Topology.IsLower.isTopologicalSpace_basis, bsupr_limsup_dimH, ENNReal.limsup_const_sub, ENNReal.add_iInf₂, Cardinal.mul_eq_max', MeasureTheory.iSup_lintegral_le, Pi.Lex.le_sSup_apply, upperSemicontinuousAt_iInf, upperSemicontinuousWithinAt_iInf, MeasureTheory.OuterMeasure.biInf_apply', CategoryTheory.ObjectProperty.instIsStableUnderShiftISupShiftOfIsClosedUnderIsomorphisms, Finset.Nonempty.ciSup_eq_max'_image, ENNReal.le_limsup_mul, Ordinal.iSup_le_iSup_add_one, Ordinal.iSup_le_iff, Cardinal.iSup_lt_ord_of_isRegular, Ordinal.iSup_eq_lsub, csInf_le_csInf', Ordinal.max_zero_right, ENNReal.limsup_add_le, IsTranscendenceBasis.lift_cardinalMk_eq_max_lift, IsTranscendenceBasis.lift_rank_eq_max_lift, MvRatFunc.rank_eq_max_lift, MeasureTheory.lintegral_liminf_le', Monotone.linearGrowthSup_comp, Ordinal.iSup_add_one_le, MeasureTheory.OuterMeasure.iSup_apply, ENNReal.iSup_mul, cauchy_davenport_minOrder_mul, Ordinal.iSup_eq_lsub_iff, lowerSemicontinuousWithinAt_biSup, ENat.sSup_eq_zero', ENat.le_iInf₂_add_iInf₂, MvPolynomial.cardinalMk_le_max, Cardinal.ciSup_add_ciSup, ENNReal.limsup_sub_const, ENNReal.inv_liminf, NNReal.agm_eq_ciInf, Cardinal.mk_freeCommRing, ENNReal.finsetSum_iSup, MeasureTheory.isTightMeasureSet_range_iff_tendsto_limsup_measure_norm_gt, Pi.Lex.sSup_apply, Ordinal.cof_iSup_add_one, Ordinal.iSup_natCast, lowerSemicontinuousAt_biSup, ENNReal.iInf_gt_eq_self, Cardinal.mk_freeAbelianGroup, ENNReal.eventually_le_limsup, ENNReal.inv_limsup, Ordinal.iSup_iterate_eq_nfp, EReal.limsup_add_bot_of_ne_top, ENat.biSup_add_biSup_le, lt_csSup_iff', Monotone.map_sInf_of_continuousAt, NNReal.toReal_liminf, Ordinal.lt_iSup_add_one_iff, MonoidAlgebra.cardinalMk_eq_max_lift_of_infinite', Set.einfsep_iUnion_mem_option, Set.chainHeight_eq_iSup, ENNReal.toNNReal_sInf, ENat.exists_eq_iSup₂_of_lt_top, exists_lt_of_lt_ciSup', HahnSeries.cardSupp_hsum_powers_le, Cardinal.add_le_max, MeasureTheory.OuterMeasure.trim_eq_iInf, ContinuousMap.enorm_eq_iSup_enorm, ENNReal.inv_sInf, ENNReal.coe_iInf, Ordinal.apply_omega0_of_isNormal, MeasureTheory.isTightMeasureSet_iff_tendsto_measure_compl_closedBall, ENat.iSup_add_iSup_le, Order.height_eq_iSup_last_eq, ENat.toENNReal_iInf, BoundedContinuousFunction.enorm_eq_iSup_enorm, ExpGrowth.expGrowthSup_iSup, Ordinal.card_opow_le, ENNReal.limsup_toReal_eq, dimH_def, NNReal.le_iInf_mul, Cardinal.mk_finsupp_lift_of_infinite', ciSup_mono', Order.coheight_eq_iSup_gt_coheight, LinearGrowth.linearGrowthSup_monotone, ModuleCat.projectiveDimension_eq_iSup_localizedModule_prime, NNReal.iSup_mul, MeasureTheory.IsStoppingTime.biInf, LinearGrowth.linearGrowthInf_le_linearGrowthSup_of_frequently_le, LinearGrowth.le_linearGrowthInf_comp, Ordinal.IsFundamentalSeq.iSup_add_one_eq, ENNReal.tprod_eq_iInf_prod, Ordinal.lsub_le_sup_succ, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_P, Antitone.map_sInf_of_continuousAt, MeasureTheory.AECover.iSup_lintegral_eq_of_countably_generated, MeasureTheory.OuterMeasure.ofFunction_apply, Cardinal.mul_le_max, CategoryTheory.ObjectProperty.shift_sup, ModuleCat.injectiveDimension_eq_iSup_localizedModule_maximal, ProbabilityTheory.bayesRisk_const', Order.IsSuccPrelimit.iSup_Iio, NNReal.iSup_pow, Ordinal.succ_iSup_le_lsub_iff, AddOreLocalization.cardinalMk_le_max, HahnSeries.cardSupp_inv_le, LinearGrowth.le_linearGrowthSup_iff, MeasureTheory.setLIntegral_iUnion_of_directed, MeasureTheory.lintegral_eq_iSup_eapprox_lintegral, ENNReal.coe_iSup, lt_ciSup_iff', isLUB_csSup', ENNReal.image_coe_uIcc, AddMonoidAlgebra.cardinalMk_of_infinite, FormalMultilinearSeries.radius_eq_liminf, Ordinal.IsNormal.apply_of_isSuccLimit, ENNReal.iInf_div', ENNReal.limsup_add_of_left_tendsto_zero, Ordinal.lsub_sum, Ordinal.iSup_lt_ord, EReal.liminf_const_mul_of_nonneg_of_ne_top, ENat.add_biSup', EReal.limsup_const_mul_of_nonpos_of_ne_bot, ENNReal.essSup_eq_zero_iff, lowerSemicontinuousOn_iff_le_liminf, EReal.limsup_add_le_of_le, Ordinal.cof_iSup_le, MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto, FreeAlgebra.cardinalMk_eq_max, ENNReal.ae_le_essSup, ZFSet.rank_union, ENat.biSup_add, ENNReal.iInf_coe_eq_top, ENNReal.iSup₂_pow_of_ne_zero, Cardinal.mk_iUnion_le, exists_eq_ciSup_of_not_isSuccPrelimit', ENat.iInf₂_add, Ordinal.preOmega_max, MonotoneOn.map_sSup_of_continuousWithinAt, Cardinal.iSup_le_sum, Order.krullDim_le_of_krullDim_preimage_le', CategoryTheory.ObjectProperty.shift_iSup, Cardinal.add_eq_right_iff, SimpleGraph.eccent_def, Cardinal.iSup_mk_le_mk_iUnion, iSup_limsup_dimH, LinearGrowth.le_linearGrowthInf_add, ZFSet.iSup_card_le_card_iUnion, Ordinal.card_iSup_le_sum_card, Cardinal.mk_finsupp_of_infinite', MvPolynomial.cardinalMk_eq_max_lift, UpperSemicontinuous.limsup_le, Cardinal.ciSup_add, Ordinal.iSup_lt, ENNReal.coe_sInf, MeasureTheory.iInf_mul_le_setLIntegral, MeasureTheory.measure_sigmaFiniteSetGE_ge, ContinuousMap.edist_eq_iSup, FirstOrder.Language.Substructure.lift_card_closure_le, ENat.iSup_coe_lt_top, Metric.infEDist_biUnion, PSet.rank_pair, EReal.limsup_add_le, analyticOrderAt_add_of_ne, NNReal.iSup_mul_le, egauge_pi', MeasureTheory.OuterMeasure.iSup_sInfGen_nonempty, FreeAlgebra.cardinalMk_eq_max_lift, ENNReal.toReal_iSup, Cardinal.sum_eq_iSup_of_lift_mk_le_iSup, NNReal.iInf_const_zero, lowerSemicontinuous_biSup, sSup_mem_closure, Ordinal.IsFundamentalSeq.iSup_eq, WithTop.coe_sInf, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.sup_P, ENat.sSup_mem_of_nonempty_of_lt_top, IsUltrametricDist.nnnorm_tsum_le, ENNReal.add_biSup, Metric.ediam_insert, MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm', LinearMap.lift_rank_comp_le, PiLp.nndist_eq_iSup, MvPolynomial.cardinalMk_eq_max, Ordinal.sInf_empty, Frequently.le_linearGrowthSup, Ordinal.sup_typein_succ, exists_eq_iSup_of_not_isSuccPrelimit, MeasureTheory.Measure.iSup_restrict_spanningSets_of_measurableSet, MeasureTheory.lintegral_le_iSup, Algebraic.cardinalMk_lift_le_max, FirstOrder.Language.BoundedFormula.card_le, MeasureTheory.le_measure_liminf_of_limsup_measure_compl_le, SimpleGraph.radius_eq_iInf_iSup_edist, ENNReal.mul_iSup, Algebra.rank_adjoin_le, EMetric.diam_iUnion_mem_option, LinearGrowth.linearGrowthInf_neg, NNReal.coe_sInf, Monotone.le_expGrowthSup_comp, ENNReal.toReal_sInf, Ordinal.succ_lt_iSup_of_ne_iSup
toOrderBot 📖	CompOp	16 math math: MeasureTheory.hittingAfter_bot_le_iff, MeasureTheory.lowerCrossingTime_le, Finset.sup_univ_eq_ciSup, MeasureTheory.upperCrossingTime_mono, MeasureTheory.hittingBtwn_bot_le_iff, MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, csSup_empty, ciSup_of_empty, MeasureTheory.hitting_bot_le_iff, MeasureTheory.upperCrossingTime_zero', MeasureTheory.lowerCrossingTime_mono, MeasureTheory.upperCrossingTime_le, csSup_empty, MeasureTheory.StronglyAdapted.isStoppingTime_leastGE, ciSup_false

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
csSup_empty 📖	mathematical	—	SupSet.sSup ConditionallyCompleteLattice.toSupSet ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice toConditionallyCompleteLinearOrder Set Set.instEmptyCollection Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice toOrderBot	—	—

WellFoundedLT

Definitions

Name	Category	Theorems
conditionallyCompleteLinearOrderBot 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
ConditionallyCompleteLattice 📖	CompData	—
ConditionallyCompleteLinearOrder 📖	CompData	—
ConditionallyCompleteLinearOrderBot 📖	CompData	—
conditionallyCompleteLatticeOfLatticeOfsInf 📖	CompOp	—
conditionallyCompleteLatticeOfLatticeOfsSup 📖	CompOp	—
conditionallyCompleteLatticeOfsInf 📖	CompOp	—
conditionallyCompleteLatticeOfsSup 📖	CompOp	—

---

← Back to Index