Basic

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

Statistics

Metric	Count
Definitions toConditionallyCompleteLattice, toConditionallyCompleteLinearOrderBot, toConditionallyCompletePartialOrder, toLinearOrder, instConditionallyCompleteLattice, instConditionallyCompleteLinearOrder, conditionallyCompleteLattice, completeLattice, completeLinearOrder, conditionallyCompleteLattice, instInfSet, instSupSet, completeLattice, completeLinearOrder, conditionallyCompleteLattice, instCompleteLinearOrder, instInfSet, instSupSet, instCompleteLatticeWithBot	19
Theorems sInf_image_Icc, sSup_image_Icc, csInf_eq, csSup_eq, csInf_image_le, csSup_image_le, le_csInf_image, le_csSup_image, map_csInf, csInf_eq_of_subset_of_forall_exists_le, csSup_eq_of_subset_of_forall_exists_le, map_csInf, sInf_image_Icc, sSup_image_Icc, coe_sInf', coe_sSup', sInf_empty, sInf_eq, sSup_empty, sSup_eq, coe_sInf, coe_sInf', coe_sSup, coe_sSup', isGLB_sInf, isGLB_sInf', isLUB_sSup, isLUB_sSup', sInf_empty, sInf_eq, sSup_eq, ciInf_eq_univ_of_not_bddBelow, ciInf_of_not_bddBelow, ciSup_eq_univ_of_not_bddAbove, ciSup_of_not_bddAbove, csInf_Ioc, csInf_Ioi, csInf_Ioo, csInf_eq_bot_of_bot_mem, csInf_eq_csInf_of_forall_exists_le, csInf_eq_of_forall_ge_of_forall_gt_exists_lt, csInf_eq_univ_of_not_bddBelow, csInf_image2_eq_csInf_csInf, csInf_image2_eq_csInf_csSup, csInf_image2_eq_csSup_csInf, csInf_image2_eq_csSup_csSup, csInf_insert, csInf_le, csInf_le', csInf_le_csInf, csInf_le_csInf', csInf_le_csSup, csInf_le_iff, csInf_le_of_le, csInf_lt_iff, csInf_lt_of_lt, csInf_mem, csInf_of_not_bddBelow, csInf_pair, csInf_union, csInf_univ, csInf_upperBounds_eq_csSup, csInf_upperBounds_range, csSup_Ico, csSup_Iio, csSup_Ioo, csSup_empty, csSup_eq_csSup_of_forall_exists_le, csSup_eq_of_forall_le_of_forall_lt_exists_gt, csSup_eq_of_is_forall_le_of_forall_le_imp_ge, csSup_eq_top_of_top_mem, csSup_eq_univ_of_not_bddAbove, csSup_image2_eq_csInf_csInf, csSup_image2_eq_csInf_csSup, csSup_image2_eq_csSup_csInf, csSup_image2_eq_csSup_csSup, csSup_insert, csSup_inter_le, csSup_le, csSup_le', csSup_le_csSup, csSup_le_csSup', csSup_le_iff, csSup_le_iff', csSup_lowerBounds_eq_csInf, csSup_lowerBounds_range, csSup_of_not_bddAbove, csSup_pair, csSup_union, exists_between_of_forall_le, exists_lt_of_csInf_lt, exists_lt_of_lt_csSup, exists_lt_of_lt_csSup', isGLB_csInf, isLUB_csSup, isLUB_csSup', isLeast_csInf, le_csInf, le_csInf_iff, le_csInf_iff', le_csInf_iff'', le_csInf_inter, le_csSup, le_csSup_iff, le_csSup_iff', le_csSup_of_le, lt_csSup_iff, lt_csSup_iff', lt_csSup_of_lt, notMem_of_csSup_lt, notMem_of_lt_csInf, notMem_of_lt_csInf', sInf_eq_argmin_on, sInf_iUnion_Ici, sSup_iUnion_Iic, subset_Icc_csInf_csSup	116
Total	135

AntitoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sInf_image_Icc 📖	mathematical	Preorder.toLE AntitoneOn PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Icc	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.image	—	Set.Icc_toDual MonotoneOn.sInf_image_Icc dual_left
sSup_image_Icc 📖	mathematical	Preorder.toLE AntitoneOn PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Icc	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.image	—	MonotoneOn.sInf_image_Icc dual_right

CompleteLattice

Definitions

Name	Category	Theorems
toConditionallyCompleteLattice 📖	CompOp	1990 math math: BooleanSubalgebra.map_iSup, NonUnitalSubalgebra.coe_starClosure, continuousNeg_iInf, CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup, upperBounds_supClosure, MeasureTheory.Measure.MeasureDense.approx, Submodule.finrank_sup_add_finrank_inf_eq, Filter.bliminf_sup_le_or_aux_right, Set.Finite.t2_separation, TopCat.binaryCofan_isColimit_iff, dirSupClosed_iff_forall_sSup, Subalgebra.LinearDisjoint.inf_eq_bot, Nat.iInf_le_succ', LinearMap.quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, AlgebraicGeometry.descendsAlong_isOpenImmersion_surjective_inf_flat_inf_quasicompact', AffineSubspace.direction_inf, Metric.ball_disjoint_ball, MeasureTheory.OuterMeasure.map_iInf, OrderIso.map_radical, Set.Iic.coe_sInf, homotopyEquivalences_le_quasiIso, continuous_sInf_dom₂, PolynormableSpace.sInf, AffineSubspace.direction_sup_eq_sup_direction, OrderEmbedding.supIrredLowerSet_apply, AddSubmonoid.smul_iSup, StarSubalgebra.coe_sInf, isFullyInvariant_iff_sSup_isotypicComponents, continuous_sup_rng_right, essSup_le_of_ae_le, Nat.iSup_lt_succ', Submodule.supIndep_torsionBySet_ideal, GroupTopology.toTopologicalSpace_iInf, equicontinuousWithinAt_iInf_dom, Subgroup.sup_eq_closure_mul, FirstOrder.Language.Substructure.mem_sSup_of_directedOn, continuousMul_inf, TopCat.Sheaf.interUnionPullbackCone_snd, iSupIndep.injOn_iInf, IntermediateField.LinearDisjoint.iff_inf_eq_bot, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inter, IntermediateField.normal_inf, ContinuousMap.compactOpen_eq_iInf_induced, sInfHom.le_apply_bliminf, AlgebraicGeometry.descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact, LinearMap.map_le_map_iff, ProbabilityTheory.measure_limsup_eq_one, Filter.bliminf_congr', IntermediateField.sSup_toSubfield, Algebra.mem_iInf, StarSubalgebra.map_inf, MulAction.IwasawaStructure.is_generator, RootPairing.instNontrivialSubtypeSubmoduleMemSublatticeInvtRootSubmodule, AlgebraicGeometry.iSup_affineOpens_eq_top, Subalgebra.coe_iSup_of_directed, AlgebraicGeometry.RingedSpace.basicOpen_res, nhds_sInf, Finpartition.isPartition_parts, Filter.sdiff_limsup, Antitone.Icc, continuousMul_sInf, TopologicalSpace.Closeds.iInf_def, Subfield.mem_sSup_of_directedOn, AddGroupTopology.toTopologicalSpace_inf, setOf_isOpen_iSup, isClosed_iSup_iff, Filter.bliminf_sup_le_and_aux_right, SeparatedNhds.disjoint, topologicalGroup_iInf, eq_sInf_coatoms, MeasureTheory.liminf_ae_eq_of_forall_ae_eq, IntermediateField.extendScalars_sup, TopologicalSpace.Opens.coe_iSup, Submodule.toConvexCone_inf, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app, IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot, TopCat.Presheaf.coveringOfPresieve.iSup_eq_of_mem_grothendieck, disjoint_or_subset_of_isClopen, FirstOrder.Language.Substructure.mem_iSup_of_directed, Module.End.mem_invtSubmodule, Subalgebra.LinearDisjoint.sup_free_of_free, Matrix.iSup_eigenspace_toLin'_diagonal_eq_top, NonUnitalStarAlgebra.mem_sup_right, AffineSubspace.direction_inf_of_mem, continuous_sup_dom, SSet.modelCategoryQuillen.I_le_monomorphisms, IntermediateField.relrank_comap_comap_eq_relrank_inf, supClosure_eq_self, MonotoneOn.Icc, Filter.bliminf_inf_not, Filter.blimsup_and_le_inf, StarSubalgebra.mem_sup_left, MeasureTheory.measureReal_symmDiff_le, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_W, Set.Icc.coe_sSup, RootPairing.Base.forall_mem_support_invtSubmodule_iff, LinearMap.IsProj.mem_invtSubmodule_iff, Submodule.mem_sup', Filter.liminf_const_top, MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt, Disjoint.of_span₀, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup, MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_disjointOfDiff, LieSubmodule.iSup_toSubmodule, MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetRing, R1Space.iInf, antitone_continuousOn, isSublattice_latticeClosure, ProbabilityTheory.condIndep_iSup_of_antitone, IntermediateField.isPurelyInseparable_iSup, AlgebraicGeometry.IsAffineOpen.iSup_of_disjoint, strictMono_nhdsSet, Filter.bliminf_sup_le_and_aux_left, SSet.iSup_subcomplexOfSimplex_prod_eq_top, nhds_iInf, TopologicalSpace.Opens.mem_sup, LinearMap.IsIdempotentElem.commute_iff, LinearPMap.domain_supSpanSingleton, continuous_sSup_dom, Ideal.sum_eq_sup, CompleteLatticeHom.apply_limsup_iterate, Monotone.Ici, Subalgebra.comap_map_eq, Subalgebra.finrank_sup_eq_finrank_right_mul_finrank_of_free, CategoryTheory.MorphismProperty.HasCardinalLT.iSup, AddMonoidHom.noncommPiCoprod_range, Subalgebra.op_sSup, Opens.pretopology_toGrothendieck, isClosed_sSup_iff, iSupIndep.disjoint_biSup, Finset.ordConnected_range_coe, AffineSubspace.mem_sInf_iff, CompleteSublattice.isComplemented_iff, AntitoneOn.Ici, AlgebraicGeometry.IsAffineOpen.isCompact_pullback_inf, Submodule.isOrtho_sup_right, SSet.finite_iSup_iff, Submodule.map₂_iSup_right, inf_mem_infClosure, OrderEmbedding.infIrredUpperSet_surjective, induced_inf, latticeClosure_univ, ClosedSubmodule.toSubmodule_sup, monotone_hausdorffEntourage, GroupTopology.toTopologicalSpace_inf, Submodule.fst_sup_snd, Ideal.mem_sSup_of_mem, IsCompactlyGenerated.BooleanGenerators.sSup_inter, NonUnitalAlgebra.mem_sup_left, FirstOrder.Language.Substructure.map_sup, IsCompactlyGenerated.BooleanGenerators.isAtom, DualNumber.range_lift, NFA.pumping_lemma, NonUnitalAlgebra.coe_inf, ProbabilityTheory.Kernel.indep_iSup_directed_limsup, TopologicalSpace.eq_induced_by_maps_to_sierpinski, LocallyConvexSpace.inf, Set.indicator_iUnion_apply, ProbabilityTheory.indep_iSup_of_monotone, SeparatedNhds.disjoint_closure_left, LinearEquiv.map_mem_invtSubmodule_conj_iff, ProbabilityTheory.indep_limsup_atTop_self, IntermediateField.coe_iSup_of_directed, Submodule.map_iSup, Submodule.mem_iSup_iff_exists_finsupp, Subalgebra.op_sInf, Filter.Realizer.map_F, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMax, StarSubalgebra.inf_toSubalgebra, ClosedSubmodule.coe_sSup, IsUltrametricDist.ball_subset_trichotomy, ConvexCone.coe_inf, Algebra.sSup_def, continuousVAdd_sInf, BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff, isGLB_infClosure, Monotone.Ioo, Submodule.mem_invtSubmodule_reflection_of_mem, SimpleGraph.ComponentCompl.disjoint_right, 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, Algebra.mem_sInf, EMetric.ball_disjoint, Topology.IsLower.toContinuousInf, generateFrom_sUnion, Subalgebra.centralizer_coe_iSup, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin_1, continuous_inf_dom_left₂, BoxIntegral.Box.disjoint_withBotCoe, Antitone.pairwise_disjoint_on_Ioc_pred, Function.sSup_div_semiconj, AlgebraicGeometry.isPullback_opens_inf, WellFoundedGT.iSup_eq_monotonicSequenceLimit, LieSubalgebra.span_union, ENNReal.iInf_ennreal, IsCompact.separation_of_notMem, Subalgebra.rank_sup_eq_rank_left_mul_rank_of_free, Finset.isWF_sup, IsSublattice.latticeClosure_eq, DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, CategoryTheory.GrothendieckTopology.monotone_close, Sublocale.coe_iInf, Submodule.coe_sup, OrderIso.essSup_apply, NonUnitalAlgebra.sInf_toNonUnitalSubsemiring, ProbabilityTheory.condIndep_iSup_of_monotone, TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul, Subfield.map_sup, biUnion_range_succ_disjointed, Submodule.iSup_map_single_le, AddSubgroup.add_normal, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal, AlgebraicGeometry.isImmersion_eq_inf, wellFoundedGT_iff_isSupFiniteCompact, Subgroup.mul_normal, LinearMap.iSup_range_single, NonUnitalStarAlgebra.mem_sInf, Ideal.comap_finsetInf, TopologicalSpace.Opens.iSup_mk, Submodule.colon_finsetInf, AddSubmonoid.iSup_map_single, iSupIndep.pairwiseDisjoint, AlgebraicGeometry.Scheme.IdealSheafData.support_mul, LinearMap.eventually_iSup_ker_pow_eq, Subfield.coe_iSup_of_directed, Representation.invtSubmodule.nontrivial_iff, Nat.iInf_lt_succ', TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one, BoxIntegral.Box.Ioo_subset_coe, generateFrom_iUnion_isOpen, MeasureTheory.measure_liminf_cofinite_eq_zero, TopologicalSpace.Closeds.coe_iInf, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom, Filter.bliminf_antitone, Subgroup.coe_mul_of_left_le_normalizer_right, AlgebraicGeometry.descendsAlong_isomorphisms_surjective_inf_flat_inf_quasicompact, NumberField.isTotallyReal_sup, continuousAdd_inf, Algebra.map_sup, SummationFilter.support_eq_limsInf, separated_by_continuous, Submodule.smul_iSup', CategoryTheory.GrothendieckTopology.arrow_intersect, Antitone.pairwise_disjoint_on_Ioo_pred, AddSubmonoid.sup_mul, MeasurableSpace.measurableSet_iInf, CategoryTheory.GrothendieckTopology.intersection_covering_iff, IntermediateField.coe_iInf, MeasureTheory.OuterMeasure.comap_iInf, continuous_inf_dom_right₂, TopCat.Sheaf.interUnionPullbackCone_fst, Filter.liminf_eq_iSup_iInf_of_nat', Module.End.mem_invtSubmodule_iff_mapsTo, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_transfiniteCompositions, NonUnitalSubalgebra.prod_inf_prod, AlgebraicGeometry.IsSeparated.eq_valuativeCriterion, generateFrom_union, SimpleGraph.ComponentCompl.pairwise_disjoint, Filter.limsup_compl, iSup_partialSups_eq, isFiniteLength_iff_exists_compositionSeries, isOpen_sup, Sylow.normalizer_sup_eq_top', MeasurableSpace.measurableSet_sSup, NonUnitalAlgebra.mem_sup_right, Subalgebra.unop_sup, Submodule.biSup_comap_subtype_eq_top, Filter.HasBasis.limsInf_eq_iSup_sInf, Subgroup.FG.biSup, AddGroupTopology.toTopologicalSpace_sInf, AlgebraicGeometry.IsClosedImmersion.eq_proper_inf_monomorphisms, LinearMap.range_domRestrict_eq_range_iff, disjoint_nested_nhds_of_not_inseparable, Order.succ_eq_iInf, Submodule.biSup_eq_range_dfinsupp_lsum, Algebra.adjoin_attach_biUnion, TopologicalSpace.Closeds.instContinuousSup, Set.mulIndicator_iUnion_apply, Filter.bliminf_eq_iSup_biInf_of_nat, Subalgebra.prod_inf_prod, Submodule.comap_map_sup_of_comap_le, TopCat.pullback_topology, LinearMap.span_singleton_sup_orthogonal_eq_top, exists_disjoint_vadd_of_isCompact, IntermediateField.inf_toSubalgebra, OrderIso.infIrredUpperSet_symm_apply, AntitoneOn.Icc, Projectivization.Subspace.span_sup, MeasureTheory.measureReal_symmDiff_eq, IsSemisimpleModule.toComplementedLattice, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, FirstOrder.Language.Substructure.map_sup_comap_of_surjective, ProbabilityTheory.Kernel.indep_limsup_atBot_self, sSupIndep.pairwiseDisjoint, Submodule.fg_biSup, TopologicalSpace.NoetherianSpace.exists_finset_irreducible, UniformContinuous.sup_closeds, generateFrom_iInter_of_generateFrom_eq_self, Disjoint.of_span, CategoryTheory.MorphismProperty.IsLocalAtSource.inf, NonUnitalAlgebra.mem_inf, sSup_atoms_le_eq, AddSubgroup.noncommPiCoprod_range, LinearMap.iInf_ker_proj_le_iSup_range_single, essSup_map_measure, NonUnitalStarAlgebra.iInf_toNonUnitalSubalgebra, AddSubmonoid.smul_sup, SSet.Subcomplex.degenerate_eq_top_iff, TopologicalSpace.Closeds.gc, isEmbedding_sumElim, NonUnitalStarAlgebra.coe_sInf, Ideal.smul_sup, IntermediateField.finiteDimensional_iSup_of_finset, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, MonotoneOn.Iio, AffineSubspace.span_iUnion, CategoryTheory.Sieve.overEquiv_le_overEquiv_iff, Ideal.isPrimary_finsetInf, SSet.iSup_skeleton, FirstOrder.Language.Substructure.comap_sup_map_of_injective, disjoint_interior_frontier, PrimeSpectrum.iSup_basicOpen_eq_top_iff, blimsup_thickening_mul_ae_eq_aux, IsNormalClosure.adjoin_rootSet, Submodule.annihilator_iSup, Subfield.closure_iUnion, Filter.Realizer.ne_bot_iff, ENNReal.iSup_ne_top, antitone_Ioi, Submodule.neg_sup, TopCat.colimit_topology, Submodule.sup_eq_range, topologicalGroup_inf, Pi.induced_restrict, Set.Finite.infClosure, MeasureTheory.OuterMeasure.iInf_apply', ofDual_preimage_latticeClosure, Submodule.neg_iSup, Submodule.sub_mem_sup, MeasureTheory.IsSetSemiring.disjointOfUnion_props, Filter.inf_limsup, Algebra.adjoin_union, ProbabilityTheory.indep_biSup_limsup, MeasureTheory.Measure.sInf_caratheodory, topologicalAddGroup_inf, Ideal.Filtration.sSup_N, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, Ideal.mem_sup_left, Monoid.CoprodI.mrange_eq_iSup, MeasureTheory.Measure.QuasiMeasurePreserving.liminf_preimage_iterate_ae_eq, SSet.Subcomplex.preimage_min, AlgebraicGeometry.Scheme.Hom.image_iSup₂, Algebra.coe_iInf, Ideal.prod_le_inf, Finset.coe_wcovBy_coe, MeasureTheory.OuterMeasure.restrict_iInf, MeasureTheory.OuterMeasure.le_sum_caratheodory, Submodule.mem_finset_inf, isNoetherian_iSup, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app, essInf_measure_zero, AddSubgroup.relIndex_map_map, CompleteSublattice.coe_iInf, ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule, Ideal.iSup_eq_span, AffineSubspace.direction_affineSpan_insert, 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, normalClosure_eq_iSup_adjoin', MeasurableEmbedding.essSup_map_measure, IntermediateField.iInf_toSubfield, sSup_isotypicComponents, Antitone.Ico, continuousNeg_sInf, MeasureTheory.OuterMeasure.map_iInf_comap, Monotone.pairwise_disjoint_on_Ioc_pred, MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff', PrimeSpectrum.basicOpen_mul, continuous_sSup_rng, CategoryTheory.Pretopology.mem_toGrothendieck, Antitone.pairwise_disjoint_on_Ioo_succ, MeasurableSpace.generateFrom_iUnion_measurableSet, ProbabilityTheory.Kernel.indep_iSup_limsup, Submodule.submodule_eq_sSup_le_nonzero_spans, εNFA.pumping_lemma, Submodule.smul_sup', HahnEmbedding.ArchimedeanStrata.ball_sup_stratum_eq, continuousNeg_inf, IntermediateField.sup_toSubalgebra_of_isAlgebraic_left, TopCat.prod_topology, Subrepresentation.toSubmodule_sup, ProbabilityTheory.indep_iSup_of_directed_le, latticeClosure_mono, IntermediateField.restrictScalars_sup, image_latticeClosure', Submodule.finiteDimensional_finset_sup, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin, Submodule.submoduleOf_sup_of_le, IsFoelner.tendsto_meas_smul_symmDiff, AffineSubspace.affineSpan_eq_sInf, AlgebraicGeometry.Scheme.Hom.preimage_iSup, Filter.cofinite.limsup_set_eq, MeasurableSpace.generateFrom_sup_generateFrom, OrderIso.supIrredLowerSet_symm_apply, ProbabilityTheory.condIndep_limsup_atTop_self, Submonoid.sup_eq_closure_mul, Submodule.iSup_mul, regularSpace_sInf, Ideal.IsPrime.inf_le', Submodule.localized'_iSup, Algebra.sInf_toSubsemiring, Algebra.sInf_toSubmodule, LinearMap.isCompl_iSup_ker_pow_iInf_range_pow, HomogeneousIdeal.toIdeal_iSup₂, Representation.invtSubmodule.coe_top, upperHemicontinuousWithinAt_iff_preimage_Iic, topologicalAddGroup_sInf, MeasureTheory.OuterMeasure.trim_sup, TopologicalSpace.Opens.mem_inf, Set.definable_finset_sup, AddSubgroup.relIndex_sup_left, MeasureTheory.Content.innerContent_iSup_nat, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso, MeasureTheory.IsSetSemiring.isSetRing_supClosure, Nucleus.mem_toSublocale, Partition.pairwiseDisjoint, Filter.bliminf_sup_le_or_aux_left, AlgebraicGeometry.instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget, TopologicalSpace.IsTopologicalBasis.inf_induced, Submodule.finiteDimensional_sup, Submodule.dualCoannihilator_iSup_eq, LinearMap.map_coprod_prod, AlgebraicGeometry.HasAffineProperty.affineAnd_eq_of_propertyIsLocal, continuous_iInf_rng, Antitone.Ioc, AlgebraicGeometry.Etale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified, LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, Subgroup.FG.finset_sup, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le, MeasureTheory.Measure.MeasureDense.fin_meas_approx, Submodule.span_attach_biUnion, NonarchimedeanGroup.exists_openSubgroup_separating, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top', MeasureTheory.edist_indicatorConstLp_eq_enorm, Subfield.extendScalars_inf, AlgebraicGeometry.IsFinite.eq_proper_inf_locallyQuasiFinite, ProbabilityTheory.Kernel.indep_limsup_self, blimsup_cthickening_ae_le_of_eventually_mul_le_aux, Subalgebra.LinearDisjoint.rank_sup_of_free, CompleteAtomicBooleanAlgebra.instIsCoatomistic, Ideal.mul_left_self_sup, StarSubalgebra.mul_mem_sup, iSupIndep_pair, Submodule.comap_iSup_map_of_injective, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app, Submodule.map₂_iSup_left, CompleteSublattice.coe_sInf', LinearMap.iSup_range_single_eq_iInf_ker_proj, NonUnitalAlgebra.mem_iInf, Ctop.Realizer.nhds_F, lowerHemicontinuous_iff_isOpen_compl_preimage_Iic_compl, MeasureTheory.IsSetSemiring.mem_supClosure_iff, Algebra.TensorProduct.map_ker, SupClosed.infClosure, Submodule.map_sup, MeasurableSpace.map_inf, disjoint_nhdsSet_principal, BoxIntegral.Box.iUnion_Ioo_of_tendsto, t2_separation_nhds, AffineSubspace.mem_iInf_iff, sInf_sub, continuousInv_inf, NonUnitalAlgebra.mul_mem_sup, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_monotone, sSup_compact_eq_top, Setoid.IsPartition.finpartition_parts, iSupIndep.supIndep', MonotoneOn.Ici, TopologicalSpace.Closeds.mem_sInf, Filter.bliminf_or_le_inf, Ideal.isPrimary_finset_inf, IntermediateField.normal_iSup, iSupIndep.supIndep, Subalgebra.op_inf, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom, LinearMap.comap_leq_ker_subToSupQuotient, ProbabilityTheory.condExpKernel_ae_eq_condExp', LieModule.coe_genWeightSpaceOf_zero, essSup_map_measure_of_measurable, CompleteSublattice.sInfClosed, Submodule.map_mkQ_eq_top, CategoryTheory.GrothendieckTopology.closureOperator_isClosed, IntermediateField.isCyclotomicExtension_lcm_sup, Submodule.eq_top_of_disjoint, infClosed_infClosure, IntermediateField.sup_toSubalgebra_of_isAlgebraic, Submodule.isOrtho_sSup_right, sInfHom.continuous, Submodule.iSup_span, essSup_const_bot, Module.End.invtSubmodule.isCompl_iff, AddSubmonoid.neg_sup, MeasureTheory.measure_symmDiff_le, Sublocale.sInf_mem, Filter.bliminf_or_eq_inf, CategoryTheory.GrothendieckTopology.PreservesSheafification.le, AffineSubspace.inf_coe, AlgebraicGeometry.IsLocalIso.eq_iInf, Filter.limsup_sup_filter, continuous_inf_dom_right, AffineSubspace.map_inf_eq, AddSubmonoid.FG.iSup, Submonoid.smul_sup, TopCat.Presheaf.SheafConditionEqualizerProducts.w, isCompactElement_iff_exists_le_iSup_of_le_iSup, MeasureTheory.dense_of_generateFrom_isSetSemiring, AffineSubspace.span_union, NonarchimedeanAddGroup.exists_openAddSubgroup_separating, TopologicalSpace.Clopens.coe_disjoint, essInf_count, LinearMap.quotientInfEquivSupQuotient_apply_mk, Sublocale.coe_inf, AffineSubspace.coe_inf, Module.End.iSup_genEigenspace_eq, Set.isCoatom_iff, Monotone.Iio, AddSubmonoid.mul_iSup, IntermediateField.sInf_toSubalgebra, sSup_inv, Submodule.iSup_dualAnnihilator_le_iInf, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc, OrderEmbedding.infIrredUpperSet_apply, Subgroup.FG.biSup_finset, essInf_antitone_measure, MeasureTheory.measure_neg_vadd_symmDiff, supClosure_empty, Algebra.map_inf, ClosedSubmodule.toSubmodule_iSup, BooleanSubalgebra.sSup_mem, Submodule.sum_mem_iSup, IsRetrocompact.finsetInf', sSup_mul, blimsup_cthickening_ae_le_of_eventually_mul_le, IntermediateField.fg_sup, Submonoid.FG.finset_sup, isInducing_sumElim, BoxIntegral.Box.Ioo_ae_eq_Icc, IntermediateField.inf_relfinrank_right, Submodule.mem_iSup_iff_exists_dfinsupp, isOpen_sSup_iff, LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute, compl_image_latticeClosure, Submodule.span_range_eq_iSup, Order.Ideal.PrimePair.isCompl_I_F, Algebra.sup_toSubsemiring, LowerSet.supIrred_iff_of_finite, TopologicalSpace.Opens.gc, AddSubgroup.coe_add_of_left_le_normalizer_right, IntermediateField.sSup_def, MeasureTheory.OuterMeasure.map_iInf_le, Ideal.IsHomogeneous.iSup, Filter.cofinite.bliminf_set_eq, PrimitiveSpectrum.gc_closureOperator, beattySeq_symmDiff_beattySeq'_pos, Irrational.beattySeq_symmDiff_beattySeq_pos, AlgebraicGeometry.iSup_basicOpen_of_span_eq_top, upperHemicontinuousOn_iff_preimage_Iic, Affine.Simplex.mongePlane_def, Subalgebra.mem_starClosure, Submodule.iSup_eq_range_dfinsupp_lsum, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_W, Monoid.CoprodI.range_eq_iSup, sInf_mul, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, induced_sInf, sInf_neg, infClosure_singleton, Submodule.IsMinimalPrimaryDecomposition.inf_eq, MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq, ConvexCone.mem_inf, Opens.pretopology_ofGrothendieck, Partition.sSup_eq', Subalgebra.finrank_right_dvd_finrank_sup_of_free, DFinsupp.iSup_range_lsingle, Partition.le_of_mem, NumberField.Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, AlgebraicGeometry.Proj.basicOpen_mul, Submonoid.iSup_map_mulSingle, PrimeSpectrum.iInf_localization_eq_bot, HomogeneousIdeal.toIdeal_sSup, Subalgebra.mul_toSubmodule, IntermediateField.extendScalars_inf, Filter.liminf_sup_filter, Set.isAtom_singleton, Ideal.mul_sup, sInf_inv, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, TopCat.nonempty_isLimit_iff_eq_induced, Polynomial.sup_aeval_range_eq_top_of_isCoprime, TopologicalSpace.Opens.functor_obj_map_obj, MeasureTheory.OuterMeasure.iInf_apply, Filter.liminf_eq_sSup_sInf, OrthogonalFamily.isInternal_iff, Filter.limsup_sdiff, MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiffUnion, AddSubgroup.index_map, NonUnitalStarAlgebra.mem_iInf, Set.monotone_accumulate, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, IsSemisimpleModule.sup, Topology.IsInducing.disjoint_of_sumElim_aux, exists_compositionSeries_of_isNoetherian_isArtinian, SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf, latticeClosure_prod, CompletePseudometrizable.iInf, SequentialSpace.iSup, Finsupp.supported_union, CompleteLatticeHom.apply_liminf_iterate, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, separated_by_isOpenEmbedding, Subgroup.relIndex_map_map, Setoid.eqv_classes_disjoint, continuousInv_sInf, Monotone.Ico, Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime, InfClosed.infClosure_eq, TopologicalSpace.Closeds.lipschitz_sup, NumberField.isTotallyReal_iSup, MeasureTheory.measure_limsup_cofinite_eq_zero, UpperSet.infIrred_Ici, essInf_const_top, pullbackTopology_def, Submodule.mul_sup, RootPairing.invtRootSubmodule.top_mem, Filter.blimsup_eq_iInf_biSup, Sublattice.le_comap_iSup, iSupIndep_def'', Antitone.Iio, AlgebraicGeometry.Scheme.pretopology_le_inf, TopologicalSpace.secondCountableTopology_iInf, LinearMap.sup_range_inl_inr, Algebra.iSup_toSubsemiring, upperHemicontinuousAt_iff_preimage_Iic, LocallyConvexSpace.iInf, TopCat.Sheaf.existsUnique_gluing, LinearMap.span_singleton_sup_ker_eq_top, Nucleus.coe_toSublocale, exists_nhds_disjoint_closure, MeasureTheory.OuterMeasure.biInf_apply, Nat.iInf_le_succ, Seminorm.closedBall_finset_sup, Topology.IsGeneratedBy.sup, Submodule.isOrtho_iSup_left, Filter.blimsup_sup_not, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp, TopologicalSpace.Opens.coe_finset_sup, MeasureTheory.IsSetSemiring.diff_mem_supClosure, MeasureTheory.OuterMeasure.le_add_caratheodory, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt, continuousSMul_sInf, Topology.IsLocallyConstructible.finsetInf, TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.hom_ext_iff, Ideal.sup_mul_right_self, Submodule.comap_finsetInf, infClosure_eq_self, ProbabilityTheory.indep_iSup_limsup, AddSubmonoid.mem_bsupr_iff_exists_dfinsupp, generateFrom_iUnion, Submodule.comap_sup_map_of_injective, CategoryTheory.PreZeroHypercover.presieve₀_restrictIndex_le, normalClosure_def, MeasureTheory.Filtration.rightCont_apply, IntermediateField.lift_inf, tsum_iSup_decode₂, compl_image_latticeClosure_eq_of_compl_image_eq_self, Subalgebra.mulMap'_surjective, partialSups_eq_sUnion_image, AddSubgroup.closure_add_le, TopCat.Sheaf.interUnionPullbackConeLift_right, Submodule.coe_finsetInf, latticeClosure_singleton, Subgroup.relIndex_sup_right, Submodule.restrictScalars_sSup, MeasurableSpace.comap_prodMk, MeasureTheory.le_measure_symmDiff, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin_1, TopologicalSpace.Closeds.coe_finset_inf, coinduced_sSup, Module.End.invtSubmodule.one, MeasurableSpace.measurableSpace_iSup_eq, IntermediateField.coe_inf, LinearMap.mem_span_iff_continuous_of_finite, MeasurableSet.bihimp, CompleteSublattice.codisjoint_iff, PrimeSpectrum.zeroLocus_iSup, IntermediateField.restrictScalars_adjoin_eq_sup, Nucleus.toSublocale_le_toSublocale, AlgebraicGeometry.Scheme.basicOpen_add_le, iSupIndep_def', Submodule.toAddSubmonoid_sSup, IsPGroup.to_sup_of_normal_left', MeasureTheory.measure_symmDiff_inv_smul, Algebra.mem_sup_left, LinearMap.quotientInfEquivSupQuotient_injective, isSemisimpleModule_iff, IntermediateField.mem_inf, Submodule.smul_iSup, Submodule.dualAnnihilator_sup_eq, Submonoid.inv_sup, exists_open_nhds_disjoint_closure, instIsModularLatticeSubgroup, MeasureTheory.OuterMeasure.sup_apply, Sublattice.setLike_mem_inf, Subgroup.toSubmonoid_zpowers, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse, Subalgebra.finrank_left_dvd_finrank_sup_of_free, Set.Icc.coe_iInf, NumberField.Units.regOfFamily_div_regulator, disjoint_measurableAtom_of_notMem, AddSubgroup.ofAddUnits_sSup, MeasureTheory.disjoint_cylinder_iff, CompleteSublattice.isCompl_iff, AddSubmonoid.mul_sup, MonotoneOn.Iic, CategoryTheory.MorphismProperty.HasCardinalLT.sup, isAtomic_of_complementedLattice, Submodule.dualCoannihilator_sup_eq, QuotientAddGroup.comap_map_mk', Subalgebra.unop_sSup, OrderIso.supIrredLowerSet_apply, CategoryTheory.MorphismProperty.retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp, NFA.disjoint_evalFrom_reverse_iff, iSupIndep_iff_supIndep_of_injOn, Filter.bliminf_sup_le_inf_aux_left, AffineIndependent.inf_affineSpan_eq_affineSpan_inter, Subalgebra.mul_toSubmodule_le, AffineSubspace.direction_sup, UniformOnFun.topologicalSpace_eq, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv, AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated, infClosure_univ, Submodule.fg_iSup, SSet.skeleton_succ, MeasureTheory.Filtration.rightCont_def, sSup_atoms_eq_top, SSet.Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top, IsSemisimpleModule.finite_tfae, Sublattice.ext_mem_iff, TopologicalSpace.IsTopologicalBasis.inf, TopologicalSpace.Opens.coe_finset_inf, subset_latticeClosure, Filter.bliminf_sup_le_inf_aux_right, LinearPMap.domain_sSup, GroupTopology.toTopologicalSpace_sInf, AffineSubspace.direction_iInf_of_mem, continuousAdd_iInf, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion_of_mem, AddSubgroup.coe_add_of_right_le_normalizer_left, subset_infClosure, MeasureTheory.Measure.sInf_apply, regularSpace_iInf, Submodule.inf_iSup_genEigenspace, Sublocale.coe_sInf, complementedLattice_of_isAtomistic, RootPairing.corootSpan_mem_invtSubmodule_coreflection, Ideal.iSup_mul, FirstOrder.Language.ClosedUnder.inf, FirstOrder.Language.isExtensionPair_iff_exists_embedding_closure_singleton_sup, continuous_iSup_dom, R1Space.inf, NumberField.IsCMField.closure_realFundSystem_sup_torsion, disjoint_frontier_iff_isOpen, RootPairing.invtRootSubmodule.eq_bot_iff, Module.Basis.flag_succ, equicontinuous_iInf_dom, IntermediateField.LinearDisjoint.finrank_sup, MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion, IsGenericPoint.disjoint_iff, Sublattice.mem_subtype, isSupClosedCompact_iff_wellFoundedGT, AlgebraicGeometry.Scheme.grothendieckTopology_eq_inf, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot', MeasureTheory.Measure.inf_apply, Algebra.sSup_toSubsemiring, Module.End.isFinitelySemisimple_iff, generateFrom_iInter, generateFrom_piiUnionInter_measurableSet, Subgroup.FG.sup, MeasureTheory.IsSetSemiring.diff_eq_sUnion', sInf_one, ENNReal.iSup_ennreal, AntitoneOn.Ioi, Antitone.pairwise_disjoint_on_Ioc_succ, alexandrovDiscrete_iSup, IntermediateField.restrictScalars_inf, partialSups_eq_biSup, dist_mulIndicator, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.exists_oneHypercover, IsIntegrallyClosed.iInf, Submodule.fg_finset_sup, Algebra.TensorProduct.productMap_range, NonUnitalSubalgebra.coe_iSup_of_directed, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sup, Filter.Realizer.mem_sets, Sublocale.sInf_mem', NonUnitalAlgebra.map_sup, AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom, CompleteSublattice.coe_sSup', tprod_iSup_decode₂, exists_seq_infinite_isOpen_pairwise_disjoint, AddSubgroup.ofAddUnits_inf, InfiniteGalois.restrict_fixedField, ProbabilityTheory.condIndep_iSup_limsup, Order.pred_eq_sSup, Ideal.Filtration.sup_N, BooleanSubalgebra.latticeClosure_subset_closure, OpenAddSubgroup.toOpens_inf, isFoelner_iff, Antitone.Ioi, TopCat.Presheaf.IsSheaf.isSheafPreservesLimitPairwiseIntersections, TopologicalSpace.Opens.mem_iSup, Submodule.sup_smul, Subgroup.ofUnits_inf, Set.limsup_eq_tendsto_sum_indicator_atTop, IsUltrametricDist.ball_eq_or_disjoint, continuous_sInf_dom, 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, Ideal.mem_span_singleton_sup, LieSubmodule.sup_toSubmodule, Ideal.finset_inf_span_singleton, ProbabilityTheory.Kernel.indep_iSup_of_directed_le, KaehlerDifferential.kerTotal_map, Subfield.closure_sUnion, UniformSpace.toTopologicalSpace_sInf, Filter.liminf_compl, ProbabilityTheory.condExp_ae_eq_integral_condExpKernel', essSup_mono_measure, BooleanSubalgebra.closure_latticeClosure, essSup_eq_iSup, sSupHom.continuous, upperHemicontinuous_iff_isOpen_preimage_Iic, Subalgebra.unop_iInf, IsRetrocompact.finsetSup, NonUnitalAlgebra.coe_iInf, upperHemicontinuous_iff_preimage_Iic, Algebra.inf_toSubmodule, BoxIntegral.Prepartition.pairwiseDisjoint, Antitone.Ici, Filter.limsInf_top, IntermediateField.sup_def, IsPGroup.to_sup_of_normal_right, MeasurableSpace.CountablyGenerated.sup, ProbabilityTheory.Kernel.indep_iSup_of_monotone, VonNeumannAlgebra.IsIdempotentElem.mem_iff, TensorProduct.quotientTensorQuotientEquiv_apply_tmul_mk_tmul_mk, Metric.ball_disjoint_closedBall, mem_add_wellApproximable_iff, sSup_one, MeasureTheory.IsStoppingTime.measurableSpace_min, Filter.HasBasis.liminf_eq_iSup_iInf, Algebra.iInf_toSubsemiring, AntitoneOn.Iic, CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.le, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot, PolynormableSpace.iInf, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero, IntermediateField.finrank_sup_le, Set.Finite.supClosure, Ideal.iSup_iInf_eq_top_iff_pairwise, Set.Iic.coe_iInf, nhds_inf, Submodule.closure_coe_iSup_map_single, Ideal.map_sup_comap_of_surjective, Filter.liminf_sdiff, TopCat.coinduced_of_isColimit, Filter.Realizer.ofEquiv_F, MeasureTheory.Filtration.rightCont_eq_of_not_isMax, MeasurableSet.measurableSet_bliminf, topologicalGroup_sInf, MeasureTheory.tendsto_ae_condExp, ProbabilityTheory.indep_iSup_directed_limsup, DividedPowers.SubDPIdeal.sSup_carrier_def, TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompact, CauchyFilter.monotone_gen, Set.isCoatom_singleton_compl, OrderEmbedding.supIrredLowerSet_surjective, AddMonoidHom.noncommPiCoprod_mrange, separableClosure_inf_perfectClosure, Subgroup.normal_mul, IsSemisimpleModule.sSup_simples_le, Subalgebra.unop_inf, isOpen_iSup_iff, biUnion_Iic_disjointed, IsSupClosedCompact.wellFoundedGT, Submodule.sInf_orthogonal, CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition, Submonoid.inv_iSup, Filter.blimsup_congr', AlgebraicGeometry.HasRingHomProperty.inf, TopologicalSpace.Compacts.coe_finset_sup, NonUnitalStarAlgebra.mul_mem_sup, Ideal.map_sup, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_of_inj, FirstOrder.Language.Substructure.CG.sup, AffineSubspace.nonempty_sup_left, LinearMap.range_coprod, ProbabilityTheory.iSup_partitionFiltration_eq_generateFrom_range, Subalgebra.finrank_sup_eq_finrank_left_mul_finrank_of_free, connectedComponent_disjoint, Submodule.mul_iSup, Set.Iic.coe_biInf, Set.Iic.coe_sSup, AlgebraicGeometry.Scheme.IdealSheafData.support_iSup, TopCat.Presheaf.presieveOfCovering.indexOfHom_spec, Set.Icc.coe_sInf, Subalgebra.finrank_sup_le_of_free, Ideal.comap_map_quotientMk, Subfield.mem_iSup_of_directed, MeasureTheory.IsSetRing.partialSups_mem, sup_mem_supClosure, Subalgebra.starClosure_toSubalgebra, ProbabilityTheory.condIndep_biSup_limsup, sSupIndep.disjoint_sSup, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom, lowerBounds_infClosure, gc_nhdsKer_interior, StarSubalgebra.mem_iInf, Submodule.span_sSup, ProperlyDiscontinuousSMul.exists_nhds_disjoint_image, Submodule.comap_map_mkQ, OpenAddSubgroup.toAddSubgroup_sup, Submodule.iSup_eq_span, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, ProbabilityTheory.condIndep_limsup_self, Filter.liminf_eq_iSup_iInf_of_nat, ProbabilityTheory.condExpKernel_def, nndist_mulIndicator, MeasureTheory.eLpNorm_indicator_sub_indicator, SeparatedNhds.disjoint_closure_right, Set.Icc.coe_iSup, NonUnitalStarAlgebra.mem_sup_left, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π, Submodule.span_iUnion, isCoatomistic_iff, Filter.limsup_bot, monotone_Iio, supClosure_isClosed, LieSubmodule.sSup_toSubmodule, ProjectiveSpectrum.basicOpen_mul, Order.pred_eq_iSup, AlexandrovDiscrete.sup, Submodule.inf_orthogonal, Ideal.map_iSup_comap_of_surjective, AffineSubspace.direction_iInf, AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom, IntermediateField.relfinrank_inf_mul_relfinrank, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating.le, CategoryTheory.Presieve.le_of_factorsThru_sieve, Pi.induced_precomp, VonNeumannAlgebra.IsStarProjection.mem_iff, Set.isAtom_iff, Set.indicator_iInter_apply, essSup_measure_zero, Monotone.Ioc, Submodule.sum_mem_biSup, Matrix.ker_diagonal_toLin', TopologicalSpace.Closeds.coe_inf, Language.IsRegular.inf, IntermediateField.LinearDisjoint.inf_eq_bot, MeasureTheory.measure_liminf_atTop_eq_zero, AddSubmonoid.FG.biSup, Finset.coe_covBy_coe, AlgebraicGeometry.isOpenImmersion_eq_inf, ClosedSubmodule.mem_sup, FirstOrder.Language.Substructure.iSup_eq_closure, Submodule.IsMinimalPrimaryDecomposition.minimal, AlgebraicGeometry.Scheme.Hom.preimage_sup, UniformSpace.toTopologicalSpace_iInf, MeasurableSet.symmDiff, CompleteSublattice.coe_iSup, Nat.iInf_lt_succ, MeasurableSpace.comap_iSup, Subalgebra.finite_sup, ClosedSubmodule.mem_iSup, Subalgebra.op_iInf, Ideal.comap_map_of_surjective, AddSubgroup.FG.iSup, Filter.limsSup_eq_iInf_sSup, smul_iInf_le, IsSemisimpleModule.sSup_simples_eq_top, iSup_disjointed, AddSubmonoid.coe_sup, supClosure_singleton, TopCat.Sheaf.interUnionPullbackConeLift_left, Ideal.quotientInfEquivQuotientProd_snd, Module.End.genEigenspace_eq_iSup_genEigenspace_nat, 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, AlgebraicGeometry.Scheme.Hom.image_iSup, image_latticeClosure, Alexandrov.lowerCone_π_app, iSupIndep.sup_indep_univ, Subfield.map_iSup, latticeClosure_eq_self, AddSubgroup.ofAddUnits_iSup₂, Algebra.iInf_toSubmodule, IsDedekindDomain.inf_prime_pow_eq_prod, NonUnitalStarSubalgebra.prod_inf_prod, IntermediateField.map_iSup, CFilter.mem_toFilter_sets, MeasureTheory.IsStoppingTime.measurableSpace_min_const, TopologicalSpace.Closeds.coe_sup, CategoryTheory.MorphismProperty.pretopology_inf, Subalgebra.rank_sup_eq_rank_right_mul_rank_of_free, AlgebraicGeometry.Scheme.IdealSheafData.mul_inf, AlgebraicGeometry.targetAffineLocally_affineAnd_eq_affineLocally, IntermediateField.map_iInf, latticeClosure_empty, ProbabilityTheory.Kernel.indep_biSup_limsup, BoxIntegral.Box.Ioo_subset_Icc, Finset.isPWO_sup, Finset.partiallyWellOrderedOn_sup, MeasurableSet.measurableSet_liminf, Filter.mono_bliminf', CategoryTheory.Precoverage.sup_mem_coverings, sSup_div, LinearMap.eqOn_sup, BoxIntegral.Box.exists_seq_mono_tendsto, MonoidHom.noncommPiCoprod_mrange, Submodule.add_mem_sup, SimpleGraph.ComponentCompl.hom_eq_iff_not_disjoint, supClosure_mono, Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection, Algebra.TensorProduct.map_range, Ideal.IsHomogeneous.sSup, Set.Iic.instIsCompactlyGenerated, AlgebraicGeometry.Scheme.basicOpen_appLE, TopologicalSpace.Opens.map_iSup, MeasurableSpace.inf_le_invariants_comp, continuousAdd_sInf, t2_separation_compact_nhds, DeltaGeneratedSpace.sup, Submonoid.FG.iSup, Submodule.sup_dualAnnihilator_le_inf, sInf_zero, ProbabilityTheory.indep_limsup_atBot_self, IndexedPartition.disjoint, LocallyConvexSpace.sInf, SSet.horn_eq_iSup, lowerHemicontinuous_iff_isClosed_preimage_Iic, RegularSpace.inf, OrderIso.infIrredUpperSet_apply, CategoryTheory.Precoverage.IsStableUnderSup.sup_mem_coverings, Measurable.iSup', Submonoid.closure_mul_le, MeasureTheory.tendsto_eLpNorm_condExp, AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj, NonUnitalAlgebra.map_iInf, MeasureTheory.hittingAfter_eq_sInf, IntermediateField.sup_toSubalgebra_of_left, Submodule.supIndep_torsionBy, SSet.range_eq_iSup_sigma_ι, SSet.Subcomplex.BicartSq.isPushout, SupClosed.supClosure_eq, Units.topology_eq_inf, Subspace.dualAnnihilator_iInf_eq, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app, IntermediateField.isSplittingField_iSup, Projectivization.Subspace.sup_span, Submodule.iSup_map_single, LinearMap.IsIdempotentElem.range_mem_invtSubmodule, Submodule.mem_sSup_of_mem, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion, Submodule.smul_sup, ClosedSubmodule.coe_inf, ProbabilityTheory.iSup_countableFiltration, completelyRegularSpace_iInf, Filter.cofinite.liminf_set_eq, Monotone.pairwise_disjoint_on_Ico_pred, Module.AEval.mem_mapSubmodule_symm_apply, AlgebraicGeometry.isPreimmersion_eq_inf, ClosedSubmodule.toSubmodule_sSup, ProbabilityTheory.indep_iSup_of_antitone, FirstOrder.Language.Substructure.closure_iUnion, continuousSMul_iInf, coinduced_iSup, monotone_Iic, MeasureTheory.OuterMeasure.sInf_apply, LinearPMap.domain_sup, IsTopologicalBasis.iInf, AntitoneOn.Ioo, Partition.iSup_eq, mem_wellApproximable_iff, IntermediateField.iSup_eq_adjoin, TopologicalSpace.Opens.mem_sSup, 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, LinearMap.IsSymmetric.iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute, MeasureTheory.measure_inv_smul_symmDiff, HomogeneousIdeal.toIdeal_sup, IntermediateField.rank_sup_le_of_isAlgebraic, AlgebraicGeometry.isProper_eq, NonUnitalStarAlgebra.coe_iInf, Sublocale.inf_mem, Subalgebra.FG.sup, ProperlyDiscontinuousVAdd.exists_nhds_disjoint_image, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom, instIsModularLatticeAddSubgroup, Submodule.isQuotientEquivQuotientPrime_iff, Submodule.map_smul', Monotone.pairwise_disjoint_on_Ioo_succ, inf_sSup_eq_iSup_inf_sup_finset, Metric.AreSeparated.disjoint, AffineSubspace.map_inf_le, ENNReal.iInf_ne_top, Subalgebra.LinearDisjoint.finrank_sup_of_free, BoxIntegral.Box.disjoint_coe, IntermediateField.iSup_toSubfield, Subgroup.smul_sup, NNReal.iInf_real_pos_eq_iInf_nnreal_pos, FirstOrder.Language.Substructure.closure_union, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf, Filter.limsSup_bot, Submodule.span_union, TopologicalSpace.Opens.leSupr_apply_mk, IsRetrocompact.finsetSup', LinearMap.range_smul', Submonoid.coe_sup, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom, AddSubmonoid.closure_add_le, MeasureTheory.Filtration.rightCont_eq, DirectSum.IsInternal.addSubmonoid_iSup_eq_top, DFA.pumping_lemma, Submodule.small_iSup, Finsupp.disjoint_lsingle_lsingle, AffineSubspace.finiteDimensional_sup, StarSubalgebra.map_sup, CategoryTheory.GrothendieckTopology.intersection_covering, Submodule.rank_add_le_rank_add_rank, AddSubgroup.FG.biSup_finset, Pi.induced_restrict_sUnion, Submodule.sup_mul, Set.mulIndicator_iInter_apply, FirstOrder.Language.Substructure.comap_iSup_map_of_injective, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom, ProbabilityTheory.condIndep_biSup_compl, Module.End.mem_invtSubmodule_symm_iff_le_map, DualNumber.range_inlAlgHom_sup_adjoin_eps, CompleteSublattice.sSupClosed, Finsupp.codisjoint_supported_supported_iff, IsCompactlyGenerated.exists_sSup_eq, Submodule.spanRank_sup_le_sum_spanRank, Set.Iic.coe_iSup, iSupIndep_def, T2Space.t2, FirstOrder.Language.Substructure.FG.sup, Module.End.genEigenspace_top, Monotone.Ioi, infClosure_min, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_assoc, IntermediateField.relfinrank_mul_relfinrank_eq_inf_relfinrank, MonoidHom.noncommPiCoprod_range, Monoid.CoprodI.iSup_mrange_of, OpenSubgroup.toOpens_inf, Submodule.iSup_torsionBy_eq_torsionBy_prod, sSup_neg, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map, IntermediateField.fg_iSup, OrderIso.essInf_apply, TopologicalSpace.Opens.functor_map_eq_inf, IsCompactlyGenerated.BooleanGenerators.sSup_le_sSup_iff_of_atoms, MeasurableSpace.map_iInf, Metric.closedBall_disjoint_ball, SSet.hasDimensionLT_iSup_iff, equicontinuousAt_iInf_dom, AlgebraicGeometry.universallyClosed_eq_universallySpecializing, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_llp_rlp, RootPairing.root_mem_submodule_iff_of_add_mem_invtSubmodule, Submodule.set_smul_eq_iSup, ProbabilityTheory.condIndep_iSup_directed_limsup, MeasureTheory.OuterMeasure.restrict_biInf, TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible, IntermediateField.adjoin_iUnion, Subgroup.relIndex_sup_left, AntitoneOn.Iio, LieSubmodule.sSup_toSubmodule_eq_iSup, CompleteSublattice.coe_sSup, Filter.Realizer.le_iff, Subgroup.FG.iSup, CategoryTheory.Pretopology.mem_inf, latticeClosure_idem, sSup_sub, ClosedSubmodule.mem_sSup, completelyRegularSpace_inf, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv, Polynomial.sup_ker_aeval_le_ker_aeval_mul, t2Space_iff_nhds, IntermediateField.normalClosure_def'', AlgebraicGeometry.RingedSpace.basicOpen_mul, Module.End.span_orbit_mem_invtSubmodule, SSet.iSup_skeletonOfMono, DividedPowers.isSubDPIdeal_iSup, Sublattice.map_iSup, AlgebraicGeometry.Flat.surjective_descendsAlong_surjective_inf_flat_inf_quasicompact, Monotone.pairwise_disjoint_on_Ioo_pred, MeasureTheory.Filtration.coeFn_sup, CategoryTheory.MorphismProperty.retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, IsSupFiniteCompact.wellFoundedGT, ProbabilityTheory.Kernel.indep_limsup_atTop_self, AffineSubspace.nonempty_sup_right, Filter.liminf_eq_iSup_iInf, IntermediateField.relfinrank_inf_mul_relfinrank_of_le, Ideal.ofList_append, AlgebraicGeometry.IsProper.eq_valuativeCriterion, Ideal.homogeneousCore'_eq_sSup, TopologicalSpace.Opens.iSup_def, TopologicalSpace.Closeds.coe_sSup, Module.End.invtSubmodule.codisjoint_iff, Monotone.pairwise_disjoint_on_Ioc_succ, Filter.inf_liminf, Topology.IsUpper.toContinuousInf, MeasurableSet.measurableSet_limsup, AlgebraicGeometry.IsClosedImmersion.eq_isFinite_inf_mono, AlgebraicGeometry.Scheme.basicOpen_mul, Algebra.EssFiniteType.aux, Subgroup.closure_mul_le, sSupIndep_pair, AddSubmonoid.sup_eq_closure_add, OrthogonalFamily.range_linearIsometry, continuous_iSup_rng, MeasurableSpace.comap_sup, ProbabilityTheory.Kernel.indep_iSup_of_antitone, sSup_compact_le_eq, Submodule.sup_orthogonal_of_hasOrthogonalProjection, ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff, IntermediateField.relrank_inf_mul_relrank_of_le, SSet.iSup_range_eq_top_of_isColimit, Measurable.sup_of_left, AffineSubspace.direction_sInf, Submodule.isOrtho_iSup_right, Algebra.isIntegral_iSup, MeasureTheory.MeasuredSets.dist_def, Subalgebra.rank_sup_le_of_free, WithBot.coe_biInf, essInf_mono_ae, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom, AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion, MeasurableSpace.measurableSet_sInf, AlgebraicGeometry.IsAffineOpen.biSup_of_disjoint, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom, Submodule.iSup_smul, Submodule.mem_iSup_finset_iff_exists_sum, Submodule.iSup_eq_span', Representation.invtSubmodule.top_mem, Algebra.isIntegral_sup, disjoint_principal_nhdsSet, Filter.Realizer.principal_F, infClosure_prod, QuotientGroup.comap_map_mk', Submodule.iInf_orthogonal, ProjectiveSpectrum.basicOpen_eq_union_of_projection, MeasureTheory.ae_mem_limsup_atTop_iff, FirstOrder.Language.Substructure.map_iSup_comap_of_surjective, NonUnitalStarSubalgebra.coe_iSup_of_directed, Subalgebra.op_iSup, disjointed_eq_inf_compl, AddSubmonoid.FG.biSup_finset, induced_to_pi, dist_indicator, LinearMap.comap_eq_sup_ker_of_disjoint, iSupIndep.iInf, CategoryTheory.GrothendieckTopology.le_close, Set.antitone_dissipate, Sublocale.toNucleus_le_toNucleus, MeasureTheory.hittingBtwn_eq_sInf, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, Subalgebra.op_sup, continuousMul_iInf, ContinuousLinearMap.IsIdempotentElem.commute_iff, SSet.Subcomplex.preimage_max, TopologicalSpace.Opens.coe_sSup, Submodule.finite_finset_sup, Set.partialSups_eq_accumulate, IsPGroup.to_sup_of_normal_right', IntermediateField.normal_iInf, AffineSubspace.direction_sInf_of_mem, RootedTree.subtrees_disjoint, MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrict, Submodule.finrank_add_le_finrank_add_finrank, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.top_mem_range, Ideal.mem_quotient_iff_mem_sup, Subalgebra.LinearDisjoint.val_mulMap_tmul, AlgebraicGeometry.isomorphisms_eq_isOpenImmersion_inf_surjective, Submodule.span_sSup', Filter.bliminf_or_le_inf_aux_left, Sublocale.iInf_mem, Metric.eball_disjoint, Subgroup.sup_normal, TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology, TopCat.induced_of_isLimit, TopologicalSpace.IsOpenCover.iSup_eq_top, Subalgebra.mulMap_range, Submodule.lt_sup_iff_notMem, PrimitiveSpectrum.kernel_hull, Set.Mapsto.mem_invtSubmodule, ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule, Subfield.coe_sSup_of_directedOn, TopologicalSpace.Closeds.iInf_mk, Filter.mem_limsup_iff_frequently_mem, Module.End.mem_invtSubmodule_iff_forall_mem_of_mem, Subfield.extendScalars_sup, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt, TopCat.Presheaf.SheafConditionEqualizerProducts.w_apply, Ideal.IsMaximal.coprime_of_ne, Submodule.map_iSup_comap_of_surjective, Ideal.add_eq_sup, RootPairing.coe_bot, Submodule.coe_iSup_of_directed, IntermediateField.finiteDimensional_iSup_of_finite, Module.End.invtSubmodule.top_mem, AlgebraicGeometry.Scheme.Hom.preimage_inf, Set.Finite.latticeClosure, continuous_iInf_dom, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_right_of_inj, NonUnitalAlgebra.inf_toSubmodule, StarSubalgebra.sInf_toSubalgebra, nucleusIsoSublocale.eq_toSublocale, MeasurableSet.measurableSet_blimsup, IntermediateField.isSeparable_sup, CategoryTheory.MorphismProperty.transfiniteCompositions_le, StarSubalgebra.coe_inf, TopologicalSpace.gc_generateFrom, BooleanSubalgebra.biSup_mem, Submonoid.FG.sup, TopologicalSpace.Closeds.isAtom_coe, Submodule.IsLattice.sup, MaximalSpectrum.iInf_localization_eq_bot, Submodule.complementedLattice, AlgebraicGeometry.IsOpenImmersion.app_ΓIso_hom_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup, AffineSubspace.sup_direction_le, Filter.HasBasis.blimsup_eq_iInf_iSup, sInf_add, continuousVAdd_inf, Alexandrov.projSup_obj, AlgebraicGeometry.geometrically_inf, Algebra.mem_iSup_of_mem, NFA.disjoint_stepSet_reverse, Submodule.map₂_sup_left, isAtomistic_of_complementedLattice, essSup_count, Partition.disjoint, MeasureTheory.Filtration.sSup_def, MeasureTheory.measure_limsup_atTop_eq_zero, Submodule.sup_eq_top_iff, IntermediateField.isAlgebraic_iSup, LinearMap.ker_sup_ker_le_ker_comp_of_commute, coinduced_sup, LinearMap.range_ofIsCompl, normalClosure_eq_iSup_adjoin, Subalgebra.centralizer_coe_sup, MeasureTheory.abs_measureReal_sub_le_measureReal_symmDiff, Submodule.mem_iSup_of_mem, Filter.limsup_eq_iInf_iSup, CategoryTheory.PreZeroHypercover.presieve₀_sum, Filter.limsup_le_iSup, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom, IsUltrametricDist.closedBall_subset_trichotomy, MonotoneOn.Ico, Subalgebra.coe_starClosure, AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv_apply, MeasureTheory.measure_symmDiff_eq, Ideal.ofList_cons_smul, Field.Emb.Cardinal.iSup_adjoin_eq_top, Filter.bliminf_antitone_filter, Sylow.normalizer_sup_eq_top, CliffordAlgebra.iSup_ι_range_eq_top, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup, AlgebraicGeometry.IsFinite.eq_isProper_inf_isAffineHom, Filter.limsup_const_bot, Subring.smul_sup, Ideal.mul_iSup, IntermediateField.toSubalgebra_iSup_of_directed, AffineSubspace.comap_supr, Alexandrov.lowerCone_pt, Submodule.span_biUnion, iSupIndep_map_orderIso_iff, NonUnitalStarAlgebra.coe_inf, ProbabilityTheory.indep_biSup_compl, MeasureTheory.SignedMeasure.of_symmDiff_compl_positive_negative, LinearMap.coe_quotientInfToSupQuotient, blimsup_cthickening_ae_eq_blimsup_thickening, IntermediateField.isSeparable_iSup, Subfield.closure_union, RootPairing.isIrreducible_iff_invtRootSubmodule, NonUnitalStarAlgebra.map_sup, inducing_iInf_to_pi, Filter.iInf_le_liminf, AddSubmonoid.mem_iSup_iff_exists_dfinsupp', supClosure_infClosure, essSup_comp_le_essSup_map_measure, IntermediateField.sInf_toSubfield, nucleusIsoSublocale.symm_eq_toNucleus, Set.instIsCoatomistic, Partition.bot_lt_of_mem, infClosure_mono, Filter.liminf_bot, AddSubgroup.FG.biSup, AffineSubspace.map_sup, isSeparatedMap_iff_nhds, Submodule.map_sup_comap_of_surjective, UpperSet.infIrred_iff_of_finite, NonUnitalAlgebra.mem_sInf, ProbabilityTheory.condExpKernel_eq, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces, MonotoneOn.Ioc, Filter.limsInf_bot, Algebra.adjoin_iUnion, isSupFiniteCompact_iff_all_elements_compact, LieSubmodule.iSup_toSubmodule_eq_top, TopCat.nonempty_isColimit_iff_eq_coinduced, Set.mabs_mulIndicator_symmDiff, AlgebraicGeometry.Scheme.basicOpen_res, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, Submodule.isOrtho_sSup_left, Nucleus.restrict_toSublocale, equicontinuousOn_iInf_dom, AddSubgroup.ofAddUnits_sup_addUnits, RootPairing.rootSpan_mem_invtSubmodule_reflection, MeasureTheory.OuterMeasure.sInf_apply', Subalgebra.map_comap_eq, Submodule.span_sup, Ideal.map_sSup, wellFoundedGT_characterisations, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens, Ideal.quotientInfEquivQuotientProd_fst, EMetric.Closeds.lipschitz_sup, MeasureTheory.AddContent.supClosure_apply_of_mem, monotone_nhdsSet, Finsupp.supported_iUnion, InfClosed.supClosure, Algebra.mem_sup_right, SSet.modelCategoryQuillen.J_le_monomorphisms, TopologicalSpace.Opens.coe_sup, Projectivization.Subspace.span_union, StarSubalgebra.coe_iInf, IntermediateField.rank_sup_le, StarSubalgebra.mem_sInf, AddSubgroup.toAddSubmonoid_zmultiples, antitone_Ici, CategoryTheory.MorphismProperty.isStableUnderTransfiniteCompositionOfShape_iff, Filter.bliminf_not_inf, Submodule.restrictScalars_iSup, MeasureTheory.measure_symmDiff_neg_vadd, SSet.boundary_eq_iSup, MeasureTheory.limsup_ae_eq_of_forall_ae_eq, AddSubmonoid.mem_iSup_iff_exists_dfinsupp, Filter.cofinite.blimsup_set_eq, Algebra.adjoin_eq_sInf, generateFrom_union_isOpen, LinearMap.coprod_map_prod, Filter.limsup_eq_iInf_iSup_of_nat', CompleteSublattice.comap_carrier, Filter.limsSup_principal_eq_sSup, RootPairing.coe_top, Seminorm.closedBall_finset_sup', TopologicalSpace.Opens.coe_disjoint, Filter.sdiff_liminf, TopologicalSpace.Closeds.uniformContinuous_sup, HomogeneousIdeal.irrelevant_eq_iSup, Set.Iic.coe_biSup, essInf_eq_iInf, IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top, Filter.blimsup_mono, isArtinian_sup, CompleteAtomicBooleanAlgebra.instIsAtomistic, BoxIntegral.Box.measurableSet_Ioo, Subsemiring.smul_sup, Algebra.coe_inf, Subgroup.ofUnits_iSup₂, nndist_indicator, TopologicalSpace.Opens.isBasis_iff_cover, Module.End.isSemisimple_iff', Subgroup.coe_mul_of_right_le_normalizer_left, Filter.limsup_piecewise, MeasureTheory.OuterMeasure.isCaratheodory_partialSups, sSup_add, DirectSum.IsInternal.submodule_iSup_eq_top, SSet.stdSimplex.face_inter_face, DoubleCoset.disjoint_out, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMin, Antitone.Iic, Submodule.mem_iSup_of_chain, OrderIso.apply_blimsup, blimsup_thickening_mul_ae_eq, MeasurableSpace.iSup_generateFrom, IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_inf, Submodule.mem_iSup_iff_exists_finset, IsAddFoelner.tendsto_meas_vadd_symmDiff, Finset.wellFoundedOn_sup, UniformSpace.toTopologicalSpace_inf, FirstOrder.Language.DirectLimit.Equiv_isup_of_apply, MonotoneOn.Ioo, complementedLattice_iff_isAtomistic, infClosure_supClosure, TensorProduct.map_ker, CompleteLatticeHom.toOrderIsoRangeOfInjective_apply, Ideal.eq_inf_of_isPrime_inf, Submodule.localized₀_iSup, Filter.bliminf_or_le_inf_aux_right, TopologicalSpace.Opens.infLELeft_apply, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, Sublocale.infClosed, IntermediateField.adjoin_union, Submodule.iSup_eq_toSubmodule_range, MeasureTheory.OuterMeasure.sInf_eq_boundedBy_sInfGen, IntermediateField.inf_toSubfield, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiff, LinearMap.iSup_range_single_le_iInf_ker_proj, Filter.Realizer.bot_F, NonUnitalAlgebra.coe_sInf, Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf, ProbabilityTheory.condIndep_iSup_of_disjoint, Monotone.Iic, Submodule.mem_sSup_iff_exists_finset, supClosure_idem, LinearMap.disjoint_single_single, Submodule.finset_inf_coe, BooleanSubalgebra.sInf_mem, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_obj, Submodule.sup_toAddSubmonoid, StarSubalgebra.mem_sup_right, Submodule.mem_finsetInf, Filter.liminf_top_eq_iInf, AffineSubspace.mem_inf_iff, BooleanSubalgebra.map_sup, Setoid.IsPartition.pairwiseDisjoint, LinearMap.map_eq_top_iff, LieSubalgebra.span_iUnion, sSupIndep_iff_pairwiseDisjoint, BooleanSubalgebra.biInf_mem, ProbabilityTheory.iSup_partitionFiltration, Filter.Realizer.top_F, PrimitiveSpectrum.hull_sSup, isNoetherian_sup, Submodule.mem_sup, NonUnitalStarAlgebra.map_inf, IntermediateField.lift_sup, Pi.induced_precomp', CategoryTheory.MorphismProperty.precoverage_inf, Partition.sSup_eq, Filter.blimsup_sup_le_or, Subgroup.ofUnits_sSup, Ideal.multiset_prod_le_inf, infClosure_idem, Algebra.mul_mem_sup, Filter.limsInf_principal_eq_sInf, AlgebraicGeometry.Scheme.IdealSheafData.inf_mul, Ideal.le_comap_sup, continuousInv_iInf, Module.End.iSup_maxGenEigenspace_eq_top, Nat.iSup_lt_succ, MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring, isCompactElement_iff_exists_le_sSup_of_le_sSup, CompleteSublattice.disjoint_iff, NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex, Opens.toPretopology_grothendieckTopology, Filter.blimsup_not_sup, AffineSubspace.coe_iInf, BooleanSubalgebra.iInf_mem, Submodule.instIsModularLattice, StarSubalgebra.mem_inf, Ideal.ofList_cons, LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff, ClosedSubmodule.coe_iSup, Submodule.finite_iSup, Sublattice.le_comap_sup, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin, AddSubgroup.sup_eq_closure_add, upperHemicontinuous_iff_isClosed_compl_preimage_Iic_compl, Submodule.exists_mem_sup, Subalgebra.val_mulMap'_tmul, Finsupp.lsingle_range_le_ker_lapply, Monotone.Icc, WCovBy.finset_coe, FirstOrder.Language.DirectLimit.iSup_range_of_eq_top, MeasureTheory.SimpleFunc.iSup_approx_apply, IntermediateField.sup_toSubalgebra_of_right, ProbabilityTheory.condIndep_limsup_atBot_self, BoxIntegral.Prepartition.disjoint_coe_of_mem, Submodule.span_insert, Filter.blimsup_eq_iInf_biSup_of_nat, SSet.Subcomplex.preimage_iSup, Ideal.comap_map_of_surjective', blimsup_cthickening_mul_ae_eq, Filter.limsup_eq_sInf_sSup, AlgHom.eqOn_sup, AlgebraicGeometry.isomorphisms_eq_stalkwise, DFA.accepts_inter, Antitone.pairwise_disjoint_on_Ico_pred, Submodule.FG.sup, Filter.HasBasis.limsSup_eq_iInf_sSup, iSupIndep_iff_supIndep, essSup_mono_ae, CategoryTheory.MorphismProperty.transfiniteCompositions_pushouts_coproducts_le_llp_rlp, Set.definable_finset_inf, isAtomistic_iff, IntermediateField.le_sup_toSubalgebra, sSup_simples_eq_top_iff_isSemisimpleModule, Sublocale.range_toNucleus, Submodule.span_monotone, partialSups_eq_biUnion_range, AlgebraicGeometry.IsFinite.eq_inf, WithBot.coe_biSup, Matrix.range_diagonal, Filter.limsup_eq_iInf_iSup_of_nat, TopologicalSpace.Closeds.coe_sInf, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_hom, BooleanSubalgebra.le_comap_sup, Filter.blimsup_false, Submodule.mem_sSup_of_directed, Perfect.splitting, IsPGroup.to_sup_of_normal_left, CovBy.finset_coe, RestrictedProduct.topologicalSpace_eq_iSup, AlgebraicGeometry.GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible, Metric.sphere_disjoint_ball, Filter.blimsup_or_eq_sup, iSupIndep_iff_supIndep_univ, PrimitiveSpectrum.hull_iSup, IntermediateField.map_inf, infClosure_isClosed, TopologicalSpace.Opens.coe_inf, Field.Emb.Cardinal.iSup_filtration, Module.End.invtSubmodule.zero, Subgroup.index_map, Filter.blimsup_monotone_filter, withSeminorms_iInf, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃_W, Topology.IsLocallyConstructible.finsetInf', subset_supClosure, 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, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top, ProjectiveSpectrum.zeroLocus_iSup_ideal, MeasureTheory.OuterMeasure.biInf_apply', continuous_sup_rng_left, AntitoneOn.Ioc, CompleteSublattice.map_carrier, setOf_isOpen_sSup, IntermediateField.inf_relfinrank_left, disjoint_nhdsWithin_of_mem_discrete, Ideal.IsHomogeneous.sup, continuous_inf_rng, finsetInf'_mem_infClosure, iSupIndep.map_orderIso, Dynamics.dynEntourage_antitone, IntermediateField.map_sup, AlgebraicGeometry.IsAffineOpen.sup_of_disjoint, Submodule.dualAnnihilator_iSup_eq, Submodule.rank_sup_add_rank_inf_eq, AntitoneOn.Ico, Matrix.iSup_eigenspace_toLin_diagonal_eq_top, AddGroupTopology.toTopologicalSpace_iInf, Seminorm.ball_finset_sup, SSet.N.iSup_subcomplex_eq_top, IntermediateField.inf_relrank_left, Submodule.finite_sup, Topology.IsGeneratedBy.iSup, Submonoid.FG.biSup_finset, Submodule.mem_biSup_iff_exists_dfinsupp, Representation.invtSubmodule.coe_bot, Filter.mono_blimsup', nhdsKer_mono, latticeClosure_isClosed, NonUnitalStarAlgebra.sInf_toNonUnitalSubalgebra, Algebra.map_iInf, Representation.invtSubmodule.instNontrivialSubtypeSubmoduleMemSublattice, Submodule.mem_sup_left, isSemisimpleModule_biSup_of_isSemisimpleModule_submodule, sSupHom.apply_blimsup_le, isArtinian_iSup, MeasurableSpace.disjoint_countablePartition, TopCat.Sheaf.eq_of_locally_eq_iff, isCompactElement_iff_le_of_directed_sSup_le, LinearMap.mapsTo_biSup_of_mapsTo, Submodule.topologicalClosure_iSup_map_single, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply, exists_disjoint_smul_of_isCompact, AlgebraicGeometry.isPullback_opens_inf_le, disjoint_nested_nhds, MeasurableSet.exists_isOpen_symmDiff_lt, IntermediateField.relrank_inf_mul_relrank, Filter.limsInf_eq_iSup_sInf, Ideal.radical_finset_inf, MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT, IntermediateField.iInf_toSubalgebra, Algebra.mem_inf, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing, ProbabilityTheory.condIndep_iSup_of_directed_le, MeasureTheory.Filtration.coeFn_inf, MeasureTheory.MeasurePreserving.measure_symmDiff_preimage_iterate_le, DirectSum.isInternal_biSup_submodule_of_iSupIndep, Submodule.mem_sup_right, Submodule.sup_set_smul, AddSubmonoid.FG.finset_sup, LinearMap.IsIdempotentElem.ker_mem_invtSubmodule, MeasureTheory.IsSetRing.finsetSup_mem, MonotoneOn.Ioi, Submodule.sup_span, AddSubmonoid.neg_iSup, NonUnitalSubalgebra.starClosure_toNonUnitalSubalgebra, MeasureTheory.IsSetSemiring.exists_finpartition_diff, LinearPMap.supSpanSingleton_apply_mk, AlgebraicGeometry.Scheme.IdealSheafData.support_sup, Ideal.mem_sup_right, Subgroup.ofUnits_iSup, LinearMap.IsSymmetric.iSup_eigenspace_inf_eigenspace_of_commute, Sublocale.toNucleus_apply, Ideal.sup_mul, Set.abs_indicator_symmDiff, EuclideanGeometry.orthogonalProjection_sup_of_orthogonalProjection_eq, Algebra.coe_sInf, Algebra.sup_def, Ideal.snd_comp_quotientInfEquivQuotientProd, isLUB_supClosure, PolishSpace.iInf, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor, BooleanSubalgebra.iSup_mem, FirstOrder.Language.Substructure.map_iSup, IntermediateField.Lifts.carrier_union, Nat.iSup_le_succ', Filter.bliminf_eq_iSup_biInf, induced_iInf, IntermediateField.normalClosure_def', Finsupp.disjoint_supported_supported_iff, StarSubalgebra.map_iInf, PrimeSpectrum.iSup_basicOpen_eq_top_iff', Filter.bliminf_false, Set.instIsAtomistic, TopologicalSpace.Closeds.mem_iInf, NonUnitalAlgebra.sInf_toSubmodule, MeasureTheory.hitting_eq_sInf, LieSubalgebra.add_eq_sup, TopCat.limit_topology, Submodule.map_add_le, Ideal.toIdeal_homogeneousHull_eq_iSup, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₄_W, TopCat.Sheaf.interUnionPullbackCone_pt, Submodule.mem_iSup_iff_exists_dfinsupp', TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso, Filter.liminf_piecewise, Submodule.covBy_span_singleton_sup, Filter.HasBasis.limsup_eq_iInf_iSup, ProbabilityTheory.Kernel.indep_biSup_compl, essSup_mono_measure', MeasureTheory.MeasuredSets.edist_def, ClosedSubmodule.coe_sup, Sublattice.setLike_mem_coe, TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt, supClosure_prod, MeasureTheory.OuterMeasure.map_biInf_comap, AlgebraicGeometry.Scheme.IdealSheafData.support_sSup, Ideal.sup_mul_left_self, MeasureTheory.measure_symmDiff_eq_zero_iff, Subgroup.IsComplement'.sup_eq_top, AddSubmonoid.iSup_mul, finsetSup'_mem_supClosure, Submodule.wcovBy_span_singleton_sup, AlgebraicGeometry.IsIntegralHom.eq_universallyClosed_inf_isAffineHom, Module.End.invtSubmodule.bot_mem, AddSubgroup.FG.sup, infClosure_empty, Order.Ideal.PrimePair.disjoint, AddSubgroup.ofAddUnits_iSup, IntermediateField.relrank_mul_relrank_eq_inf_relrank, IsRetrocompact.finsetInf, Submodule.mem_iSup_of_directed, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup, Module.End.mem_invtSubmodule_iff_map_le, MeasureTheory.OuterMeasure.restrict_iInf_restrict, 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, sSup_zero, iSupIndep_iff_pairwiseDisjoint, Ideal.mem_iSup_of_mem, AffineSubspace.map_iSup, MeasurableSpace.measurableSet_inf, AddSubmonoid.FG.sup, Module.AEval.mem_mapSubmodule_apply, Ideal.IsHomogeneous.iSup₂, Seminorm.ball_finset_sup', IntermediateField.coe_sInf, Ideal.Filtration.iSup_N, Submodule.iSup_toAddSubmonoid, LowerSet.supIrred_Iic, MeasurableSpace.measurableSet_sup, Sublattice.setLike_mem_sup, supClosed_supClosure, R1Space.sInf, Filter.sup_liminf, Submodule.add_eq_sup, PolynormableSpace.inf, Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W, r1_separation, Subspace.dualAnnihilator_inf_eq, TrivSqZeroExt.range_inlAlgHom_sup_adjoin_range_inr, Submodule.mem_sSup, Representation.mem_invtSubmodule, KaehlerDifferential.kerTotal_map', eq_sSup_atoms, IntermediateField.normal_sup, Algebra.inf_toSubsemiring, edist_indicator, AddSubgroup.relIndex_sup_right, StarSubalgebra.iInf_toSubalgebra, Submodule.sup_toAddSubgroup, OnePoint.isCompl_range_coe_infty, CategoryTheory.PreZeroHypercover.presieve₀_add, NonUnitalAlgebra.inf_toNonUnitalSubsemiring, Submodule.mem_invtSubmodule_reflection_iff, ProbabilityTheory.indep_iSup_of_disjoint, CategoryTheory.MorphismProperty.IsLocalAtTarget.inf, FirstOrder.Language.DirectLimit.cod_partialEquivLimit, Ideal.map_iSup, MeasureTheory.OuterMeasure.map_sup, MeasureTheory.NullMeasurableSet.symmDiff, FirstOrder.Language.DirectLimit.range_lift, isAddFoelner_iff, PrimitiveSpectrum.gc, Antitone.Ioo, HomogeneousIdeal.toIdeal_iSup, IntermediateField.finiteDimensional_iSup_of_finset', LinearMap.quotientInfEquivSupQuotient_surjective, IsCyclotomicExtension.lcm_sup, ProbabilityTheory.Kernel.indep_iSup_of_disjoint, SequentialSpace.sup, AffineSubspace.sup_direction_lt_of_nonempty_of_inter_empty, Ideal.span_insert, BooleanSubalgebra.le_comap_iSup, SSet.Subcomplex.image_iSup, LinearMap.mem_span_iff_continuous, sInf_div, Submodule.map₂_sup_right, CompleteSublattice.subtype_apply, Module.End.invtSubmodule.disjoint_iff, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sSup, Module.End.isSemisimple_iff, AddUnits.topology_eq_inf, IntermediateField.finiteDimensional_sup, MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiff, Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin, Submodule.isOrtho_sup_left, ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, Submodule.isPrimary_finsetInf, MeasureTheory.Measure.QuasiMeasurePreserving.limsup_preimage_iterate_ae_eq, NonUnitalSubalgebra.mem_starClosure, IntermediateField.fixingSubgroup_sup, supClosure_univ, AlgebraicGeometry.ValuativeCriterion.eq, MeasureTheory.dist_indicatorConstLp_eq_norm, Projectivization.Subspace.span_iUnion, measurableSet_iSup_of_mem_piiUnionInter, Subgroup.noncommPiCoprod_range, OpenSubgroup.toSubgroup_sup, le_iff_compact_le_imp, topologicalAddGroup_iInf, Subgroup.ofUnits_sup_units, LieSubmodule.instIsModularLattice, t2_separation, DeltaGeneratedSpace.iSup, DirectSum.range_coeLinearMap, Alexandrov.projSup_map, Filter.Realizer.tendsto_iff, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π_apply, CategoryTheory.MorphismProperty.transfiniteCompositions_monotone, continuous_inf_dom_left, latticeClosure_min, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiffUnion, Submodule.mem_iSup, NonUnitalAlgebra.map_inf, Submodule.starProjection_tendsto_closure_iSup, Submodule.comap_sup_of_injective, LinearMap.range_add_le, continuous_sInf_rng, Sublattice.map_sup, IntermediateField.isPurelyInseparable_sup, Submodule.span_eq_iSup_of_singleton_spans, NonUnitalStarAlgebra.mem_inf, Submodule.small_sup, ProbabilityTheory.indep_limsup_self, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.sup_W, CategoryTheory.MorphismProperty.transfiniteCompositions_le_llp_rlp, MeasureTheory.Filtration.stronglyMeasurable_limitProcess, AlgebraicGeometry.descendsAlong_universallyOpen_surjective_inf_flat_inf_quasicompact, NonUnitalAlgebra.iInf_toSubmodule, Submonoid.FG.biSup, IsUltrametricDist.closedBall_eq_or_disjoint, SSet.range_eq_iSup_of_isColimit, Submodule.span_iUnion₂, FirstOrder.Language.DirectLimit.rangeLiftInclusion, LinearMap.prod_eq_sup_map, Filter.limsup_top_eq_iSup, SSet.Subcomplex.preimage_iInf, Nat.iSup_le_succ, Affine.Simplex.altitude_def, CategoryTheory.PreZeroHypercover.Hom.sieve₀_le_sieve₀, TrivSqZeroExt.range_liftAux, SSet.skeletonOfMono_succ, Dynamics.dynEntourage_monotone, Ideal.span_iUnion, monotone_closure, Order.succ_eq_sInf, LinearMap.surjective_domRestrict_iff, Submodule.coe_iSup_of_chain, MeasurableSpace.measurableSet_iSup, FirstOrder.Language.DirectLimit.dom_partialEquivLimit, AffineSubspace.comap_inf, AffineSubspace.coe_sInf, Finsupp.iSup_lsingle_range, Representation.invtSubmodule.bot_mem, continuousVAdd_iInf, MeasureTheory.Filtration.sInf_def, IsTopologicalBasis.iInf_induced, Antitone.pairwise_disjoint_on_Ico_succ, edist_mulIndicator, IntermediateField.biSup_adjoin_simple, OrderIso.apply_bliminf, AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_apply, Filter.mem_liminf_iff_eventually_mem, Algebra.Subalgebra.restrictScalars_adjoin, AlgebraicGeometry.descendsAlong_universallyInjective_surjective_inf_flat_inf_quasicompact, NonUnitalStarAlgebra.map_iInf, supClosure_min, NonUnitalStarAlgebra.inf_toNonUnitalSubalgebra, Metric.closedBall_disjoint_closedBall, ProbabilityTheory.condExpKernel_apply_eq_condDistrib, le_essInf_of_ae_le, Filter.limsSup_top, CategoryTheory.MorphismProperty.le_transfiniteCompositions, t2Space_iff, LinearMap.ker_comp_eq_of_commute_of_disjoint_ker, TopologicalSpace.Opens.mk_inf_mk, Subalgebra.unop_iSup, Subalgebra.unop_sInf, Submodule.finiteDimensional_iSup, dirSupInacc_iff_forall_sSup, CompleteSublattice.coe_sInf, LinearMap.BilinForm.span_singleton_sup_orthogonal_eq_top, CategoryTheory.MorphismProperty.transfiniteCompositions_le_iff, setOf_isOpen_sup, HilbertBasis.finite_spans_dense, Monotone.pairwise_disjoint_on_Ico_succ, Submodule.comap_map_eq

CompleteLinearOrder

Definitions

Name	Category	Theorems
toConditionallyCompleteLinearOrderBot 📖	CompOp	648 math math: Order.coheight_add_one_le, LinearGrowth.linearGrowthSup_zero, IsClosed.sSup_mem, LinearGrowth.linearGrowthSup_top, ProbabilityTheory.bayesRisk_of_subsingleton, ENNReal.iInf_div_of_ne, SimpleGraph.ediam_le_iff, SimpleGraph.ediam_anti, Order.LTSeries.length_le_krullDim, ENat.floor_pos, MeasureTheory.lintegral_def, isSaddlePointOn_value, Order.krullDim_le_of_strictComono_and_surj, Set.Finite.einfsep, MeasureTheory.iInf_mul_le_lintegral, EMetric.hausdorffEdist_iUnion_le, ENNReal.add_sInf, ENat.sSup_eq_top_of_infinite, dimH_sUnion, Set.einfsep_of_fintype, PartENat.ofENat_le, lowerSemicontinuousOn_biSup, MeasureTheory.lintegral_iSup', ENNReal.le_liminf_mul, Order.krullDim_lt_coe_iff, LinearGrowth.linearGrowthInf_add_le', LinearGrowth.le_linearGrowthSup_add, CategoryTheory.ObjectProperty.HasCardinalLT.sup, FormalMultilinearSeries.radius_pi_eq_iInf, ENNReal.ofNNReal_limsup, lowerSemicontinuousWithinAt_iSup, ENat.iInf_mul_of_ne, ENat.smul_sSup, MeasureTheory.setLIntegral_le_iSup_mul, LinearGrowth.linearGrowthSup_add_le, upperSemicontinuousAt_biInf, Metric.hausdorffEDist_def, Order.krullDim_nonneg_iff, ENNReal.limsup_const_mul_of_ne_top, IsOpen.measure_eq_iSup_isClosed, ENat.gc_toENNReal_floor, Metric.hausdorffEDist_iUnion_le, ENNReal.iSup_pow_of_ne_zero, ENat.iSup_zero, MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top, MeasureTheory.lintegral_iSup_ae, ENat.ceil_le_ceil, Order.length_le_coheight, Order.height_add_one_le, SimpleGraph.Walk.edist_le, LowerSemicontinuousOn.le_liminf, MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top, ENat.iInf_toNat, Order.krullDim_pos_iff, Order.krullDim_le_one_iff, SimpleGraph.ediam_eq_top, ENNReal.ofReal_iInf, MeasureTheory.OuterMeasure.coe_iSup, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone, MeasureTheory.lintegral_iSup_directed, 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, Submodule.spanRank_toENat_eq_iInf_encard, ExpGrowth.expGrowthSup_add, LinearGrowth.linearGrowthInf_bot, ENat.le_floor, MeasureTheory.Measure.mkMetric_apply, ENNReal.mul_iInf, ENNReal.limsup_const_mul, MeasureTheory.Measure.iInf_IicSnd_gt, Order.height_pos, MeasureTheory.biSup_measure_Iic, ENNReal.toNNReal_sSup, Order.le_krullDim_iff, MeasureTheory.lintegral_iInf_ae, ENNReal.inv_sSup, MeasureTheory.lintegral_iInf', ENNReal.limsup_liminf_le_liminf_limsup, MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum, spectrum.spectralRadius_le_liminf_pow_nnnorm_pow_one_div, LinearGrowth.linearGrowthSup_bot, MeasureTheory.SimpleFunc.iSup_coe_eapprox, ENNReal.liminf_toReal_eq, MeasurableSet.measure_eq_iSup_isCompact_of_ne_top, lowerSemicontinuousOn_iSup, lowerSemicontinuous_iff_le_liminf, LinearGrowth.linearGrowthInf_biInf, upperSemicontinuous_biInf, ENat.mul_iSup, ENat.sSup_eq_zero, IsClosed.sInf_mem, MeasureTheory.Measure.LebesgueDecomposition.iSup_succ_eq_sup, MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE, Pi.Colex.sSup_apply, ENNReal.le_iInf₂_add_iInf₂, hasCardinalLT_subtype_max, ExpGrowth.expGrowthSup_def, MeasureTheory.limsup_lintegral_le, MeasureTheory.OuterMeasure.iInf_apply', Set.Finset.coe_einfsep, egauge_univ_pi, Eventually.le_linearGrowthInf, Order.coheight_le_krullDim, ProbabilityTheory.bayesRisk_eq_iInf_measure_of_subsingleton, Order.krullDim_nonpos_iff_forall_isMax, ENNReal.iInf_div, ExpGrowth.expGrowthSup_biSup, MeasureTheory.eLpNormEssSup_eq_iSup, MeasureTheory.exists_isSigmaFiniteSet_measure_ge, ENat.biSup_add', MeasureTheory.Measure.mkMetric_le_liminf_tsum, ENNReal.biSup_add, MeasureTheory.measure_sigmaFiniteSetGE_le, ENat.iInf_mul', ENNReal.sSup_div, ENNReal.essSup_add_le, Pi.Lex.sInf_apply, EMetric.diam_insert, Order.coheight_eq_coe_add_one_iff, Order.krullDim_nonpos_iff_forall_isMin, ENNReal.iInf_sum, ENNReal.coe_sSup, liminf_eq_top, Pi.Lex.sInf_apply_le, Dynamics.coverEntropyEntourage_union, LinearGrowth.linearGrowthInf_top, MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le, ENNReal.biSup_add_biSup_le, EReal.limsup_neg, SimpleGraph.eccent_le_one_iff, PartENat.toWithTop_lt, ENat.floor_le_ceil, ENNReal.essSup_const_mul, ENNReal.iSup_coe_lt_top, LinearGrowth.linearGrowthInf_const_mul_self, MeasureTheory.lintegral_le_iSup_mul, LowerSemicontinuousWithinAt.le_liminf, ENat.iInf_coe_lt_top, ProbabilityTheory.avgRisk_le_iSup_risk, ENat.ceil_lt_top, ENNReal.iSup_natCast, CategoryTheory.ObjectProperty.IsLocal.inf, Order.height_le_krullDim, ENat.iInf_mul, Topology.IsUpper.isTopologicalSpace_basis, ENNReal.ofReal_limsup, Dynamics.coverEntropy_union, limsup_eq_bot, MvPowerSeries.le_order_subst, MeasureTheory.essSup_trim, ENat.add_iSup, ENNReal.iInf_add_iInf, MeasureTheory.OuterMeasure.trim_eq_iInf', MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure, SimpleGraph.chromaticNumber_eq_iInf, ENat.mul_sSup, LinearGrowth.linearGrowthInf_zero, SimpleGraph.chromaticNumber_sum, upperSemicontinuousOn_iInf, MeasurableSet.measure_eq_iSup_isCompact, LowerSemicontinuousAt.le_liminf, Order.bot_lt_krullDim, topologicalKrullDim_subspace_le, Eventually.linearGrowthSup_le, MeasureTheory.Content.outerMeasure_eq_iInf, topologicalKrullDim_zero_of_discreteTopology, ENNReal.liminf_sub_const, 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, ENNReal.tsum_iSup_eq, ENat.sInf_eq_zero, Order.krullDim_eq_iSup_length, Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim, Order.coheight_pos_of_lt_top, egauge_pi, essSup_comp_quotientAddGroup_mk, ENNReal.add_iInf, Order.coheight_eq_coe_iff_maximal_le_coheight, ENat.ceil_le, ENNReal.toNNReal_iSup, Antitone.measure_iUnion, MeasureTheory.lintegral_liminf_le, Order.height_pos_of_bot_lt, upperSemicontinuousWithinAt_iff_limsup_le, ENNReal.tsum_eq_iSup_nat', Metric.ediam_eq_sSup, ENNReal.inv_iSup, ENat.ceil_lt, MeasureTheory.OuterMeasure.iInf_apply, UpperSemicontinuousWithinAt.limsup_le, SimpleGraph.edist_pos_of_ne, EReal.min_neg_neg, upperSemicontinuousOn_iff_limsup_le, LinearGrowth.linearGrowthSup_biSup, ENNReal.liminf_mul_le, EReal.le_liminf_add, FormalMultilinearSeries.radius_inv_eq_limsup, ENat.ceil_pos, Set.einfsep_insert, ENat.add_sSup, ENNReal.tsum_eq_iSup_sum, Order.krullDim_nonpos_of_subsingleton, Order.coheight_eq_iSup_head_eq, ENat.ceil_add_le, MeasureTheory.le_liminf_measure_open_of_forall_tendsto_measure, ENat.lt_ceil, 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, PartENat.toWithTop_le, IsInducing.topologicalKrullDim_le, ENNReal.mul_iInf', EReal.liminf_add_le, MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le, LinearGrowth.linearGrowthSup_le_iff, 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, LinearGrowth.linearGrowthSup_const_mul_self, MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto, Set.einfsep_insert_le, MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict, ENat.sub_iSup, ENat.iInf_eq_top_of_isEmpty, MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm, ENNReal.biSup_add', ENat.floor_lt_ceil, MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto, ENat.iInf_coe_eq_top, ENNReal.iSup_add_iSup, lowerSemicontinuous_iSup, ENNReal.coe_essSup, ENat.floor_lt_top, ENNReal.iSup_sub, ENNReal.tsum_eq_iSup_sum', MvPowerSeries.le_weightedOrder_subst, ENat.gc_ceil_toENNReal, MeasureTheory.measure_sigmaFiniteSetWRT', ENat.exists_eq_iInf, IsCompact.measure_eq_iInf_isOpen, ENNReal.sub_eq_sInf, MeasureTheory.OuterMeasure.ofFunction_eq_iInf_mem, Order.height_eq_iSup_lt_height, Order.height_eq_coe_add_one_iff, dimH_eq_iInf, ENNReal.le_iInf_mul, IsClosedEmbedding.topologicalKrullDim_le, NormedSpace.equicontinuous_TFAE, Order.krullDim_enat, Order.height_le_coe_iff, LinearGrowth.linearGrowthSup_sup, IsOpen.measure_eq_iSup_isCompact, MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd, MeasureTheory.limsup_trim, Monotone.measure_iInter, Order.height_eq_coe_iff, MeasureTheory.Measure.inf_apply, ENNReal.essSup_liminf_le, SimpleGraph.edist_le_eccent, UpperSemicontinuousOn.limsup_le, SimpleGraph.edist_triangle, LinearGrowth.linearGrowthInf_inf, Relation.cutExpand_le_invImage_lex, upperSemicontinuous_iInf, ENat.coe_iInf, dimH_bUnion, EReal.coe_toENNReal_eq_max, ENNReal.inv_iInf, Order.length_le_height, ENat.mul_iInf_of_ne, EMetric.infEdist_iUnion, sInf_mem_closure, ENNReal.toNNReal_iInf, Order.height_le_height_apply_of_strictMono, MeasureTheory.eLpNormEssSup_eq_essSup_enorm, MeasureTheory.inducedOuterMeasure_eq_iInf, MeasureTheory.lintegral_iInf, MeasureTheory.le_iInf_lintegral, ENNReal.le_iInf_mul_iInf, LinearGrowth.linearGrowthSup_eventually_monotone, CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂MinOfIsClosedUnderIsomorphisms, Order.krullDim_le_one_iff_of_boundedOrder, LowerSemicontinuous.le_liminf, LinearGrowth.linearGrowthSup_const, LSeries.abscissaOfAbsConv_binop_le, MeasureTheory.measure_iUnion_of_tendsto_zero, ENat.iSup_natCast, MeasureTheory.Lp.eLpNorm'_lim_eq_lintegral_liminf, LSeries.abscissaOfAbsConv_add_le, Pi.Colex.sInf_apply_le, CategoryTheory.ObjectProperty.HasCardinalLT.iSup, ProbabilityTheory.bayesRisk_le_iInf, PiLp.edist_eq_iSup, Manifold.riemannianEDist_def, LinearGrowth.linearGrowthInf_natCast_nonneg, ENNReal.tsum_eq_limsup_sum_nat, ENat.floor_mono, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone', IsOpen.measure_eq_biSup_integral_continuous, ExpGrowth.expGrowthInf_inf, MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup, UpperSemicontinuousAt.limsup_le, EReal.le_limsup_mul, ENNReal.toReal_limsup, EReal.limsup_mul_le, ENat.le_ceil, LinearGrowth.linearGrowthSup_comp_nonneg, spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius, Order.krullDim_eq_iSup_coheight, ENNReal.add_iSup, ENNReal.iSup_coe_eq_top, SimpleGraph.ediam_le_two_mul_radius, SimpleGraph.edist_eq_sInf, upperSemicontinuousAt_iff_limsup_le, ENNReal.ofNNReal_liminf, EReal.le_liminf_mul, ENat.iSup_mul, SimpleGraph.eccent_le_ediam, le_analyticOrderAt_sub, le_analyticOrderAt_add, MeasureTheory.OuterMeasure.sSup_apply, ExpGrowth.le_expGrowthInf_add, SimpleGraph.ediam_eq_iSup_iSup_edist, LSeries.abscissaOfAbsConv_convolution_le, Order.krullDim_eq_iSup_height, UniformOnFun.edist_def', Monotone.linearGrowthInf_nonneg, MeasureTheory.tendsto_measure_sigmaFiniteSetGE, SimpleGraph.eccent_pos_iff, Topology.IsScott.instUnivSetOfIsUpper, MeasureTheory.Measure.hausdorffMeasure_le_liminf_tsum, hasCardinalLT_subtype_iSup, ENat.sSup_add, ExpGrowth.expGrowthSup_comp_le, Order.coheight_le_coheight_apply_of_strictMono, upperSemicontinuous_iff_limsup_le, ENNReal.biSup_add_biSup_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', SimpleGraph.edist_anti, ENNReal.mul_sSup, ENNReal.iSup_add_iSup_of_monotone, ENNReal.mul_iInf_of_ne, MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE', ENNReal.ofReal_essSup, ENat.coe_sInf, ENNReal.sSup_mul, ENNReal.iSup_zero, PartENat.ofENat_lt, Order.one_le_krullDim_iff, Set.einfsep_eq_iInf, ENat.iSup_eq_zero, essSup_comp_quotientGroup_mk, EReal.liminf_neg, LinearGrowth.linearGrowthInf_eventually_monotone, MeasureTheory.lintegral_eq_nnreal, UniformFun.edist_def, Order.coheight_le_iff', Order.krullDim_le_of_strictMono, ENNReal.iInf_mul_iInf, MeasureTheory.SimpleFunc.lintegral_restrict_iUnion_of_directed, ENNReal.limsup_eq_zero_iff, MeasureTheory.IsFundamentalDomain.essSup_measure_restrict, ExpGrowth.expGrowthInf_iInf, EReal.liminf_mul_le, EReal.max_neg_neg, MeasureTheory.OuterMeasure.sInf_apply, MeasureTheory.iInf_le_lintegral, iSup₂_iInf₂_le_iInf₂_iSup₂, ENNReal.add_biSup', lowerSemicontinuousWithinAt_iff_le_liminf, Monotone.expGrowthInf_comp_le, PartENat.withTopEquiv_le, ENNReal.hasSum, ENat.iSup_add, PartENat.withTopEquiv_lt, StieltjesFunction.length_eq, ENNReal.add_sSup, MeasureTheory.measure_eq_iInf', ENNReal.iInf_mul', MeasureTheory.lintegral_iInf_directed_of_measurable, Metric.infEDist_iUnion, ENNReal.iSup_div, LinearGrowth.linearGrowthInf_iInf, lowerSemicontinuousAt_iff_le_liminf, UniformOnFun.edist_def, MeasureTheory.Measure.iInf_rat_gt_prod_Iic, MeasureTheory.OuterMeasure.boundedBy_apply, ENNReal.limsup_add_of_right_tendsto_zero, ProbabilityTheory.iSup_bayesRisk_le_minimaxRisk, LinearGrowth.linearGrowthInf_monotone, ENat.ceil_mono, ENat.mul_iInf, SimpleGraph.diam_def, ENat.sSup_mul, ENat.iSup_coe_eq_top, ProbabilityTheory.bayesRisk_le_iInf', ENNReal.toReal_essSup, BoundedContinuousFunction.edist_eq_iSup, ExpGrowth.expGrowthInf_biInf, LinearGrowth.linearGrowthSup_iSup, LinearGrowth.linearGrowthInf_comp_nonneg, ENNReal.essSup_mul_le, SimpleGraph.edist_le_ediam, ENNReal.toReal_sSup, ENNReal.sub_iSup, Order.coheight_le_coe_iff, 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, ProbabilityTheory.bayesRisk_const_of_neZero, MeasureTheory.measure_eq_iInf, ENNReal.limsup_mul_le', MeasureTheory.le_iInf₂_lintegral, upperSemicontinuousOn_biInf, MeasureTheory.Measure.iSup_restrict_spanningSets, ENNReal.le_iInf_add_iInf, MeasureTheory.lintegral_iSup, ENNReal.iInf_mul, ENNReal.toReal_iInf, Order.krullDim_le_one_iff_forall_isMax, ENNReal.iSup_eq_zero, ENNReal.sInf_add, ENat.floor_lt, MeasurableSet.measure_eq_iSup_isClosed_of_ne_top, ENNReal.iInf_coe_lt_top, Order.krullDim_pos_iff_of_orderTop, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, MeasureTheory.eLpNormEssSup_count, ProbabilityTheory.bayesRisk_const, SimpleGraph.radius_le_ediam, MeasureTheory.OuterMeasure.iUnion_of_tendsto_zero, cauchy_davenport_minOrder_add, ENNReal.smul_sSup, SimpleGraph.chromaticNumber_eq_biInf, Order.coheight_coe_enat, ENNReal.sSup_add, LinearGrowth.le_linearGrowthInf_iff, Topology.IsScott.isOpen_iff_Iic_compl_or_univ, SimpleGraph.eccent_le_iff, MeasureTheory.iSup₂_lintegral_le, Order.krullDim_eq_iSup_height_add_coheight_of_nonempty, ENNReal.tsum_eq_iSup_nat, AlgebraicGeometry.geometrically_inf, ENNReal.iInf₂_add, upperSemicontinuousWithinAt_biInf, Order.krullDim_pos_iff_of_orderBot, SimpleGraph.ediam_def, ENNReal.essSup_indicator_eq_essSup_restrict, MeasureTheory.OuterMeasure.top_apply', ExpGrowth.expGrowthInf_def, LinearGrowth.linearGrowthInf_le_of_eventually_le, ENNReal.tsum_eq_liminf_sum_nat, LinearGrowth.linearGrowthInf_le_iff, EReal.le_limsup_add, MeasureTheory.Measure.hausdorffMeasure_apply, PartENat.withTopEquiv_symm_le, LinearGrowth.linearGrowthSup_comp_le, Monotone.linearGrowthInf_comp_le, ProbabilityTheory.bayesRisk_discard, ENNReal.iSup_pow, Ideal.sup_height_eq_ringKrullDim, Monotone.linearGrowthInf_comp_mul, isSaddlePointOn_iff, EMetric.hausdorffEdist_def, ENNReal.sub_iInf, ENNReal.essSup_restrict_eq_of_support_subset, Set.measure_eq_iInf_isOpen, LSeries.abscissaOfAbsConv_sub_le, MeasureTheory.Measure.mkMetric_le_liminf_sum, MeasureTheory.lintegral_enorm_le_liminf_of_tendsto, ENNReal.iSup_lt_eq_self, MeasureTheory.OuterMeasure.sInf_apply', Order.coheight_eq_coe_iff, ENNReal.finsetSum_iSup_of_monotone, IsCompact.measure_eq_biInf_integral_hasCompactSupport, MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf, MeasureTheory.SimpleFunc.iSup_eapprox_apply, SimpleGraph.radius_le_eccent, MeasureTheory.ae_eq_set_symmDiff, ENat.toENNReal_iSup, ENat.lt_floor, dimH_iUnion, Monotone.measure_iUnion, LinearGrowth.linearGrowthInf_add_le, Order.height_le_iff, Frequently.linearGrowthInf_le, Order.KrullDimLE.krullDim_le, ENNReal.iSup_mul_le, Monotone.linearGrowthInf_comp, ENat.add_biSup, ENNReal.liminf_add_of_left_tendsto_zero, MeasureTheory.OuterMeasure.sInfGen_def, Directed.measure_iInter, ENat.mul_iInf', Order.coheight_anti, EMetric.diam_eq_sSup, Order.height_mono, CategoryTheory.ObjectProperty.instIsTriangulatedMinOfIsClosedUnderIsomorphisms, Order.height_le_iff', Order.krullDim_nonneg, MeasureTheory.measure_iUnion_eq_iSup_accumulate, lowerSemicontinuousAt_iSup, Monotone.linearGrowthSup_nonneg, ENNReal.hasProd_iInf_prod, Pi.Colex.sInf_apply, Order.coheight_pos, ENat.iInf_eq_zero, Metric.ediam_iUnion_mem_option, Monotone.linearGrowthSup_comp_mul, Monotone.le_linearGrowthSup_comp, Order.index_le_height, ExpGrowth.expGrowthSup_sup, Order.coheight_eq, Order.krullDim_le_one_iff_forall_isMin, Topology.IsLower.isTopologicalSpace_basis, bsupr_limsup_dimH, ENNReal.limsup_const_sub, ENNReal.add_iInf₂, ENat.floor_le_floor, MeasureTheory.iSup_lintegral_le, Pi.Lex.le_sSup_apply, upperSemicontinuousAt_iInf, upperSemicontinuousWithinAt_iInf, MeasureTheory.OuterMeasure.biInf_apply', ENNReal.le_limsup_mul, SimpleGraph.edist_le, ENNReal.limsup_add_le, Order.rev_index_le_coheight, MeasureTheory.lintegral_liminf_le', Monotone.linearGrowthSup_comp, MeasureTheory.OuterMeasure.iSup_apply, ENNReal.iSup_mul, cauchy_davenport_minOrder_mul, lowerSemicontinuousWithinAt_biSup, ENat.sSup_eq_zero', ENNReal.limsup_sub_const, ENNReal.inv_liminf, ENNReal.finsetSum_iSup, Pi.Lex.sSup_apply, lowerSemicontinuousAt_biSup, ENNReal.iInf_gt_eq_self, ENNReal.eventually_le_limsup, ENNReal.inv_limsup, Set.einfsep_iUnion_mem_option, Set.chainHeight_eq_iSup, ENNReal.toNNReal_sInf, MeasureTheory.OuterMeasure.trim_eq_iInf, ContinuousMap.enorm_eq_iSup_enorm, ENNReal.inv_sInf, ENNReal.coe_iInf, Order.height_eq_iSup_last_eq, ENat.toENNReal_iInf, BoundedContinuousFunction.enorm_eq_iSup_enorm, ExpGrowth.expGrowthSup_iSup, Order.height_enat, ENNReal.limsup_toReal_eq, dimH_def, Order.length_le_height_last, Order.coheight_eq_iSup_gt_coheight, LinearGrowth.linearGrowthSup_monotone, LinearGrowth.linearGrowthInf_le_linearGrowthSup_of_frequently_le, LinearGrowth.le_linearGrowthInf_comp, ENNReal.tprod_eq_iInf_prod, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_P, MeasureTheory.AECover.iSup_lintegral_eq_of_countably_generated, MeasureTheory.OuterMeasure.ofFunction_apply, ProbabilityTheory.bayesRisk_const', LinearGrowth.le_linearGrowthSup_iff, Order.length_le_coheight_head, MeasureTheory.setLIntegral_iUnion_of_directed, ENat.ceil_le_floor_add_one, MeasureTheory.lintegral_eq_iSup_eapprox_lintegral, ENNReal.coe_iSup, ENNReal.image_coe_uIcc, FormalMultilinearSeries.radius_eq_liminf, PartENat.withTopEquiv_symm_lt, ENNReal.iInf_div', ENNReal.limsup_add_of_left_tendsto_zero, ENat.add_biSup', ENNReal.essSup_eq_zero_iff, lowerSemicontinuousOn_iff_le_liminf, MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto, ENNReal.ae_le_essSup, Mathlib.Meta.Positivity.natCeil_pos, ENat.biSup_add, Order.bot_lt_krullDim_iff, ENNReal.iInf_coe_eq_top, ENNReal.iSup₂_pow_of_ne_zero, Order.height_eq_coe_iff_minimal_le_height, SimpleGraph.eccent_def, iSup_limsup_dimH, LinearGrowth.le_linearGrowthInf_add, UpperSemicontinuous.limsup_le, ENNReal.coe_sInf, Order.one_lt_height_iff, MeasureTheory.iInf_mul_le_setLIntegral, MeasureTheory.measure_sigmaFiniteSetGE_ge, ContinuousMap.edist_eq_iSup, Order.coheight_le_iff, ENat.iSup_coe_lt_top, Metric.infEDist_biUnion, EReal.limsup_add_le, analyticOrderAt_add_of_ne, egauge_pi', MeasureTheory.OuterMeasure.iSup_sInfGen_nonempty, ENNReal.toReal_iSup, lowerSemicontinuous_biSup, ENat.floor_le, sSup_mem_closure, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.sup_P, Order.krullDimLE_iff, ENNReal.add_biSup, Metric.ediam_insert, MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm', Frequently.le_linearGrowthSup, MeasureTheory.Measure.iSup_restrict_spanningSets_of_measurableSet, SimpleGraph.edist_le_one_iff_adj_or_eq, MeasureTheory.lintegral_le_iSup, SimpleGraph.radius_eq_iInf_iSup_edist, ENNReal.mul_iSup, EMetric.diam_iUnion_mem_option, LinearGrowth.linearGrowthInf_neg, Monotone.le_expGrowthSup_comp, ENNReal.toReal_sInf

ConditionallyCompleteLattice

Definitions

Name	Category	Theorems
toConditionallyCompletePartialOrder 📖	CompOp	1999 math math: BooleanSubalgebra.map_iSup, continuousNeg_iInf, CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup, Ordinal.iSup_eq_iSup, Order.coheight_add_one_le, IsClosed.sSup_mem, upperBounds_supClosure, Filter.bliminf_sup_le_or_aux_right, Set.Finite.t2_separation, Ordinal.iSup_eq_bsup, TopCat.binaryCofan_isColimit_iff, dirSupClosed_iff_forall_sSup, Nat.iInf_le_succ', tendsto_zero_iff_meromorphicOrderAt_pos, ProbabilityTheory.bayesRisk_of_subsingleton, csSup_pair, ENNReal.iInf_div_of_ne, Metric.ball_disjoint_ball, MeasureTheory.OuterMeasure.map_iInf, Ordinal.lift_card_iSup_le_sum_card, SimpleGraph.ediam_le_iff, OrderIso.map_radical, SimpleGraph.ediam_anti, Set.Iic.coe_sInf, Acc.rank_eq, homotopyEquivalences_le_quasiIso, continuous_sInf_dom₂, Cardinal.mk_sUnion_le, PolynormableSpace.sInf, Ordinal.iSup_pow_natCast, Filter.liminf_eq, Order.LTSeries.length_le_krullDim, ENat.floor_pos, AddSubmonoid.smul_iSup, StarSubalgebra.coe_sInf, Module.rank_def, isFullyInvariant_iff_sSup_isotypicComponents, Filter.HasBasis.liminf_eq_ite, Nat.iSup_lt_succ', MeasureTheory.lintegral_def, SetTheory.PGame.grundyValue_eq_sInf_moveLeft, Continuous.strictMono_of_inj_boundedOrder', GroupTopology.toTopologicalSpace_iInf, Ordinal.sup_eq_lsub_iff_lt_sup, equicontinuousWithinAt_iInf_dom, FirstOrder.Language.Substructure.mem_sSup_of_directedOn, isSaddlePointOn_value, Order.krullDim_le_of_strictComono_and_surj, iSupIndep.injOn_iInf, ContinuousMap.compactOpen_eq_iInf_induced, MeasureTheory.iInf_mul_le_lintegral, sInfHom.le_apply_bliminf, Measurable.biSup, EMetric.hausdorffEdist_iUnion_le, ENNReal.add_sInf, IntermediateField.sSup_toSubfield, Algebra.mem_iInf, ENat.sSup_eq_top_of_infinite, EisensteinSeries.hasSum_e2Summand_symmetricIcc, MulAction.IwasawaStructure.is_generator, AlgebraicGeometry.iSup_affineOpens_eq_top, Subalgebra.coe_iSup_of_directed, dimH_sUnion, nhds_sInf, Ordinal.sInf_compl_lt_lift_ord_succ, MeasureTheory.hittingBtwn_apply_mono_right, Antitone.Icc, PartENat.ofENat_le, continuousMul_sInf, TopologicalSpace.Closeds.iInf_def, Subfield.mem_sSup_of_directedOn, MeasureTheory.hittingBtwn_mono_left, setOf_isOpen_iSup, RootPairing.Base.not_nonneg_iff_neg_of_sum_mem_range_root, isClosed_iSup_iff, lowerSemicontinuousOn_biSup, MeasureTheory.lintegral_iSup', Filter.bliminf_sup_le_and_aux_right, SeparatedNhds.disjoint, Cardinal.lift_iSup_le_lift_iSup, topologicalGroup_iInf, Order.krullDim_lt_coe_iff, eq_sInf_coatoms, TopologicalSpace.Opens.coe_iSup, IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot, TopCat.Presheaf.coveringOfPresieve.iSup_eq_of_mem_grothendieck, disjoint_or_subset_of_isClopen, FirstOrder.Language.Substructure.mem_iSup_of_directed, ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm, NNReal.iSup_of_not_bddAbove, Ordinal.sup_eq_lsub_iff_succ, Matrix.iSup_eigenspace_toLin'_diagonal_eq_top, FormalMultilinearSeries.radius_pi_eq_iInf, NatOrdinal.instAddLeftReflectLE, SSet.modelCategoryQuillen.I_le_monomorphisms, supClosure_eq_self, MonotoneOn.Icc, Finset.inf'_univ_eq_ciInf, Filter.blimsup_and_le_inf, Padic.withValUniformEquiv_norm_le_one_iff, tendsto_cobounded_iff_meromorphicOrderAt_neg, lowerSemicontinuousWithinAt_iSup, Set.Finite.lt_csInf_iff, NNReal.mul_iSup_le, NatOrdinal.lt_mul_iff, ENat.iInf_mul_of_ne, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_W, ENat.smul_sSup, Disjoint.of_span₀, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup, MeasureTheory.setLIntegral_le_iSup_mul, MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_disjointOfDiff, Ordinal.iSup_typein_succ, LieSubmodule.iSup_toSubmodule, R1Space.iInf, antitone_continuousOn, MeasureTheory.hittingAfter_bot_le_iff, isSublattice_latticeClosure, ProbabilityTheory.condIndep_iSup_of_antitone, IntermediateField.isPurelyInseparable_iSup, AlgebraicGeometry.IsAffineOpen.iSup_of_disjoint, strictMono_nhdsSet, Filter.bliminf_sup_le_and_aux_left, upperSemicontinuousAt_biInf, Metric.hausdorffEDist_def, SSet.iSup_subcomplexOfSimplex_prod_eq_top, csInf_mem, nhds_iInf, continuous_sSup_dom, Ordinal.log_def, ConditionallyCompleteLinearOrder.toCompactIccSpace, Monotone.Ici, isPreconnected_iff_ordConnected, CategoryTheory.MorphismProperty.HasCardinalLT.iSup, AddMonoidHom.noncommPiCoprod_range, Subalgebra.op_sSup, isClosed_sSup_iff, Bornology.IsBounded.subset_Icc_sInf_sSup, iSupIndep.disjoint_biSup, Finset.ordConnected_range_coe, AffineSubspace.mem_sInf_iff, CompleteSublattice.isComplemented_iff, AntitoneOn.Ici, ciSup_partialSups_eq', Cardinal.iSup_of_empty, Order.krullDim_nonneg_iff, MeasureTheory.hittingBtwn_univ, SSet.finite_iSup_iff, Submodule.map₂_iSup_right, inf_mem_infClosure, sSup_Iio_eq_self_iff_isSuccPrelimit, IsOpen.measure_eq_iSup_isClosed, Cardinal.iSup_lt_of_isRegular, latticeClosure_univ, monotone_hausdorffEntourage, ENat.gc_toENNReal_floor, Ideal.mem_sSup_of_mem, ContinuousLinearMap.nnnorm_def, Metric.hausdorffEDist_iUnion_le, IsCompactlyGenerated.BooleanGenerators.sSup_inter, ENNReal.iSup_pow_of_ne_zero, IsCompactlyGenerated.BooleanGenerators.isAtom, ENat.iSup_zero, NFA.pumping_lemma, ProbabilityTheory.Kernel.indep_iSup_directed_limsup, MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top, TopologicalSpace.eq_induced_by_maps_to_sierpinski, isPreconnected_Ici, NNReal.coe_sSup, Set.indicator_iUnion_apply, ProbabilityTheory.indep_iSup_of_monotone, MeasureTheory.lintegral_iSup_ae, isLeast_csInf, SeparatedNhds.disjoint_closure_left, ENat.ceil_le_ceil, IntermediateField.coe_iSup_of_directed, Order.length_le_coheight, Submodule.map_iSup, Int.padicValuation_lt_one_iff, Order.height_add_one_le, MeromorphicNFAt.meromorphicOrderAt_nonneg_iff_analyticAt, Submodule.mem_iSup_iff_exists_finsupp, Subalgebra.op_sInf, Filter.Realizer.map_F, Ordinal.sup_succ_le_lsub, ClosedSubmodule.coe_sSup, IsUltrametricDist.ball_subset_trichotomy, Algebra.sSup_def, SimpleGraph.Walk.edist_le, Ordinal.iSup_le_lsub, continuousVAdd_sInf, Ordinal.card_iSup_Iio_le_sum_card, BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff, isGLB_infClosure, ENat.iInf_toNat, IsClosed.upperClosure, Monotone.Ioo, Order.krullDim_pos_iff, SimpleGraph.ComponentCompl.disjoint_right, Nimber.succ_def, Order.krullDim_le_one_iff, Filter.bliminf_sup_le_and, SimpleGraph.ediam_eq_top, Algebra.mem_sInf, ENNReal.ofReal_iInf, MeasureTheory.OuterMeasure.coe_iSup, Cardinal.sum_le_mk_mul_iSup, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone, EMetric.ball_disjoint, cbiSup_eq_of_not_forall, generateFrom_sUnion, csInf_zero, MeasureTheory.lintegral_iSup_directed, Subalgebra.centralizer_coe_iSup, ProbabilityTheory.bayesRisk_of_subsingleton', Ideal.sup_primeHeight_eq_ringKrullDim, BoxIntegral.Box.disjoint_withBotCoe, Antitone.pairwise_disjoint_on_Ioc_pred, Function.sSup_div_semiconj, RootPairing.coe_chainBotCoeff_eq_sSup, ENNReal.iSup_add_iSup_le, setOf_liouvilleWith_subset_aux, WellFoundedGT.iSup_eq_monotonicSequenceLimit, Pi.Colex.le_sSup_apply, ENNReal.iInf_ennreal, Set.Nonempty.eq_Icc_iff_int, IsCompact.separation_of_notMem, Directed.measure_iUnion, IsSublattice.latticeClosure_eq, MeasureTheory.lowerCrossingTime_le, DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, CategoryTheory.GrothendieckTopology.monotone_close, Submodule.spanRank_toENat_eq_iInf_encard, Sublocale.coe_iInf, SupClosed.biSup_mem_of_nonempty, NonUnitalAlgebra.sInf_toNonUnitalSubsemiring, ProbabilityTheory.condIndep_iSup_of_monotone, NatOrdinal.instIsOrderedMonoid, MeasureTheory.hittingAfter_mono, Submodule.iSup_map_single_le, NatOrdinal.instIsOrderedRing, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.exists_ordinal, Nimber.mul_le_of_forall_ne, IsCompact.sSup_mem, CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact, LinearMap.iSup_range_single, NonUnitalStarAlgebra.mem_sInf, ENat.le_floor, NNReal.coe_iSup, TopologicalSpace.Opens.iSup_mk, AddSubmonoid.iSup_map_single, iSupIndep.pairwiseDisjoint, LinearMap.eventually_iSup_ker_pow_eq, AEMeasurable.iInf, Subfield.coe_iSup_of_directed, Nat.iInf_lt_succ', TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one, BoxIntegral.Box.Ioo_subset_coe, IsCompact.isLeast_sInf, generateFrom_iUnion_isOpen, MeasureTheory.Measure.mkMetric_apply, ENNReal.mul_iInf, TopologicalSpace.Closeds.coe_iInf, RootPairing.setOf_root_add_zsmul_mem_eq_Icc, LinearOrderedField.lt_inducedMap_iff, MeasureTheory.Measure.iInf_IicSnd_gt, Order.height_pos, MeasureTheory.biSup_measure_Iic, Filter.bliminf_antitone, Finite.ciInf_le, separated_by_continuous, ENNReal.toNNReal_sSup, Submodule.smul_iSup', Order.le_krullDim_iff, Antitone.pairwise_disjoint_on_Ioo_pred, MeasureTheory.lintegral_iInf_ae, ENNReal.inv_sSup, MeasurableSpace.measurableSet_iInf, IntermediateField.coe_iInf, MeasureTheory.OuterMeasure.comap_iInf, Filter.liminf_eq_iSup_iInf_of_nat', MeasureTheory.lintegral_iInf', CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_transfiniteCompositions, Cardinal.lift_iInf, SimpleGraph.ComponentCompl.pairwise_disjoint, iSup_partialSups_eq, Nimber.add_le_of_forall_ne, MeasurableSpace.measurableSet_sSup, Submodule.biSup_comap_subtype_eq_top, Filter.HasBasis.limsInf_eq_iSup_sInf, Subgroup.FG.biSup, AddGroupTopology.toTopologicalSpace_sInf, disjoint_nested_nhds_of_not_inseparable, Order.succ_eq_iInf, Submodule.biSup_eq_range_dfinsupp_lsum, Algebra.adjoin_attach_biUnion, ContinuousLinearMap.sSup_sphere_eq_nnnorm, Set.mulIndicator_iUnion_apply, Filter.bliminf_eq_iSup_biInf_of_nat, MeasureTheory.SimpleFunc.iSup_coe_eapprox, LinearOrderedField.inducedOrderRingIso_self, exists_disjoint_vadd_of_isCompact, AntitoneOn.Icc, MeasurableSet.measure_eq_iSup_isCompact_of_ne_top, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, IsCompact.sSup_lt_iff_of_continuous, sSupIndep.pairwiseDisjoint, lowerSemicontinuousOn_iSup, Submodule.fg_biSup, generateFrom_iInter_of_generateFrom_eq_self, upperSemicontinuous_biInf, ENat.mul_iSup, ENat.sSup_eq_zero, Disjoint.of_span, RootPairing.Base.pos_or_neg_of_sum_smul_root_mem, IsClosed.sInf_mem, sSup_atoms_le_eq, AddSubgroup.noncommPiCoprod_range, LinearMap.iInf_ker_proj_le_iSup_range_single, NonUnitalStarAlgebra.iInf_toNonUnitalSubalgebra, MeasureTheory.Measure.LebesgueDecomposition.iSup_succ_eq_sup, NNReal.iSup_eq_zero, Matroid.cRank_eq_iSup_cardinalMk_indep, TopologicalSpace.Closeds.gc, isEmbedding_sumElim, Ordinal.card_sInf_range_compl_le_lift, NonUnitalStarAlgebra.coe_sInf, MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE, Ordinal.iSup_le, CompleteSublattice.sSupClosed', Pi.Colex.sSup_apply, IntermediateField.finiteDimensional_iSup_of_finset, ENNReal.le_iInf₂_add_iInf₂, NNReal.natCast_iInf, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, MonotoneOn.Iio, AffineSubspace.span_iUnion, CategoryTheory.Sieve.overEquiv_le_overEquiv_iff, SSet.iSup_skeleton, disjoint_interior_frontier, Filter.blimsup_eq, PrimeSpectrum.iSup_basicOpen_eq_top_iff, IsNormalClosure.adjoin_rootSet, Submodule.annihilator_iSup, Subfield.closure_iUnion, Filter.Realizer.ne_bot_iff, ENNReal.iSup_ne_top, antitone_Ioi, TopCat.colimit_topology, Pi.induced_restrict, Set.Finite.infClosure, Filter.HasBasis.limsup_eq_sInf_univ_of_empty, MeasureTheory.OuterMeasure.iInf_apply', ofDual_preimage_latticeClosure, Submodule.neg_iSup, Ordinal.iSup_succ, MeasureTheory.IsSetSemiring.disjointOfUnion_props, Ordinal.Principal.sSup, NatOrdinal.add_le_iff, egauge_univ_pi, ProbabilityTheory.indep_biSup_limsup, MeasureTheory.Measure.sInf_caratheodory, Order.coheight_le_krullDim, Ideal.Filtration.sSup_N, ProbabilityTheory.bayesRisk_eq_iInf_measure_of_subsingleton, Monoid.CoprodI.mrange_eq_iSup, AlgebraicGeometry.Scheme.Hom.image_iSup₂, Algebra.coe_iInf, Order.krullDim_nonpos_iff_forall_isMax, ValuativeRel.nonempty_orderIso_withZeroMul_int_iff, Finset.coe_wcovBy_coe, MeasureTheory.OuterMeasure.restrict_iInf, MeasureTheory.OuterMeasure.le_sum_caratheodory, ENNReal.iInf_div, ExpGrowth.expGrowthSup_biSup, MeasureTheory.eLpNormEssSup_eq_iSup, isNoetherian_iSup, MeasureTheory.exists_isSigmaFiniteSet_measure_ge, Filter.HasBasis.limsup_eq_ite, ENat.biSup_add', CompleteSublattice.coe_iInf, Ideal.iSup_eq_span, Finset.sup_univ_eq_ciSup, Nimber.pos_iff_ne_zero, normalClosure_eq_iSup_adjoin', NatOrdinal.succ_def, ENNReal.biSup_add, MeasureTheory.measure_sigmaFiniteSetGE_le, ENat.iInf_mul', IntermediateField.iInf_toSubfield, sSup_isotypicComponents, Antitone.Ico, continuousNeg_sInf, MeasureTheory.OuterMeasure.map_iInf_comap, ENNReal.sSup_div, Monotone.pairwise_disjoint_on_Ioc_pred, continuous_sSup_rng, CategoryTheory.Pretopology.mem_toGrothendieck, Antitone.pairwise_disjoint_on_Ioo_succ, Measurable.iSup, Pi.Lex.sInf_apply, MeasurableSpace.generateFrom_iUnion_measurableSet, ProbabilityTheory.Kernel.indep_iSup_limsup, Ordinal.iSup_pow, Submodule.submodule_eq_sSup_le_nonzero_spans, εNFA.pumping_lemma, EMetric.diam_insert, Cardinal.lift_iSup, Filter.HasBasis.limsup_eq_sInf_iUnion_iInter, Order.coheight_eq_coe_add_one_iff, ProbabilityTheory.indep_iSup_of_directed_le, latticeClosure_mono, Ordinal.deriv_limit, image_latticeClosure', Order.krullDim_nonpos_iff_forall_isMin, isConnected_Iio, ENNReal.iInf_sum, Nimber.add_trichotomy, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types, ENNReal.coe_sSup, Measurable.iSup_Prop, EisensteinSeries.tsum_symmetricIco_linear_sub_linear_add_one_eq_zero, AffineSubspace.affineSpan_eq_sInf, AlgebraicGeometry.Scheme.Hom.preimage_iSup, MeasureTheory.hittingBtwn_mono, Pi.Lex.sInf_apply_le, Ordinal.card_sInf_range_compl_le, MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le, ENNReal.biSup_add_biSup_le, SupClosed.iSup_mem, Submodule.iSup_mul, NatOrdinal.lt_add_iff, regularSpace_sInf, Submodule.localized'_iSup, meromorphicOrderAt_add, Algebra.sInf_toSubsemiring, Algebra.sInf_toSubmodule, LinearMap.isCompl_iSup_ker_pow_iInf_range_pow, HomogeneousIdeal.toIdeal_iSup₂, upperHemicontinuousWithinAt_iff_preimage_Iic, topologicalAddGroup_sInf, EisensteinSeries.G2_eq_tsum_symmetricIco, Ordinal.sSup_eq_bsup, Nimber.add_def, Cardinal.lift_sSup, MeasureTheory.Content.innerContent_iSup_nat, MeasureTheory.IsSetSemiring.isSetRing_supClosure, SimpleGraph.eccent_le_one_iff, Partition.pairwiseDisjoint, PartENat.toWithTop_lt, Filter.bliminf_sup_le_or_aux_left, MeasureTheory.upperCrossingTime_mono, Submodule.dualCoannihilator_iSup_eq, ENat.floor_le_ceil, isPreconnected_Iic, continuous_iInf_rng, Ordinal.iSup_add_nat, Antitone.Ioc, MeasureTheory.hittingBtwn_apply_anti, Cardinal.mk_biUnion_le_lift, ENNReal.iSup_coe_lt_top, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le, IsCompact.isLUB_sSup, Submodule.span_attach_biUnion, NonarchimedeanGroup.exists_openSubgroup_separating, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top', MeasureTheory.lintegral_le_iSup_mul, RootPairing.setOf_root_sub_zsmul_mem_eq_Icc, Cardinal.lift_iSup_le, Int.cofinite_eq, Set.Nonempty.ordConnected_iff_of_bdd', MeasureTheory.AddContent.supClosure_apply_finpartition, CompleteAtomicBooleanAlgebra.instIsCoatomistic, Ordinal.iSup_sum, iSupIndep_pair, Submodule.comap_iSup_map_of_injective, Submodule.map₂_iSup_left, CompleteSublattice.coe_sInf', ENat.iInf_coe_lt_top, ProbabilityTheory.avgRisk_le_iSup_risk, LinearMap.iSup_range_single_eq_iInf_ker_proj, NonUnitalAlgebra.mem_iInf, ENat.ceil_lt_top, Ctop.Realizer.nhds_F, Set.Finite.csSup_lt_iff, ENNReal.iSup_natCast, lowerHemicontinuous_iff_isOpen_compl_preimage_Iic_compl, MeasureTheory.IsSetSemiring.mem_supClosure_iff, exists_eq_ciInf_of_finite, Order.height_le_krullDim, ENat.iInf_mul, SupClosed.infClosure, Topology.IsUpper.isTopologicalSpace_basis, NatOrdinal.lt_one_iff_zero, tendsto_intCast_atBot_sup_atTop_cobounded, disjoint_nhdsSet_principal, BoxIntegral.Box.iUnion_Ioo_of_tendsto, t2_separation_nhds, sInf_eq_argmin_on, AffineSubspace.mem_iInf_iff, NatOrdinal.instIsOrderedCancelAddMonoid, PseudoMetricSpace.dist_ofPreNNDist, sInf_sub, MvPowerSeries.le_order_subst, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_monotone, sSup_compact_eq_top, MonotoneOn.Ici, ENat.add_iSup, ciInf_le', NNReal.iSup_mul_iSup_le, TopologicalSpace.Closeds.mem_sInf, Filter.bliminf_or_le_inf, MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ, ENNReal.iInf_add_iInf, IntermediateField.normal_iSup, AEMeasurable.biInf, MeasureTheory.OuterMeasure.trim_eq_iInf', Function.mulSupport_iSup, LieModule.coe_genWeightSpaceOf_zero, CompleteSublattice.sInfClosed, SimpleGraph.chromaticNumber_eq_iInf, Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub, CategoryTheory.GrothendieckTopology.closureOperator_isClosed, ENat.mul_sSup, infClosed_infClosure, SummationFilter.hasSum_symmetricIoc_int_iff, Submodule.isOrtho_sSup_right, sInfHom.continuous, Submodule.iSup_span, upperSemicontinuousOn_iInf, MeasurableSet.measure_eq_iSup_isCompact, Ordinal.sup_succ_eq_lsub, Sublocale.sInf_mem, IsCompact.sInf_mem, CategoryTheory.GrothendieckTopology.PreservesSheafification.le, Ordinal.succ_log_def, Order.bot_lt_krullDim, AlgebraicGeometry.IsLocalIso.eq_iInf, SupClosed.sSup_mem_of_nonempty, isConnected_Ici, AnalyticAt.meromorphicOrderAt_nonneg, Ordinal.sSup_ord, topologicalKrullDim_subspace_le, AddSubmonoid.FG.iSup, Int.ball_eq_Ioo, essSup_eq_sInf, MeasureTheory.upperCrossingTime_le_lowerCrossingTime, MeasureTheory.Content.outerMeasure_eq_iInf, TopCat.Presheaf.SheafConditionEqualizerProducts.w, csSup_one, CompleteLattice.isCompactElement_iff_exists_le_iSup_of_le_iSup, MeasureTheory.dense_of_generateFrom_isSetSemiring, NonarchimedeanAddGroup.exists_openAddSubgroup_separating, TopologicalSpace.Clopens.coe_disjoint, essInf_count, topologicalKrullDim_zero_of_discreteTopology, Module.End.iSup_genEigenspace_eq, Set.isCoatom_iff, MeasureTheory.hitting_eq_end_iff, Monotone.Iio, EisensteinSeries.tendsto_e2Summand_atTop_nhds_zero, AddSubmonoid.mul_iSup, Ordinal.enumOrd_zero, ciInf_mem, ENNReal.smul_iSup, Order.krullDim_eq_iSup_coheight_of_nonempty, IntermediateField.sInf_toSubalgebra, ENNReal.iSup_add, sSup_inv, Submodule.iSup_dualAnnihilator_le_iInf, Subgroup.FG.biSup_finset, ENat.coe_sSup, ENNReal.iInf_mul_of_ne, SummationFilter.hasSum_symmetricIcc_iff, MeasureTheory.measure_biUnion_eq_iSup, RootPairing.coe_chainTopCoeff_eq_sSup, supClosure_empty, Ordinal.iSup_mul_nat, ClosedSubmodule.toSubmodule_iSup, BooleanSubalgebra.sSup_mem, Submodule.sum_mem_iSup, sSup_mul, ENNReal.tsum_iSup_eq, ENat.sInf_eq_zero, isInducing_sumElim, BoxIntegral.Box.Ioo_ae_eq_Icc, Submodule.mem_iSup_iff_exists_dfinsupp, isOpen_sSup_iff, LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute, compl_image_latticeClosure, Submodule.span_range_eq_iSup, Order.krullDim_eq_iSup_length, Order.Ideal.PrimePair.isCompl_I_F, Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim, TopologicalSpace.Opens.gc, IntermediateField.sSup_def, MeasureTheory.OuterMeasure.map_iInf_le, Ideal.IsHomogeneous.iSup, PrimitiveSpectrum.gc_closureOperator, Finset.Nonempty.ciSup_mem_image, Order.coheight_pos_of_lt_top, egauge_pi, WithTop.iInf_coe_eq_top, AlgebraicGeometry.iSup_basicOpen_of_span_eq_top, ENNReal.add_iInf, upperHemicontinuousOn_iff_preimage_Iic, Submodule.iSup_eq_range_dfinsupp_lsum, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_W, Set.Nonempty.ciSup_lt_iff, Monoid.CoprodI.range_eq_iSup, sInf_mul, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, induced_sInf, sInf_neg, infClosure_singleton, Order.coheight_eq_coe_iff_maximal_le_coheight, ENat.ceil_le, csInf_le', MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq, Partition.sSup_eq', NNReal.agm_eq_ciSup, DFinsupp.iSup_range_lsingle, RootPairing.setOf_root_add_zsmul_eq_Icc_of_linearIndependent, SetTheory.PGame.grundyValue_eq_sInf_moveRight, ENNReal.toNNReal_iSup, Partition.le_of_mem, Antitone.measure_iUnion, SetTheory.PGame.grundyValue_le_of_forall_moveLeft, Order.height_pos_of_bot_lt, Submonoid.iSup_map_mulSingle, PrimeSpectrum.iInf_localization_eq_bot, HomogeneousIdeal.toIdeal_sSup, ENNReal.tsum_eq_iSup_nat', Set.isAtom_singleton, Metric.ediam_eq_sSup, NatOrdinal.not_lt_zero, ENNReal.inv_iSup, sInf_inv, TopCat.nonempty_isLimit_iff_eq_induced, ENat.ceil_lt, MeasureTheory.OuterMeasure.iInf_apply, Filter.liminf_eq_sSup_sInf, Finset.sup'_eq_csSup_image, OrthogonalFamily.isInternal_iff, SimpleGraph.edist_pos_of_ne, MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiffUnion, NonUnitalStarAlgebra.mem_iInf, Set.monotone_accumulate, tendsto_nhds_iff_meromorphicOrderAt_nonneg, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, CompleteSublattice.sInfClosed', Topology.IsInducing.disjoint_of_sumElim_aux, SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf, latticeClosure_prod, isPreconnected_Icc, CompletePseudometrizable.iInf, ContinuousOn.image_uIcc_eq_Icc, SequentialSpace.iSup, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, separated_by_isOpenEmbedding, Setoid.eqv_classes_disjoint, continuousInv_sInf, Monotone.Ico, InfClosed.infClosure_eq, NumberField.isTotallyReal_iSup, Ordinal.sup_le_lsub, Ordinal.iSup_add_natCast, ENat.ceil_pos, EisensteinSeries.hasSum_e2Summand_symmetricIco, Set.einfsep_insert, MeasureTheory.hitting_le, ENat.add_sSup, Filter.blimsup_eq_iInf_biSup, ENNReal.tsum_eq_iSup_sum, Sublattice.le_comap_iSup, Order.krullDim_nonpos_of_subsingleton, LinearOrderedField.inducedOrderRingHom_toFun, Ordinal.IsNormal.map_iSup, NNReal.sSup_of_not_bddAbove, iSupIndep_def'', Antitone.Iio, Padic.AddValuation.map_add, Order.coheight_eq_iSup_head_eq, Ordinal.card_iSup_Iio_le_card_mul_iSup, TopologicalSpace.secondCountableTopology_iInf, Algebra.iSup_toSubsemiring, cbiInf_eq_of_not_forall, upperHemicontinuousAt_iff_preimage_Iic, ENat.ceil_add_le, LocallyConvexSpace.iInf, ENat.lt_ceil, TopCat.Sheaf.existsUnique_gluing, exists_nhds_disjoint_closure, LinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap, MeasureTheory.OuterMeasure.biInf_apply, Nat.iInf_le_succ, Submodule.isOrtho_iSup_left, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp, ENNReal.iInf_add, ProbabilityTheory.bayesRisk_const_of_nonempty, ENat.coe_iSup, ENat.smul_iSup, iSup_le_iSup_of_partialSups_le_partialSups, PartENat.toWithTop_le, Finite.le_ciSup, Finset.Nonempty.csSup_mem, IsInducing.topologicalKrullDim_le, MeasureTheory.IsSetSemiring.diff_mem_supClosure, ENNReal.mul_iInf', SupClosed.iSup_mem_of_nonempty, MeasureTheory.hittingAfter_eq_top_iff, LinearMap.ker_noncommProd_eq_of_supIndep_ker, continuousSMul_sInf, infClosure_eq_self, ProbabilityTheory.indep_iSup_limsup, MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le, Cardinal.mul_ciSup, AddSubmonoid.mem_bsupr_iff_exists_dfinsupp, generateFrom_iUnion, csInf_Ioi, IsCompact.lt_sInf_iff_of_continuous, CategoryTheory.PreZeroHypercover.presieve₀_restrictIndex_le, normalClosure_def, MeasureTheory.Filtration.rightCont_apply, tsum_iSup_decode₂, meromorphicNFAt_iff_analyticAt_or, NNReal.iSup_pow_of_ne_zero, compl_image_latticeClosure_eq_of_compl_image_eq_self, Order.krullDim_eq_iSup_height_of_nonempty, EMetric.infEdist_biUnion, MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral, latticeClosure_singleton, ENNReal.iInf_add_iInf_of_monotone, Nimber.small_Ioo, Submodule.restrictScalars_sSup, Ordinal.sup_eq_bsup, Cardinal.ciSup_mul, setOf_isPreconnected_eq_of_ordered, coinduced_sSup, MeasurableSpace.measurableSpace_iSup_eq, Set.einfsep_insert_le, LinearMap.mem_span_iff_continuous_of_finite, Ordinal.Principal.iSup, ENat.sub_iSup, ENat.iInf_eq_top_of_isEmpty, Function.support_iInf, CompleteSublattice.codisjoint_iff, PrimeSpectrum.zeroLocus_iSup, Set.Nonempty.csSup_mem, Cardinal.ord_eq_Inf, MeasureTheory.hittingAfter_univ, ENNReal.biSup_add', ENat.floor_lt_ceil, iSupIndep_def', le_ciInf_iff', Submodule.toAddSubmonoid_sSup, csSup_empty, ENat.iInf_coe_eq_top, WithTop.iSup_coe_lt_top, ENNReal.iSup_add_iSup, Submodule.smul_iSup, lowerSemicontinuous_iSup, exists_open_nhds_disjoint_closure, untrop_sum, ENat.floor_lt_top, ENNReal.iSup_sub, ENNReal.tsum_eq_iSup_sum', disjoint_measurableAtom_of_notMem, AddSubgroup.ofAddUnits_sSup, MeasureTheory.disjoint_cylinder_iff, CompleteSublattice.isCompl_iff, MonotoneOn.Iic, isAtomic_of_complementedLattice, MeasureTheory.hittingBtwn_apply_mono_left, Subalgebra.unop_sSup, isPreconnected_Ioi, MeasureTheory.hittingBtwn_anti, MvPowerSeries.le_weightedOrder_subst, CategoryTheory.MorphismProperty.retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp, ENat.gc_ceil_toENNReal, NFA.disjoint_evalFrom_reverse_iff, MeasureTheory.measure_sigmaFiniteSetWRT', Filter.bliminf_sup_le_inf_aux_left, ENat.exists_eq_iInf, IsCompact.measure_eq_iInf_isOpen, UniformOnFun.topologicalSpace_eq, ENNReal.sub_eq_sInf, Ordinal.opow_limit, Finset.Nonempty.csInf_eq_min', MeasureTheory.OuterMeasure.ofFunction_eq_iInf_mem, infClosure_univ, Submodule.fg_iSup, SSet.skeleton_succ, MeasureTheory.Filtration.rightCont_def, Cardinal.preAleph_limit, sSup_atoms_eq_top, SSet.Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top, IsSemisimpleModule.finite_tfae, subset_latticeClosure, Filter.bliminf_sup_le_inf_aux_right, LinearPMap.domain_sSup, Order.height_eq_iSup_lt_height, Order.height_eq_coe_add_one_iff, GroupTopology.toTopologicalSpace_sInf, AffineSubspace.direction_iInf_of_mem, dimH_eq_iInf, continuousAdd_iInf, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion_of_mem, subset_infClosure, MeasureTheory.Measure.sInf_apply, ENNReal.le_iInf_mul, regularSpace_iInf, Submodule.inf_iSup_genEigenspace, Sublocale.coe_sInf, Ideal.iSup_mul, IsClosedEmbedding.topologicalKrullDim_le, continuous_iSup_dom, disjoint_frontier_iff_isOpen, equicontinuous_iInf_dom, NormedSpace.equicontinuous_TFAE, Order.krullDim_enat, isTotallyDisconnected_iff_lt, MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion, Order.height_le_coe_iff, IsGenericPoint.disjoint_iff, IsOpen.measure_eq_iSup_isCompact, PiLp.nnnorm_eq_ciSup, NatOrdinal.mul_le_iff, Cardinal.lift_iSup_le_sum, CompleteLattice.isSupClosedCompact_iff_wellFoundedGT, Monotone.measure_iInter, Order.height_eq_coe_iff, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot', MeasureTheory.Measure.inf_apply, Algebra.sSup_toSubsemiring, MeasureTheory.hittingAfter_apply_anti, generateFrom_iInter, generateFrom_piiUnionInter_measurableSet, MeasureTheory.IsSetSemiring.diff_eq_sUnion', sInf_one, ENNReal.iSup_ennreal, AntitoneOn.Ioi, Antitone.pairwise_disjoint_on_Ioc_succ, SimpleGraph.edist_le_eccent, alexandrovDiscrete_iSup, partialSups_eq_biSup, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.exists_oneHypercover, InfClosed.biInf_mem_of_nonempty, IsIntegrallyClosed.iInf, isPreconnected_Ico, SimpleGraph.edist_triangle, NonUnitalSubalgebra.coe_iSup_of_directed, InfClosed.iInf_mem_of_nonempty, Filter.Realizer.mem_sets, Sublocale.sInf_mem', AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom, CompleteSublattice.coe_sSup', upperSemicontinuous_iInf, RootPairing.Base.not_nonpos_iff_pos_of_sum_mem_range_root, tprod_iSup_decode₂, WithTop.iInf_coe_lt_top, exists_seq_infinite_isOpen_pairwise_disjoint, ENat.coe_iInf, ProbabilityTheory.condIndep_iSup_limsup, dimH_bUnion, Order.pred_eq_sSup, BooleanSubalgebra.latticeClosure_subset_closure, Antitone.Ioi, TopologicalSpace.Opens.mem_iSup, Cardinal.sum_le_lift_mk_mul_iSup, ConditionallyCompleteLinearOrderedField.to_archimedean, ENNReal.inv_iInf, Ordinal.bsup_eq_sup, Order.length_le_height, ENat.mul_iInf_of_ne, IsUltrametricDist.ball_eq_or_disjoint, eq_Icc_of_connected_compact, EMetric.infEdist_iUnion, continuous_sInf_dom, ProbabilityTheory.Kernel.indep_iSup_of_directed_le, Subfield.closure_sUnion, Multiset.iSup_mem_map_of_ne_zero, sInf_mem_closure, UniformSpace.toTopologicalSpace_sInf, BooleanSubalgebra.closure_latticeClosure, essSup_eq_iSup, ENNReal.toNNReal_iInf, sSupHom.continuous, Order.height_le_height_apply_of_strictMono, upperHemicontinuous_iff_isOpen_preimage_Iic, Subalgebra.unop_iInf, MeasureTheory.inducedOuterMeasure_eq_iInf, MeasureTheory.lintegral_iInf, MeasureTheory.le_iInf_lintegral, NonUnitalAlgebra.coe_iInf, upperHemicontinuous_iff_preimage_Iic, NNReal.le_iInf_mul_iInf, ENNReal.le_iInf_mul_iInf, BoxIntegral.Prepartition.pairwiseDisjoint, Antitone.Ici, ciSup_or', trdeg_eq_iSup_cardinalMk_isTranscendenceBasis, ProbabilityTheory.Kernel.indep_iSup_of_monotone, NatOrdinal.instAddLeftStrictMono, Metric.ball_disjoint_closedBall, Order.krullDim_le_one_iff_of_boundedOrder, sSup_one, Ordinal.iSup_mul_natCast, Ordinal.mem_closure_iff_iSup, Filter.HasBasis.liminf_eq_iSup_iInf, Algebra.iInf_toSubsemiring, AntitoneOn.Iic, Cardinal.sInf_eq_zero_iff, sInf_iUnion_Ici, CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.le, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot, PolynormableSpace.iInf, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, NNReal.iSup_div, Set.Finite.supClosure, Ideal.iSup_iInf_eq_top_iff_pairwise, Set.Iic.coe_iInf, MeasureTheory.measure_iUnion_of_tendsto_zero, Submodule.closure_coe_iSup_map_single, ENat.iSup_natCast, Ordinal.iSup_lt_ord_lift, TopCat.coinduced_of_isColimit, Filter.Realizer.ofEquiv_F, Pi.Colex.sInf_apply_le, ciSup_of_empty, MeasureTheory.Filtration.rightCont_eq_of_not_isMax, CategoryTheory.ObjectProperty.HasCardinalLT.iSup, topologicalGroup_sInf, MeasureTheory.tendsto_ae_condExp, ProbabilityTheory.bayesRisk_le_iInf, ProbabilityTheory.indep_iSup_directed_limsup, DividedPowers.SubDPIdeal.sSup_carrier_def, TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompact, ContinuousOn.image_uIcc, PiLp.edist_eq_iSup, CauchyFilter.monotone_gen, Set.isCoatom_singleton_compl, AddMonoidHom.noncommPiCoprod_mrange, Manifold.riemannianEDist_def, Finset.Nonempty.csSup_eq_max', IsSemisimpleModule.sSup_simples_le, isOpen_iSup_iff, ENat.floor_mono, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone', IsOpen.measure_eq_biSup_integral_continuous, CompleteLattice.IsSupClosedCompact.wellFoundedGT, Submodule.sInf_orthogonal, CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition, Ordinal.cof_eq_sInf_lsub, Submonoid.inv_iSup, MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup, LinearOrderedField.inducedMap_mono, SupClosed.biSup_mem, setOf_isPreconnected_subset_of_ordered, ProbabilityTheory.iSup_partitionFiltration_eq_generateFrom_range, connectedComponent_disjoint, ENat.le_ceil, Submodule.mul_iSup, Order.krullDim_eq_iSup_coheight, Set.Iic.coe_biInf, Set.Iic.coe_sSup, ENNReal.add_iSup, AlgebraicGeometry.Scheme.IdealSheafData.support_iSup, OrderIso.map_ciSup', TopCat.Presheaf.presieveOfCovering.indexOfHom_spec, ENNReal.iSup_coe_eq_top, Subfield.mem_iSup_of_directed, sup_mem_supClosure, ProbabilityTheory.condIndep_biSup_limsup, sSupIndep.disjoint_sSup, SimpleGraph.ediam_le_two_mul_radius, lowerBounds_infClosure, isPreconnected_Ioc, gc_nhdsKer_interior, StarSubalgebra.mem_iInf, Submodule.span_sSup, ProperlyDiscontinuousSMul.exists_nhds_disjoint_image, SimpleGraph.edist_eq_sInf, Filter.bliminf_eq, Submodule.iSup_eq_span, ENat.iSup_mul, Filter.liminf_eq_iSup_iInf_of_nat, Ordinal.mem_closure_tfae, Cardinal.iSup_lt_ord_lift_of_isRegular, isPreconnected_Ioo, SeparatedNhds.disjoint_closure_right, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π, Submodule.span_iUnion, CompleteLattice.isCoatomistic_iff, SummationFilter.hasProd_symmetricIco_int_iff, MeasureTheory.hittingBtwn_mono_right, BoundedContinuousFunction.nndist_eq_iSup, monotone_Iio, SummationFilter.hasSum_symmetricIco_int_iff, SimpleGraph.eccent_le_ediam, supClosure_isClosed, LieSubmodule.sSup_toSubmodule, MeasureTheory.OuterMeasure.sSup_apply, NNReal.natCast_iSup, Order.pred_eq_iSup, Ideal.map_iSup_comap_of_surjective, AffineSubspace.direction_iInf, AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom, SimpleGraph.ediam_eq_iSup_iSup_edist, Cardinal.iSup_lt_lift_of_isRegular, CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating.le, CategoryTheory.Presieve.le_of_factorsThru_sieve, Ordinal.iSup'_eq_bsup, Pi.induced_precomp, Set.isAtom_iff, Measurable.sInf, Set.indicator_iInter_apply, Monotone.Ioc, Submodule.sum_mem_biSup, Matrix.ker_diagonal_toLin', Nimber.not_bddAbove_compl_of_small, Order.krullDim_eq_iSup_height, AddSubmonoid.FG.biSup, Finset.coe_covBy_coe, FirstOrder.Language.Substructure.iSup_eq_closure, ContinuousLinearMap.sSup_unit_ball_eq_nnnorm, UniformSpace.toTopologicalSpace_iInf, UniformOnFun.edist_def', MeasureTheory.tendsto_measure_sigmaFiniteSetGE, CompleteSublattice.coe_iSup, Nat.iInf_lt_succ, MeasurableSpace.comap_iSup, SimpleGraph.eccent_pos_iff, ClosedSubmodule.mem_iSup, Topology.IsScott.instUnivSetOfIsUpper, Filter.HasBasis.liminf_eq_sSup_univ_of_empty, Subalgebra.op_iInf, AddSubgroup.FG.iSup, Filter.limsSup_eq_iInf_sSup, smul_iInf_le, IsSemisimpleModule.sSup_simples_eq_top, hasCardinalLT_subtype_iSup, iSup_disjointed, ENat.sSup_add, Cardinal.beth_limit, supClosure_singleton, Function.support_iSup, Module.End.genEigenspace_eq_iSup_genEigenspace_nat, trop_iInf, Order.coheight_le_coheight_apply_of_strictMono, AlgebraicGeometry.Scheme.Hom.image_iSup, image_latticeClosure, Alexandrov.lowerCone_π_app, ENNReal.biSup_add_biSup_le', Cardinal.mk_biUnion_le, MeasureTheory.lintegral_iSup_directed_of_measurable, MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part, Subfield.map_iSup, latticeClosure_eq_self, AddSubgroup.ofAddUnits_iSup₂, Algebra.iInf_toSubmodule, IntermediateField.map_iSup, iSup_eq_iSup_of_partialSups_eq_partialSups, CFilter.mem_toFilter_sets, Submodule.spanRank_toENat_eq_iInf_finset_card, IntermediateField.map_iInf, isSaddlePointOn_iff', latticeClosure_empty, NatOrdinal.instAddLeftMono, Ordinal.iSup_sequence_lt_omega_one, ProbabilityTheory.Kernel.indep_biSup_limsup, BoxIntegral.Box.Ioo_subset_Icc, SimpleGraph.edist_anti, ENNReal.mul_sSup, ENNReal.iSup_add_iSup_of_monotone, Filter.mono_bliminf', sSup_div, ENNReal.mul_iInf_of_ne, le_csInf_iff', IsCompact.isGLB_sInf, BoxIntegral.Box.exists_seq_mono_tendsto, MonoidHom.noncommPiCoprod_mrange, MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE', SimpleGraph.ComponentCompl.hom_eq_iff_not_disjoint, Finset.untrop_sum, supClosure_mono, ENat.coe_sInf, Ideal.IsHomogeneous.sSup, Set.Iic.instIsCompactlyGenerated, ENNReal.sSup_mul, TopologicalSpace.Opens.map_iSup, ENNReal.iSup_zero, PartENat.ofENat_lt, continuousAdd_sInf, t2_separation_compact_nhds, Order.one_le_krullDim_iff, Submonoid.FG.iSup, sInf_zero, IndexedPartition.disjoint, LocallyConvexSpace.sInf, Cardinal.sum_le_iSup_lift, Set.einfsep_eq_iInf, IsWellFounded.rank_eq, SSet.horn_eq_iSup, Ordinal.iSup_typein_limit, lowerHemicontinuous_iff_isClosed_preimage_Iic, ENat.iSup_eq_zero, Nimber.not_lt_zero, Measurable.iSup', MeasureTheory.tendsto_eLpNorm_condExp, Ordinal.iSup_lt_lift, AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj, NonUnitalAlgebra.map_iInf, MeasureTheory.lintegral_eq_nnreal, UniformFun.edist_def, MeasureTheory.hittingAfter_eq_sInf, Cardinal.mk_iUnion_le_lift, Order.coheight_le_iff', Order.krullDim_le_of_strictMono, SSet.range_eq_iSup_sigma_ι, SupClosed.supClosure_eq, essInf_eq_sSup, WithTop.isGLB_sInf, Subspace.dualAnnihilator_iInf_eq, ENNReal.iInf_mul_iInf, IntermediateField.isSplittingField_iSup, Submodule.iSup_map_single, MeasureTheory.SimpleFunc.lintegral_restrict_iUnion_of_directed, Submodule.mem_sSup_of_mem, NNReal.le_mul_iInf, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion, ProbabilityTheory.iSup_countableFiltration, ExpGrowth.expGrowthInf_iInf, completelyRegularSpace_iInf, PrimitiveSpectrum.closedsGC_closureOperator, Monotone.pairwise_disjoint_on_Ico_pred, Order.pred_eq_csSup, ClosedSubmodule.toSubmodule_sSup, ProbabilityTheory.indep_iSup_of_antitone, FirstOrder.Language.Substructure.closure_iUnion, ConditionallyCompleteLinearOrder.isCompact_Icc, Ordinal.derivFamily_limit, continuousSMul_iInf, BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm, Nimber.small_Ioc, coinduced_iSup, monotone_Iic, MeasureTheory.OuterMeasure.sInf_apply, IsTopologicalBasis.iInf, MeasureTheory.iInf_le_lintegral, AntitoneOn.Ioo, Partition.iSup_eq, ZFSet.rank_range, IntermediateField.iSup_eq_adjoin, TopologicalSpace.Opens.mem_sSup, iSup₂_iInf₂_le_iInf₂_iSup₂, ENNReal.add_biSup', LinearMap.IsSymmetric.iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute, Cardinal.succ_def, NonUnitalStarAlgebra.coe_iInf, PartENat.withTopEquiv_le, ProperlyDiscontinuousVAdd.exists_nhds_disjoint_image, EisensteinSeries.tsum_tsum_symmetricIco_sub_eq, Submodule.map_smul', Monotone.pairwise_disjoint_on_Ioo_succ, Ordinal.iSup_ord, inf_sSup_eq_iSup_inf_sup_finset, Metric.AreSeparated.disjoint, ENNReal.iInf_ne_top, ENNReal.hasSum, BoxIntegral.Box.disjoint_coe, IntermediateField.iSup_toSubfield, NNReal.iInf_real_pos_eq_iInf_nnreal_pos, ENat.iSup_add, Ordinal.sup_eq_sup, PartENat.withTopEquiv_lt, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf, TopologicalSpace.Opens.leSupr_apply_mk, LinearMap.range_smul', StieltjesFunction.length_eq, csInf_one, MeasureTheory.Filtration.rightCont_eq, DirectSum.IsInternal.addSubmonoid_iSup_eq_top, DFA.pumping_lemma, ENNReal.add_sSup, Submodule.small_iSup, Finsupp.disjoint_lsingle_lsingle, Ordinal.le_iSup, MeasureTheory.measure_eq_iInf', le_csInf_iff'', ENNReal.iInf_mul', Nimber.small_Icc, MeasureTheory.lintegral_iInf_directed_of_measurable, Ordinal.iSup_eq_zero_iff, LinearOrderedField.inducedOrderRingIso_symm, AddSubgroup.FG.biSup_finset, Pi.induced_restrict_sUnion, Set.mulIndicator_iInter_apply, FirstOrder.Language.Substructure.comap_iSup_map_of_injective, ProbabilityTheory.condIndep_biSup_compl, MeasureTheory.hitting_mono, CompleteSublattice.sSupClosed, Cardinal.sInf_empty, Continuous.strictMono_of_inj, Finsupp.codisjoint_supported_supported_iff, Metric.infEDist_iUnion, IsCompactlyGenerated.exists_sSup_eq, Set.Iic.coe_iSup, iSupIndep_def, T2Space.t2, Module.End.genEigenspace_top, Monotone.Ioi, infClosure_min, ENNReal.iSup_div, Set.Nonempty.ciSup_mem_image, MonoidHom.noncommPiCoprod_range, Monoid.CoprodI.iSup_mrange_of, Submodule.iSup_torsionBy_eq_torsionBy_prod, sSup_neg, UniformOnFun.edist_def, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_map, IntermediateField.fg_iSup, MeasureTheory.Measure.iInf_rat_gt_prod_Iic, IsCompactlyGenerated.BooleanGenerators.sSup_le_sSup_iff_of_atoms, MeasurableSpace.map_iInf, MeasureTheory.OuterMeasure.boundedBy_apply, Metric.closedBall_disjoint_ball, ProbabilityTheory.iSup_bayesRisk_le_minimaxRisk, SSet.hasDimensionLT_iSup_iff, equicontinuousAt_iInf_dom, ENat.ceil_mono, CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_llp_rlp, iSup_succ, Ordinal.sup_eq_bsup', Submodule.set_smul_eq_iSup, ProbabilityTheory.condIndep_iSup_directed_limsup, MeasureTheory.OuterMeasure.restrict_biInf, TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible, IntermediateField.adjoin_iUnion, AntitoneOn.Iio, Ordinal.succ_iSup_eq_lsub_iff, ENat.mul_iInf, LieSubmodule.sSup_toSubmodule_eq_iSup, CompleteSublattice.coe_sSup, isConnected_Iic, Filter.Realizer.le_iff, SimpleGraph.diam_def, Subgroup.FG.iSup, ENat.sSup_mul, Cardinal.sum_le_lift_mk_mul_iSup_lift, ENat.iSup_coe_eq_top, latticeClosure_idem, sSup_sub, ClosedSubmodule.mem_sSup, t2Space_iff_nhds, IntermediateField.normalClosure_def'', SSet.iSup_skeletonOfMono, DividedPowers.isSubDPIdeal_iSup, Nimber.small_Iic, Sublattice.map_iSup, MeasureTheory.hittingAfter_mem_set_of_ne_top, ProbabilityTheory.bayesRisk_le_iInf', Monotone.pairwise_disjoint_on_Ioo_pred, CategoryTheory.MorphismProperty.retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp, CompleteLattice.IsSupFiniteCompact.wellFoundedGT, BoundedContinuousFunction.edist_eq_iSup, RootPairing.Base.exists_root_eq_sum_int, Filter.liminf_eq_iSup_iInf, Filter.HasBasis.liminf_eq_sSup_iUnion_iInter, Ideal.homogeneousCore'_eq_sSup, TopologicalSpace.Opens.iSup_def, TopologicalSpace.Closeds.coe_sSup, Monotone.pairwise_disjoint_on_Ioc_succ, Ordinal.sup_eq_lsub, Nimber.one_le_iff_ne_zero, ExpGrowth.expGrowthInf_biInf, Ordinal.lift_card_sInf_compl_le, RootPairing.root_add_zsmul_mem_range_iff, sSupIndep_pair, SimpleGraph.edist_le_ediam, OrthogonalFamily.range_linearIsometry, iSup_Iio_eq_self_iff_isSuccPrelimit, Ordinal.iSup_eq_lsub_iff_lt_iSup, continuous_iSup_rng, ProbabilityTheory.Kernel.indep_iSup_of_antitone, ENNReal.toReal_sSup, sSup_compact_le_eq, isPreconnected_Iio, ENNReal.sub_iSup, Order.coheight_le_coe_iff, SSet.iSup_range_eq_top_of_isColimit, ContinuousMap.nnnorm_eq_iSup_nnnorm, Antitone.measure_iInter, AffineSubspace.direction_sInf, Function.mulSupport_iInf, Submodule.isOrtho_iSup_right, IsClosed.lowerClosure, partialSups_eq_ciSup_Iic, Algebra.isIntegral_iSup, Topology.IsScott.scott_eq_upper_of_completeLinearOrder, MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup, WithBot.coe_biInf, EisensteinSeries.tendsto_double_sum_S_act, Ordinal.IsNormal.map_iSup_of_bddAbove, SummationFilter.symmetricIcc_eq_symmetricIoo_int, InfClosed.biInf_mem, MeasurableSpace.measurableSet_sInf, AlgebraicGeometry.IsAffineOpen.biSup_of_disjoint, Cardinal.preBeth_limit, IsCompact.continuous_sInf, Submodule.iSup_smul, Submodule.mem_iSup_finset_iff_exists_sum, ProbabilityTheory.bayesRisk_const_of_neZero, Submodule.iSup_eq_span', MeasureTheory.measure_eq_iInf, disjoint_principal_nhdsSet, Filter.Realizer.principal_F, infClosure_prod, MeasureTheory.hittingBtwn_le, MeasureTheory.le_iInf₂_lintegral, upperSemicontinuousOn_biInf, Submodule.iInf_orthogonal, ProjectiveSpectrum.basicOpen_eq_union_of_projection, MeasureTheory.Measure.iSup_restrict_spanningSets, ContinuousMap.nndist_eq_iSup, FirstOrder.Language.Substructure.map_iSup_comap_of_surjective, NonUnitalStarSubalgebra.coe_iSup_of_directed, Subalgebra.op_iSup, disjointed_eq_inf_compl, ENNReal.le_iInf_add_iInf, AddSubmonoid.FG.biSup_finset, MeasureTheory.lintegral_iSup, induced_to_pi, Int.closedBall_eq_Icc, Ordinal.lt_iSup_iff, iSupIndep.iInf, CategoryTheory.GrothendieckTopology.le_close, Set.antitone_dissipate, ENNReal.iInf_mul, Ordinal.IsNormal.map_sSup_of_bddAbove, MeasureTheory.hittingBtwn_eq_sInf, continuousMul_iInf, TopologicalSpace.Opens.coe_sSup, ENNReal.toReal_iInf, Order.krullDim_le_one_iff_forall_isMax, NatOrdinal.zero_le, IntermediateField.normal_iInf, AffineSubspace.direction_sInf_of_mem, RootedTree.subtrees_disjoint, EisensteinSeries.summable_e2Summand_symmetricIcc, ENNReal.iSup_eq_zero, MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrict, ENNReal.sInf_add, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.top_mem_range, Ordinal.bsup'_eq_iSup, ENat.floor_lt, Submodule.span_sSup', Ordinal.IsNormal.apply_omega0, Filter.bliminf_or_le_inf_aux_left, Sublocale.iInf_mem, MeasurableSet.measure_eq_iSup_isClosed_of_ne_top, ENNReal.iInf_coe_lt_top, Metric.eball_disjoint, Order.krullDim_pos_iff_of_orderTop, TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology, TopCat.induced_of_isLimit, TopologicalSpace.IsOpenCover.iSup_eq_top, Nimber.mul_def, MeasureTheory.eLpNormEssSup_count, ProbabilityTheory.bayesRisk_const, SimpleGraph.radius_le_ediam, Subfield.coe_sSup_of_directedOn, TopologicalSpace.Closeds.iInf_mk, Ordinal.iSup_Iio_eq_bsup, WithTop.iSup_coe_eq_top, NNReal.coe_iInf, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt, MeasureTheory.OuterMeasure.iUnion_of_tendsto_zero, AEMeasurable.iSup, TopCat.Presheaf.SheafConditionEqualizerProducts.w_apply, WithTop.isLUB_sSup, ENNReal.smul_sSup, Submodule.map_iSup_comap_of_surjective, Submodule.coe_iSup_of_directed, IntermediateField.finiteDimensional_iSup_of_finite, SimpleGraph.chromaticNumber_eq_biInf, Ordinal.iSup_eq_of_range_eq, MeasureTheory.hittingBtwn_eq_end_iff, Set.Finite.latticeClosure, Order.coheight_coe_enat, ZFSet.rank_iUnion, ENNReal.sSup_add, Ordinal.IsNormal.map_sSup, continuous_iInf_dom, Topology.IsScott.isOpen_iff_Iic_compl_or_univ, StarSubalgebra.sInf_toSubalgebra, CategoryTheory.MorphismProperty.transfiniteCompositions_le, TopologicalSpace.gc_generateFrom, BooleanSubalgebra.biSup_mem, TopologicalSpace.Closeds.isAtom_coe, SimpleGraph.eccent_le_iff, MeasureTheory.upperCrossingTime_zero', MaximalSpectrum.iInf_localization_eq_bot, MeasureTheory.iSup₂_lintegral_le, Order.krullDim_eq_iSup_height_add_coheight_of_nonempty, Ordinal.iSup_sequence_lt_omega1, Filter.HasBasis.blimsup_eq_iInf_iSup, sInf_add, FiberBundle.exists_trivialization_Icc_subset, Alexandrov.projSup_obj, ENNReal.tsum_eq_iSup_nat, ENNReal.iInf₂_add, Ordinal.bsup_eq_iSup, Algebra.mem_iSup_of_mem, NFA.disjoint_stepSet_reverse, LinearOrderedField.inducedMap_nonneg, upperSemicontinuousWithinAt_biInf, isAtomistic_of_complementedLattice, essSup_count, Order.krullDim_pos_iff_of_orderBot, Partition.disjoint, MeasureTheory.Filtration.sSup_def, SimpleGraph.ediam_def, IntermediateField.isAlgebraic_iSup, normalClosure_eq_iSup_adjoin, Ordinal.lsub_le_succ_iSup, Cardinal.ciSup_mul_ciSup, Submodule.mem_iSup_of_mem, Filter.limsup_eq_iInf_iSup, Nimber.small_Ico, Cardinal.lift_sInf, AEMeasurable.biSup, MeasureTheory.OuterMeasure.top_apply', Filter.limsup_le_iSup, Order.succ_eq_csInf, IsUltrametricDist.closedBall_subset_trichotomy, SupClosed.sSup_mem, MonotoneOn.Ico, Measurable.iInf, Field.Emb.Cardinal.iSup_adjoin_eq_top, Filter.bliminf_antitone_filter, CliffordAlgebra.iSup_ι_range_eq_top, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup, Finset.sup'_id_eq_csSup, NNReal.iSup_empty, Ideal.mul_iSup, IntermediateField.toSubalgebra_iSup_of_directed, IsUltrametricDist.nnnorm_tprod_le, MeasureTheory.Measure.hausdorffMeasure_apply, PartENat.withTopEquiv_symm_le, AffineSubspace.comap_supr, Alexandrov.lowerCone_pt, Submodule.span_biUnion, InfClosed.iInf_mem, iSupIndep_map_orderIso_iff, ProbabilityTheory.indep_biSup_compl, IntermediateField.isSeparable_iSup, inducing_iInf_to_pi, Filter.iInf_le_liminf, AddSubmonoid.mem_iSup_iff_exists_dfinsupp', ProbabilityTheory.bayesRisk_discard, supClosure_infClosure, IntermediateField.sInf_toSubfield, ENNReal.iSup_pow, Ideal.sup_height_eq_ringKrullDim, isSaddlePointOn_iff, Set.instIsCoatomistic, Partition.bot_lt_of_mem, Ordinal.mem_iff_iSup_of_isClosed, infClosure_mono, NNReal.mul_iSup, EMetric.hausdorffEdist_def, ENNReal.sub_iInf, AddSubgroup.FG.biSup, isSeparatedMap_iff_nhds, LinearOrderedField.coe_inducedOrderRingIso, MeasureTheory.lowerCrossingTime_mono, Cardinal.add_ciSup, NonUnitalAlgebra.mem_sInf, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces, MonotoneOn.Ioc, Algebra.adjoin_iUnion, CompleteLattice.isSupFiniteCompact_iff_all_elements_compact, LieSubmodule.iSup_toSubmodule_eq_top, TopCat.nonempty_isColimit_iff_eq_coinduced, MeasureTheory.hittingAfter_le_iff, Set.measure_eq_iInf_isOpen, Ordinal.sInf_compl_lt_ord_succ, Submodule.isOrtho_sSup_left, equicontinuousOn_iInf_dom, ENNReal.iSup_lt_eq_self, MeasureTheory.OuterMeasure.sInf_apply', Ideal.map_sSup, CompleteLattice.wellFoundedGT_characterisations, Order.coheight_eq_coe_iff, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens, BoundedContinuousFunction.nndist_eq, ENNReal.finsetSum_iSup_of_monotone, NatOrdinal.small_Ioc, IsCompact.measure_eq_biInf_integral_hasCompactSupport, MeasureTheory.AddContent.supClosure_apply_of_mem, monotone_nhdsSet, Finsupp.supported_iUnion, InfClosed.supClosure, exists_eq_ciSup_of_finite, SSet.modelCategoryQuillen.J_le_monomorphisms, StarSubalgebra.coe_iInf, StarSubalgebra.mem_sInf, antitone_Ici, MeasureTheory.SimpleFunc.iSup_eapprox_apply, CategoryTheory.MorphismProperty.isStableUnderTransfiniteCompositionOfShape_iff, SimpleGraph.radius_le_eccent, Dense.ciInf', Submodule.restrictScalars_iSup, SSet.boundary_eq_iSup, ENat.toENNReal_iSup, AddSubmonoid.mem_iSup_iff_exists_dfinsupp, Ordinal.isClosed_iff_iSup, MeasureTheory.upperCrossingTime_le, Algebra.adjoin_eq_sInf, Ordinal.bsup_eq_sup', Filter.limsup_eq_iInf_iSup_of_nat', ENat.lt_floor, NatOrdinal.small_Iio, Filter.limsSup_principal_eq_sSup, LinearOrderedField.coe_lt_inducedMap_iff, csSup_Iio, InfClosed.sInf_mem_of_nonempty, isConnected_Ioi, TopologicalSpace.Opens.coe_disjoint, Finset.inf'_id_eq_csInf, MeasureTheory.hittingAfter_apply_mono, HomogeneousIdeal.irrelevant_eq_iSup, Set.Iic.coe_biSup, essInf_eq_iInf, IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top, Filter.blimsup_mono, NNReal.sInf_empty, CompleteAtomicBooleanAlgebra.instIsAtomistic, BoxIntegral.Box.measurableSet_Ioo, IsCompact.continuous_sSup, Subgroup.ofUnits_iSup₂, TopologicalSpace.Opens.isBasis_iff_cover, dimH_iUnion, NNReal.mul_iInf, EisensteinSeries.tendsto_tsum_one_div_linear_sub_succ_eq, Monotone.measure_iUnion, sSup_add, DirectSum.IsInternal.submodule_iSup_eq_top, MeasureTheory.le_hittingAfter, DoubleCoset.disjoint_out, Order.height_le_iff, Antitone.Iic, Submodule.mem_iSup_of_chain, OrderIso.apply_blimsup, NNReal.iInf_mul, MeasurableSpace.iSup_generateFrom, Submodule.mem_iSup_iff_exists_finset, Cardinal.lift_iSup_le_lift_iSup', FirstOrder.Language.DirectLimit.Equiv_isup_of_apply, MonotoneOn.Ioo, complementedLattice_iff_isAtomistic, infClosure_supClosure, CompleteLatticeHom.toOrderIsoRangeOfInjective_apply, Submodule.localized₀_iSup, untrop_sum_eq_sInf_image, Ordinal.sup_typein_limit, Filter.bliminf_or_le_inf_aux_right, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, Submodule.iSup_eq_toSubmodule_range, MeasureTheory.OuterMeasure.sInf_eq_boundedBy_sInfGen, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiff, LinearMap.iSup_range_single_le_iInf_ker_proj, Filter.Realizer.bot_F, NonUnitalAlgebra.coe_sInf, Order.KrullDimLE.krullDim_le, Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf, ProbabilityTheory.condIndep_iSup_of_disjoint, Monotone.Iic, Submodule.mem_sSup_iff_exists_finset, NatOrdinal.small_Ico, supClosure_idem, LinearMap.disjoint_single_single, List.iSup_mem_map_of_ne_nil, ENNReal.iSup_mul_le, BooleanSubalgebra.sInf_mem, CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functorToMonoOver_obj, ENat.add_biSup, NNReal.iInf_empty, Filter.liminf_top_eq_iInf, ciSup_false, Finset.inf'_eq_csInf_image, Setoid.IsPartition.pairwiseDisjoint, Padic.norm_rat_le_one_iff_padicValuation_le_one, LieSubalgebra.span_iUnion, sSupIndep_iff_pairwiseDisjoint, BooleanSubalgebra.biInf_mem, ProbabilityTheory.iSup_partitionFiltration, MeasureTheory.OuterMeasure.sInfGen_def, Filter.Realizer.top_F, PrimitiveSpectrum.hull_sSup, EisensteinSeries.summable_e2Summand_symmetricIco, Finset.Nonempty.csInf_mem, Directed.measure_iInter, RootPairing.root_sub_zsmul_mem_range_iff, Pi.induced_precomp', ENat.mul_iInf', Partition.sSup_eq, Filter.blimsup_sup_le_or, Subgroup.ofUnits_sSup, NatOrdinal.small_Ioo, Order.coheight_anti, Cardinal.sum_le_iSup, infClosure_idem, EMetric.diam_eq_sSup, Filter.limsInf_principal_eq_sInf, continuousInv_iInf, Module.End.iSup_maxGenEigenspace_eq_top, Nat.iSup_lt_succ, MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring, NNReal.le_iInf_add_iInf, CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup, CompleteSublattice.disjoint_iff, Measurable.sSup, Order.height_mono, AffineSubspace.coe_iInf, BooleanSubalgebra.iInf_mem, Ordinal.sup_eq_lsub_or_sup_succ_eq_lsub, Cardinal.iInf_eq_zero_iff, ClosedSubmodule.coe_iSup, Submodule.finite_iSup, Order.height_le_iff', Order.krullDim_nonneg, upperHemicontinuous_iff_isClosed_compl_preimage_Iic_compl, Finsupp.lsingle_range_le_ker_lapply, Monotone.Icc, MeasureTheory.measure_iUnion_eq_iSup_accumulate, WCovBy.finset_coe, lowerSemicontinuousAt_iSup, FirstOrder.Language.DirectLimit.iSup_range_of_eq_top, MeasureTheory.SimpleFunc.iSup_approx_apply, BoxIntegral.Prepartition.disjoint_coe_of_mem, Cardinal.lift_iSup_le_iff, Filter.blimsup_eq_iInf_biSup_of_nat, SSet.Subcomplex.preimage_iSup, Filter.limsup_eq_sInf_sSup, ENNReal.hasProd_iInf_prod, Pi.Colex.sInf_apply, Antitone.pairwise_disjoint_on_Ico_pred, Filter.HasBasis.limsSup_eq_iInf_sSup, Order.coheight_pos, CategoryTheory.MorphismProperty.transfiniteCompositions_pushouts_coproducts_le_llp_rlp, CompleteLattice.isAtomistic_iff, SummationFilter.symmetricIcc_eq_map_Icc_nat, Measurable.biInf, sSup_simples_eq_top_iff_isSemisimpleModule, sSup_iUnion_Iic, ENat.iInf_eq_zero, Metric.ediam_iUnion_mem_option, Submodule.span_monotone, WithBot.coe_biSup, Matrix.range_diagonal, Filter.limsup_eq_iInf_iSup_of_nat, TopologicalSpace.Closeds.coe_sInf, Submodule.mem_sSup_of_directed, Perfect.splitting, Order.index_le_height, CovBy.finset_coe, RestrictedProduct.topologicalSpace_eq_iSup, Order.coheight_eq, Metric.sphere_disjoint_ball, PrimitiveSpectrum.hull_iSup, infClosure_isClosed, Measurable.iInf_Prop, Field.Emb.Cardinal.iSup_filtration, tendsto_intCast_atTop_cobounded, Cardinal.aleph_limit, Order.krullDim_le_one_iff_forall_isMin, SummationFilter.hasProd_symmetricIcc_iff, Topology.IsLower.isTopologicalSpace_basis, bsupr_limsup_dimH, Filter.blimsup_monotone_filter, withSeminorms_iInf, ENNReal.add_iInf₂, subset_supClosure, ENat.floor_le_floor, MeasureTheory.iSup_lintegral_le, Pi.Lex.le_sSup_apply, upperSemicontinuousAt_iInf, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf, upperSemicontinuousWithinAt_iInf, Filter.limsup_eq, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top, ProjectiveSpectrum.zeroLocus_iSup_ideal, MeasureTheory.OuterMeasure.biInf_apply', Finset.Nonempty.ciSup_eq_max'_image, IsCompact.exists_sInf_image_eq, AntitoneOn.Ioc, SimpleGraph.edist_le, setOf_isOpen_sSup, disjoint_nhdsWithin_of_mem_discrete, Ordinal.iSup_le_iff, Cardinal.iSup_lt_ord_of_isRegular, finsetInf'_mem_infClosure, iSupIndep.map_orderIso, Ordinal.iSup_eq_lsub, csInf_le_csInf', Dynamics.dynEntourage_antitone, Submodule.dualAnnihilator_iSup_eq, Order.rev_index_le_coheight, AntitoneOn.Ico, Matrix.iSup_eigenspace_toLin_diagonal_eq_top, AddGroupTopology.toTopologicalSpace_iInf, Int.padicValuation_le_one, MeasureTheory.OuterMeasure.iSup_apply, SSet.N.iSup_subcomplex_eq_top, ENNReal.iSup_mul, Ordinal.iSup_eq_lsub_iff, IsCompact.exists_sSup_image_eq, Topology.IsGeneratedBy.iSup, Submonoid.FG.biSup_finset, lowerSemicontinuousWithinAt_biSup, Submodule.mem_biSup_iff_exists_dfinsupp, Filter.mono_blimsup', nhdsKer_mono, ENat.sSup_eq_zero', latticeClosure_isClosed, Cardinal.ciSup_add_ciSup, NonUnitalStarAlgebra.sInf_toNonUnitalSubalgebra, SetTheory.PGame.grundyValue_le_of_forall_moveRight, Algebra.map_iInf, isSemisimpleModule_biSup_of_isSemisimpleModule_submodule, sSupHom.apply_blimsup_le, NNReal.agm_eq_ciInf, isArtinian_iSup, ENNReal.finsetSum_iSup, MeasurableSpace.disjoint_countablePartition, TopCat.Sheaf.eq_of_locally_eq_iff, CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le, Pi.Lex.sSup_apply, Ordinal.iSup_natCast, LinearMap.mapsTo_biSup_of_mapsTo, lowerSemicontinuousAt_biSup, ENNReal.iInf_gt_eq_self, Submodule.topologicalClosure_iSup_map_single, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply, exists_disjoint_smul_of_isCompact, disjoint_nested_nhds, Filter.limsInf_eq_iSup_sInf, MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT, IntermediateField.iInf_toSubalgebra, Ordinal.iSup_iterate_eq_nfp, csInf_univ, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing, Int.instIsOrderBornology, ProbabilityTheory.condIndep_iSup_of_directed_le, DirectSum.isInternal_biSup_submodule_of_iSupIndep, NatOrdinal.small_Icc, Nimber.le_zero, Set.einfsep_iUnion_mem_option, Set.chainHeight_eq_iSup, ENNReal.toNNReal_sInf, MonotoneOn.Ioi, IsCompact.isGreatest_sSup, AddSubmonoid.neg_iSup, Subgroup.ofUnits_iSup, LinearMap.IsSymmetric.iSup_eigenspace_inf_eigenspace_of_commute, Nimber.small_Iio, Algebra.coe_sInf, MeasureTheory.OuterMeasure.trim_eq_iInf, isLUB_supClosure, ZLattice.sum_piFinset_Icc_rpow_le, ContinuousMap.enorm_eq_iSup_enorm, ENNReal.inv_sInf, PolishSpace.iInf, BooleanSubalgebra.iSup_mem, ENNReal.coe_iInf, FirstOrder.Language.Substructure.map_iSup, Ordinal.apply_omega0_of_isNormal, IntermediateField.Lifts.carrier_union, Nat.iSup_le_succ', Filter.bliminf_eq_iSup_biInf, induced_iInf, IntermediateField.normalClosure_def', Finsupp.disjoint_supported_supported_iff, StarSubalgebra.map_iInf, PrimeSpectrum.iSup_basicOpen_eq_top_iff', Set.instIsAtomistic, TopologicalSpace.Closeds.mem_iInf, NonUnitalAlgebra.sInf_toSubmodule, MeasureTheory.hitting_eq_sInf, TopCat.limit_topology, Ideal.toIdeal_homogeneousHull_eq_iSup, Submodule.mem_iSup_iff_exists_dfinsupp', Order.height_eq_iSup_last_eq, ENat.toENNReal_iInf, BoundedContinuousFunction.enorm_eq_iSup_enorm, Filter.HasBasis.limsup_eq_iInf_iSup, ExpGrowth.expGrowthSup_iSup, Order.height_enat, ProbabilityTheory.Kernel.indep_biSup_compl, supClosure_prod, MeasureTheory.OuterMeasure.map_biInf_comap, AlgebraicGeometry.Scheme.IdealSheafData.support_sSup, dimH_def, NNReal.le_iInf_mul, AddSubmonoid.iSup_mul, finsetSup'_mem_supClosure, Order.length_le_height_last, Finset.sup'_univ_eq_ciSup, Order.coheight_eq_iSup_gt_coheight, IsPreconnected.mem_intervals, tendsto_intCast_atBot_cobounded, NNReal.iSup_mul, infClosure_empty, Order.Ideal.PrimePair.disjoint, AddSubgroup.ofAddUnits_iSup, Submodule.mem_iSup_of_directed, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup, MeasureTheory.OuterMeasure.restrict_iInf_restrict, InfClosed.sInf_mem, ENNReal.tprod_eq_iInf_prod, Ordinal.lsub_le_sup_succ, MeasureTheory.AddContent.supClosure_apply, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_P, sSup_zero, iSupIndep_iff_pairwiseDisjoint, Ideal.mem_iSup_of_mem, AffineSubspace.map_iSup, MeasureTheory.AECover.iSup_lintegral_eq_of_countably_generated, MeasureTheory.OuterMeasure.ofFunction_apply, Ideal.IsHomogeneous.iSup₂, IntermediateField.coe_sInf, Ideal.Filtration.iSup_N, Submodule.iSup_toAddSubmonoid, ProbabilityTheory.bayesRisk_const', Pell.IsFundamental.y_strictMono, Dense.ciSup', NNReal.iSup_pow, Ordinal.succ_iSup_le_lsub_iff, supClosed_supClosure, R1Space.sInf, MeasureTheory.hittingAfter_anti, Order.length_le_coheight_head, Nimber.lt_one_iff_zero, NatOrdinal.small_Iic, Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W, MeasureTheory.setLIntegral_iUnion_of_directed, r1_separation, ENat.ceil_le_floor_add_one, Submodule.mem_sSup, MeasureTheory.lintegral_eq_iSup_eapprox_lintegral, ENNReal.coe_iSup, eq_sSup_atoms, PartENat.withTopEquiv_symm_lt, SummationFilter.hasProd_symmetricIoc_int_iff, StarSubalgebra.iInf_toSubalgebra, Ordinal.IsNormal.apply_of_isSuccLimit, ENNReal.iInf_div', OnePoint.isCompl_range_coe_infty, ProbabilityTheory.indep_iSup_of_disjoint, Ordinal.iSup_lt_ord, FirstOrder.Language.DirectLimit.cod_partialEquivLimit, Ideal.map_iSup, FirstOrder.Language.DirectLimit.range_lift, MeasureTheory.hittingAfter_lt_iff, PrimitiveSpectrum.gc, Antitone.Ioo, HomogeneousIdeal.toIdeal_iSup, IntermediateField.finiteDimensional_iSup_of_finset', ENat.add_biSup', csSup_zero, csInf_pair, ProbabilityTheory.Kernel.indep_iSup_of_disjoint, BooleanSubalgebra.le_comap_iSup, SSet.Subcomplex.image_iSup, LinearMap.mem_span_iff_continuous, sInf_div, Mathlib.Meta.Positivity.natCeil_pos, ENat.biSup_add, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sSup, Order.bot_lt_krullDim_iff, ENNReal.iInf_coe_eq_top, ENNReal.iSup₂_pow_of_ne_zero, MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiff, Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin, Cardinal.mk_iUnion_le, Order.height_eq_coe_iff_minimal_le_height, EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act, trop_sInf_image, supClosure_univ, Cardinal.iSup_le_sum, Projectivization.Subspace.span_iUnion, measurableSet_iSup_of_mem_piiUnionInter, Subgroup.noncommPiCoprod_range, le_iff_compact_le_imp, topologicalAddGroup_iInf, SimpleGraph.eccent_def, Cardinal.iSup_mk_le_mk_iUnion, iSup_limsup_dimH, t2_separation, DeltaGeneratedSpace.iSup, ZFSet.iSup_card_le_card_iUnion, Ordinal.card_iSup_le_sum_card, DirectSum.range_coeLinearMap, Alexandrov.projSup_map, Filter.Realizer.tendsto_iff, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π_apply, CategoryTheory.MorphismProperty.transfiniteCompositions_monotone, Cardinal.ciSup_add, WithTop.isLUB_sSup', latticeClosure_min, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiffUnion, Ordinal.iSup_lt, ENNReal.coe_sInf, Submodule.mem_iSup, Submodule.starProjection_tendsto_closure_iSup, Order.one_lt_height_iff, MeasureTheory.iInf_mul_le_setLIntegral, MeasureTheory.measure_sigmaFiniteSetGE_ge, ContinuousMap.edist_eq_iSup, continuous_sInf_rng, Order.coheight_le_iff, ENat.iSup_coe_lt_top, Submodule.span_eq_iSup_of_singleton_spans, Metric.infEDist_biUnion, NNReal.iSup_mul_le, egauge_pi', CategoryTheory.MorphismProperty.transfiniteCompositions_le_llp_rlp, MeasureTheory.Filtration.stronglyMeasurable_limitProcess, MeasureTheory.OuterMeasure.iSup_sInfGen_nonempty, ENNReal.toReal_iSup, IsCompact.exists_sSup_image_eq_and_ge, NonUnitalAlgebra.iInf_toSubmodule, NNReal.iInf_const_zero, Submonoid.FG.biSup, IsUltrametricDist.closedBall_eq_or_disjoint, lowerSemicontinuous_biSup, SSet.range_eq_iSup_of_isColimit, Submodule.span_iUnion₂, FirstOrder.Language.DirectLimit.rangeLiftInclusion, ClassGroup.exists_mem_finset_approx', ENat.floor_le, sSup_mem_closure, Filter.limsup_top_eq_iSup, IsUltrametricDist.nnnorm_tsum_le, SSet.Subcomplex.preimage_iInf, Nat.iSup_le_succ, Order.krullDimLE_iff, CategoryTheory.PreZeroHypercover.Hom.sieve₀_le_sieve₀, ENNReal.add_biSup, Metric.ediam_insert, SSet.skeletonOfMono_succ, Dynamics.dynEntourage_monotone, Ideal.span_iUnion, monotone_closure, Order.succ_eq_sInf, ClassGroup.exists_mem_finsetApprox, Rat.padicValuation_le_one_iff, PiLp.nndist_eq_iSup, Submodule.coe_iSup_of_chain, MeasurableSpace.measurableSet_iSup, FirstOrder.Language.DirectLimit.dom_partialEquivLimit, Set.Nonempty.csInf_mem, AffineSubspace.coe_sInf, Finsupp.iSup_lsingle_range, continuousVAdd_iInf, Ordinal.sInf_empty, MeasureTheory.Filtration.sInf_def, IsTopologicalBasis.iInf_induced, Ordinal.sup_typein_succ, Antitone.pairwise_disjoint_on_Ico_succ, MeasureTheory.Measure.iSup_restrict_spanningSets_of_measurableSet, SimpleGraph.edist_le_one_iff_adj_or_eq, IntermediateField.biSup_adjoin_simple, OrderIso.apply_bliminf, MeasureTheory.lintegral_le_iSup, NonUnitalStarAlgebra.map_iInf, supClosure_min, Metric.closedBall_disjoint_closedBall, IsCompact.exists_sInf_image_eq_and_le, SimpleGraph.radius_eq_iInf_iSup_edist, ENNReal.mul_iSup, CategoryTheory.MorphismProperty.le_transfiniteCompositions, t2Space_iff, Subalgebra.unop_iSup, Subalgebra.unop_sInf, Submodule.finiteDimensional_iSup, dirSupInacc_iff_forall_sSup, EMetric.diam_iUnion_mem_option, Int.cobounded_eq, CompleteSublattice.coe_sInf, NNReal.coe_sInf, ENNReal.toReal_sInf, EisensteinSeries.tsum_symmetricIco_tsum_sub_eq, CategoryTheory.MorphismProperty.transfiniteCompositions_le_iff, HilbertBasis.finite_spans_dense, Monotone.pairwise_disjoint_on_Ico_succ

ConditionallyCompleteLinearOrder

Definitions

Name	Category	Theorems
toLinearOrder 📖	CompOp	20 math math: isPreconnected_uIoo, Finset.Nonempty.ciSup_mem_image, untrop_sum, Finset.Nonempty.csInf_eq_min', Finset.ciInf_mem_image, Finset.Nonempty.csSup_eq_max', exists_isLocalExtr_uIoo, LinearOrderedField.inducedMap_inv_self, trop_iInf, Finset.untrop_sum, isPreconnected_uIoc, LinearOrderedField.coe_inducedOrderRingIso, LinearOrderedField.inducedMap_self, untrop_sum_eq_sInf_image, LinearOrderedField.inducedMap_inducedMap, isConnected_uIoo, isConnected_uIoc, exists_uIoo_isExtrOn_uIcc, Finset.ciSup_mem_image, trop_sInf_image

IsGLB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
csInf_eq 📖	mathematical	IsGLB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice Set.Nonempty	InfSet.sInf ConditionallyCompleteLattice.toInfSet	—	unique isGLB_csInf

IsLUB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
csSup_eq 📖	mathematical	IsLUB Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice Set.Nonempty	SupSet.sSup ConditionallyCompleteLattice.toSupSet	—	unique isLUB_csSup

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
csInf_image_le 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set Set.instMembership BddBelow Preorder.toLE	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.image	—	le_csSup_image
csSup_image_le 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty Set Set.instMembership upperBounds Preorder.toLE	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.image	—	csSup_le Set.Nonempty.image mem_upperBounds_image
le_csInf_image 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty Set Set.instMembership lowerBounds Preorder.toLE	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.image	—	csSup_image_le
le_csSup_image 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set Set.instMembership BddAbove Preorder.toLE	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.image	—	le_csSup map_bddAbove Set.mem_image_of_mem
map_csInf 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set.Nonempty	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.image	—	IsLeast.csInf_eq map_isLeast isLeast_csInf

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
csInf_eq_of_subset_of_forall_exists_le 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.image MonotoneOn Set Set.instHasSubset Set.instMembership	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	Set.eq_empty_or_nonempty le_antisymm le_csInf Set.Nonempty.image Set.Nonempty.mono csInf_le_of_le BddBelow.mono Set.image_mono csInf_le_csInf
csSup_eq_of_subset_of_forall_exists_le 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.image MonotoneOn Set Set.instHasSubset Set.instMembership	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	csInf_eq_of_subset_of_forall_exists_le dual
map_csInf 📖	mathematical	MonotoneOn PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set.Nonempty	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.image	—	IsLeast.csInf_eq map_isLeast isLeast_csInf
sInf_image_Icc 📖	mathematical	Preorder.toLE MonotoneOn PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Icc	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.image	—	IsGLB.csInf_eq isGLB_iff_le_iff LE.le.trans Set.left_mem_Icc Set.Nonempty.image Set.nonempty_Icc
sSup_image_Icc 📖	mathematical	Preorder.toLE MonotoneOn PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Icc	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.image	—	Set.Icc_toDual sInf_image_Icc AntitoneOn.dual_left dual_right

OrderDual

Definitions

Name	Category	Theorems
instConditionallyCompleteLattice 📖	CompOp	—
instConditionallyCompleteLinearOrder 📖	CompOp	—

Pi

Definitions

Name	Category	Theorems
conditionallyCompleteLattice 📖	CompOp	—

WithBot

Definitions

Name	Category	Theorems
conditionallyCompleteLattice 📖	CompOp	—
instInfSet 📖	CompOp	5 math math: coe_sInf', sInf_eq, coe_iInf, sInf_empty, coe_biInf
instSupSet 📖	CompOp	8 math math: Order.krullDim_eq_iSup_coheight, sSup_empty, Order.krullDim_eq_iSup_height, coe_iSup, ciSup_empty, coe_biSup, coe_sSup', sSup_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_sInf' 📖	mathematical	BddBelow Preorder.toLE	some InfSet.sInf WithBot instInfSet Set.image	—	WithTop.coe_sSup'
coe_sSup' 📖	mathematical	Set.Nonempty BddAbove Preorder.toLE	some SupSet.sSup WithBot instSupSet Set.image	—	WithTop.coe_sInf'
sInf_empty 📖	mathematical	—	InfSet.sInf WithBot instInfSet PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteSemilatticeInf.toInfSet Set Set.instEmptyCollection Top.top instTop OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	sInf_eq OrderBot.bddBelow Set.preimage_empty sInf_empty coe_top
sInf_eq 📖	mathematical	WithBot Set Set.instMembership Bot.bot bot BddBelow Preorder.toLE Set.preimage some	InfSet.sInf instInfSet	—	—
sSup_empty 📖	mathematical	—	SupSet.sSup WithBot instSupSet Set Set.instEmptyCollection Bot.bot bot	—	WithTop.sInf_empty
sSup_eq 📖	mathematical	Set WithBot Set.instHasSubset Set.instSingletonSet Bot.bot bot BddAbove Preorder.toLE instPreorder	SupSet.sSup instSupSet some Set.preimage	—	WithTop.sInf_eq

WithBot.WithTop

Definitions

Name	Category	Theorems
completeLattice 📖	CompOp	—
completeLinearOrder 📖	CompOp	—

WithTop

Definitions

Name	Category	Theorems
conditionallyCompleteLattice 📖	CompOp	—
instCompleteLinearOrder 📖	CompOp	—
instInfSet 📖	CompOp	15 math math: iInf_empty, sInf_empty, coe_iInf, iInf_coe_eq_top, coe_sInf', untrop_sum, iInf_coe_lt_top, trop_iInf, Finset.untrop_sum, isGLB_sInf, sInf_eq, isGLB_sInf', untrop_sum_eq_sInf_image, trop_sInf_image, coe_sInf
instSupSet 📖	CompOp	8 math math: coe_sSup, coe_sSup', iSup_coe_lt_top, sSup_eq, iSup_coe_eq_top, isLUB_sSup, coe_iSup, isLUB_sSup'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_sInf 📖	mathematical	Set.Nonempty BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder	some InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf iInf WithTop instInfSet Set Set.instMembership	—	coe_sInf' sInf_image
coe_sInf' 📖	mathematical	Set.Nonempty BddBelow Preorder.toLE	some InfSet.sInf WithTop instInfSet Set.image	—	Set.mem_image_of_mem Monotone.map_bddBelow coe_mono Set.preimage_image_eq Option.some_injective
coe_sSup 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder	some SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet iSup WithTop instSupSet Set Set.instMembership	—	coe_sSup' sSup_image
coe_sSup' 📖	mathematical	BddAbove Preorder.toLE	some SupSet.sSup WithTop instSupSet Set.image	—	Set.preimage_image_eq Option.some_injective
isGLB_sInf 📖	mathematical	—	IsGLB WithTop Preorder.toLE instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder InfSet.sInf instInfSet ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	isGLB_sInf' bot_le
isGLB_sInf' 📖	mathematical	BddBelow WithTop Preorder.toLE instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	IsGLB InfSet.sInf instInfSet ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	top_le_iff Set.mem_singleton_iff le_top coe_le_coe csInf_le le_csInf Mathlib.Tactic.Contrapose.contrapose₂ Set.mem_singleton Set.not_nonempty_iff_eq_empty
isLUB_sSup 📖	mathematical	—	IsLUB WithTop Preorder.toLE instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder SupSet.sSup instSupSet ConditionallyCompletePartialOrderSup.toSupSet	—	Set.eq_empty_or_nonempty bot_nonempty csSup_empty isLUB_sSup'
isLUB_sSup' 📖	mathematical	Set.Nonempty WithTop	IsLUB Preorder.toLE instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder SupSet.sSup instSupSet ConditionallyCompletePartialOrderSup.toSupSet	—	le_top coe_le_coe le_csSup le_rfl not_top_le_coe csSup_le
sInf_empty 📖	mathematical	—	InfSet.sInf WithTop instInfSet Set Set.instEmptyCollection Top.top top	—	instIsEmptyFalse
sInf_eq 📖	mathematical	Set WithTop Set.instHasSubset Set.instSingletonSet Top.top top BddBelow Preorder.toLE instPreorder	InfSet.sInf instInfSet some Set.preimage	—	—
sSup_eq 📖	mathematical	WithTop Set Set.instMembership Top.top top BddAbove Preorder.toLE Set.preimage some	SupSet.sSup instSupSet	—	—

WithTop.WithBot

Definitions

Name	Category	Theorems
completeLattice 📖	CompOp	—
completeLinearOrder 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
instCompleteLatticeWithBot 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ciInf_eq_univ_of_not_bddBelow 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set.range	iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf InfSet.sInf Set.univ	—	csInf_eq_univ_of_not_bddBelow
ciInf_of_not_bddBelow 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set.range	iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf InfSet.sInf Set Set.instEmptyCollection	—	csInf_of_not_bddBelow
ciSup_eq_univ_of_not_bddAbove 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set.range	iSup ConditionallyCompletePartialOrderSup.toSupSet SupSet.sSup Set.univ	—	csSup_eq_univ_of_not_bddAbove
ciSup_of_not_bddAbove 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set.range	iSup ConditionallyCompletePartialOrderSup.toSupSet SupSet.sSup Set Set.instEmptyCollection	—	csSup_of_not_bddAbove
csInf_Ioc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.Ioc	—	IsGLB.csInf_eq isGLB_Ioc Set.nonempty_Ioc
csInf_Ioi 📖	mathematical	—	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Ioi PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup	—	csInf_eq_of_forall_ge_of_forall_gt_exists_lt Set.nonempty_Ioi le_of_lt exists_between
csInf_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.Ioo	—	IsGLB.csInf_eq isGLB_Ioo Set.nonempty_Ioo
csInf_eq_bot_of_bot_mem 📖	mathematical	Set Set.instMembership Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	eq_bot_iff csInf_le OrderBot.bddBelow
csInf_eq_csInf_of_forall_exists_le 📖	mathematical	Set Set.instMembership Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csSup_eq_csSup_of_forall_exists_le
csInf_eq_of_forall_ge_of_forall_gt_exists_lt 📖	mathematical	Set.Nonempty Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set Set.instMembership Preorder.toLT	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csSup_eq_of_forall_le_of_forall_lt_exists_gt
csInf_eq_univ_of_not_bddBelow 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.univ	—	csSup_eq_univ_of_not_bddAbove
csInf_image2_eq_csInf_csInf 📖	mathematical	GaloisConnection PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Function.swap Set.Nonempty BddBelow Preorder.toLE	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.image2	—	IsGLB.csInf_eq isGLB_image2_of_isGLB_isGLB isGLB_csInf Set.Nonempty.image2
csInf_image2_eq_csInf_csSup 📖	mathematical	GaloisConnection PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Function.swap OrderDual OrderDual.instPreorder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual OrderDual.ofDual Set.Nonempty BddBelow Preorder.toLE BddAbove	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.image2 SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	csInf_image2_eq_csInf_csInf
csInf_image2_eq_csSup_csInf 📖	mathematical	GaloisConnection OrderDual PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder OrderDual.instPreorder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual Function.swap OrderDual.ofDual Set.Nonempty BddAbove Preorder.toLE BddBelow	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.image2 SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	csInf_image2_eq_csInf_csInf
csInf_image2_eq_csSup_csSup 📖	mathematical	GaloisConnection OrderDual PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder OrderDual.instPreorder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual Function.swap OrderDual.ofDual Set.Nonempty BddAbove Preorder.toLE	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.image2 SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	csInf_image2_eq_csInf_csInf
csInf_insert 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set Set.instInsert SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice	—	csSup_insert
csInf_le 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice Set Set.instMembership	InfSet.sInf ConditionallyCompleteLattice.toInfSet	—	ConditionallyCompleteLattice.csInf_le
csInf_le' 📖	mathematical	Set Set.instMembership	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csInf_le OrderBot.bddBelow
csInf_le_csInf 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice Set.Nonempty Set Set.instHasSubset	InfSet.sInf ConditionallyCompleteLattice.toInfSet	—	le_csInf csInf_le
csInf_le_csInf' 📖	mathematical	Set.Nonempty Set Set.instHasSubset	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csInf_le_csInf OrderBot.bddBelow
csInf_le_csSup 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder BddAbove Set.Nonempty	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	isGLB_le_isLUB isGLB_csInf isLUB_csSup
csInf_le_iff 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice Set.Nonempty	InfSet.sInf ConditionallyCompleteLattice.toInfSet	—	le_trans le_csInf csInf_le
csInf_le_of_le 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice Set Set.instMembership	InfSet.sInf ConditionallyCompleteLattice.toInfSet	—	le_trans csInf_le
csInf_lt_iff 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set.Nonempty	Preorder.toLT InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set Set.instMembership	—	isGLB_lt_iff isGLB_csInf
csInf_lt_of_lt 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set Set.instMembership Preorder.toLT	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	lt_csSup_of_lt
csInf_mem 📖	mathematical	Set.Nonempty	Set Set.instMembership InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	—	isLeast_csInf
csInf_of_not_bddBelow 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set Set.instEmptyCollection	—	ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow
csInf_pair 📖	mathematical	—	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set Set.instInsert Set.instSingletonSet SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice	—	IsGLB.csInf_eq isGLB_pair Set.insert_nonempty
csInf_union 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set Set.instUnion SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice	—	csSup_union
csInf_univ 📖	mathematical	—	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.univ Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup	—	IsLeast.csInf_eq isLeast_univ
csInf_upperBounds_eq_csSup 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf upperBounds SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	IsGLB.unique isGLB_csInf Set.Nonempty.mono IsLeast.isGLB isLUB_csSup
csInf_upperBounds_range 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf upperBounds iSup ConditionallyCompletePartialOrderSup.toSupSet	—	csInf_upperBounds_eq_csSup Set.range_nonempty
csSup_Ico 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.Ico	—	IsLUB.csSup_eq isLUB_Ico Set.nonempty_Ico
csSup_Iio 📖	mathematical	—	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Iio PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder	—	csSup_eq_of_forall_le_of_forall_lt_exists_gt Set.nonempty_Iio le_of_lt exists_between
csSup_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.Ioo	—	IsLUB.csSup_eq isLUB_Ioo Set.nonempty_Ioo
csSup_empty 📖	mathematical	—	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Set Set.instEmptyCollection Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrderBot.toOrderBot	—	ConditionallyCompleteLinearOrderBot.csSup_empty
csSup_eq_csSup_of_forall_exists_le 📖	mathematical	Set Set.instMembership Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	Set.eq_empty_or_nonempty Set.eq_empty_of_forall_notMem supSet_to_nonempty LE.le.trans le_antisymm csSup_le le_csSup csSup_of_not_bddAbove
csSup_eq_of_forall_le_of_forall_lt_exists_gt 📖	mathematical	Set.Nonempty Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set Set.instMembership Preorder.toLT	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	eq_of_le_of_not_lt csSup_le lt_irrefl LT.lt.trans_le le_csSup
csSup_eq_of_is_forall_le_of_forall_le_imp_ge 📖	mathematical	Set.Nonempty Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	LE.le.antisymm csSup_le le_csSup
csSup_eq_top_of_top_mem 📖	mathematical	Set Set.instMembership Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	csInf_eq_bot_of_bot_mem
csSup_eq_univ_of_not_bddAbove 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.univ	—	csSup_of_not_bddAbove Mathlib.Tactic.Contrapose.contrapose₄ BddAbove.mono Set.subset_univ
csSup_image2_eq_csInf_csInf 📖	mathematical	GaloisConnection OrderDual OrderDual.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Function.swap DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.toDual Set.Nonempty BddBelow Preorder.toLE	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.image2 InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csSup_image2_eq_csSup_csSup
csSup_image2_eq_csInf_csSup 📖	mathematical	GaloisConnection OrderDual OrderDual.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Function.swap DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.toDual Set.Nonempty BddBelow Preorder.toLE BddAbove	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.image2 InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csSup_image2_eq_csSup_csSup
csSup_image2_eq_csSup_csInf 📖	mathematical	GaloisConnection PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Function.swap OrderDual OrderDual.instPreorder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual OrderDual.toDual Set.Nonempty BddAbove Preorder.toLE BddBelow	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.image2 InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csSup_image2_eq_csSup_csSup
csSup_image2_eq_csSup_csSup 📖	mathematical	GaloisConnection PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Function.swap Set.Nonempty BddAbove Preorder.toLE	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set.image2	—	IsLUB.csSup_eq isLUB_image2_of_isLUB_isLUB isLUB_csSup Set.Nonempty.image2
csSup_insert 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set Set.instInsert SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice	—	IsLUB.csSup_eq IsLUB.insert isLUB_csSup Set.insert_nonempty
csSup_inter_le 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty Set Set.instInter	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice	—	csSup_le le_inf le_csSup
csSup_le 📖	mathematical	Set.Nonempty Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice	SupSet.sSup ConditionallyCompleteLattice.toSupSet	—	ConditionallyCompleteLattice.csSup_le
csSup_le' 📖	mathematical	Set Set.instMembership upperBounds Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	csSup_le_iff'
csSup_le_csSup 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice Set.Nonempty Set Set.instHasSubset	SupSet.sSup ConditionallyCompleteLattice.toSupSet	—	csSup_le le_csSup
csSup_le_csSup' 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Set Set.instHasSubset	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	Set.eq_empty_or_nonempty csSup_empty bot_le csSup_le_csSup
csSup_le_iff 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	isLUB_le_iff isLUB_csSup
csSup_le_iff' 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	isLUB_le_iff isLUB_csSup'
csSup_lowerBounds_eq_csInf 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet lowerBounds InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	IsLUB.unique isLUB_csSup Set.Nonempty.mono IsGreatest.isLUB isGLB_csInf
csSup_lowerBounds_range 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet lowerBounds iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csSup_lowerBounds_eq_csInf Set.range_nonempty
csSup_of_not_bddAbove 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set Set.instEmptyCollection	—	ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove
csSup_pair 📖	mathematical	—	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set Set.instInsert Set.instSingletonSet SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice	—	IsLUB.csSup_eq isLUB_pair Set.insert_nonempty
csSup_union 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set Set.instUnion SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice	—	IsLUB.csSup_eq IsLUB.union isLUB_csSup Set.Nonempty.inl
exists_between_of_forall_le 📖	mathematical	Set.Nonempty Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	Set Set.instInter upperBounds lowerBounds	—	le_csInf csInf_le Set.Nonempty.mono
exists_lt_of_csInf_lt 📖	mathematical	Set.Nonempty Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	Set Set.instMembership	—	exists_lt_of_lt_csSup
exists_lt_of_lt_csSup 📖	mathematical	Set.Nonempty Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	Set Set.instMembership	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq csSup_le
exists_lt_of_lt_csSup' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	Set Set.instMembership	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq csSup_le'
isGLB_csInf 📖	mathematical	Set.Nonempty BddBelow Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice	IsGLB InfSet.sInf ConditionallyCompleteLattice.toInfSet	—	csInf_le le_csInf
isLUB_csSup 📖	mathematical	Set.Nonempty BddAbove Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice	IsLUB SupSet.sSup ConditionallyCompleteLattice.toSupSet	—	le_csSup csSup_le
isLUB_csSup' 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder	IsLUB SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	Set.eq_empty_or_nonempty csSup_empty isLUB_csSup
isLeast_csInf 📖	mathematical	Set.Nonempty	IsLeast Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	sInf_eq_argmin_on Function.argminOn_mem Function.argminOn_le Set.nonempty_of_mem
le_csInf 📖	mathematical	Set.Nonempty Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice	InfSet.sInf ConditionallyCompleteLattice.toInfSet	—	ConditionallyCompleteLattice.le_csInf
le_csInf_iff 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	le_isGLB_iff isGLB_csInf
le_csInf_iff' 📖	mathematical	Set.Nonempty	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set Set.instMembership lowerBounds	—	le_isGLB_iff IsLeast.isGLB isLeast_csInf
le_csInf_iff'' 📖	mathematical	Set.Nonempty	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	le_csInf_iff OrderBot.bddBelow
le_csInf_inter 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.Nonempty Set Set.instInter	SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csSup_inter_le
le_csSup 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice Set Set.instMembership	SupSet.sSup ConditionallyCompleteLattice.toSupSet	—	ConditionallyCompleteLattice.le_csSup
le_csSup_iff 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice Set.Nonempty	SupSet.sSup ConditionallyCompleteLattice.toSupSet	—	le_trans csSup_le le_csSup
le_csSup_iff' 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	le_trans csSup_le' le_csSup
le_csSup_of_le 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice Set Set.instMembership	SupSet.sSup ConditionallyCompleteLattice.toSupSet	—	le_trans le_csSup
lt_csSup_iff 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set.Nonempty	Preorder.toLT SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set Set.instMembership	—	lt_isLUB_iff isLUB_csSup
lt_csSup_iff' 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder	Preorder.toLT SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet Set Set.instMembership	—	Iff.not csSup_le_iff'
lt_csSup_of_lt 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set Set.instMembership Preorder.toLT	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	lt_of_lt_of_le le_csSup
notMem_of_csSup_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet BddAbove Preorder.toLE	Set Set.instMembership	—	notMem_of_lt_csInf
notMem_of_lt_csInf 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf BddBelow Preorder.toLE	Set Set.instMembership	—	lt_irrefl LT.lt.trans_le csInf_le
notMem_of_lt_csInf' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	Set Set.instMembership	—	notMem_of_lt_csInf OrderBot.bddBelow
sInf_eq_argmin_on 📖	mathematical	Set.Nonempty	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Function.argminOn Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup	—	IsLeast.csInf_eq Function.argminOn_mem Function.argminOn_le Set.nonempty_of_mem
sInf_iUnion_Ici 📖	mathematical	—	InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set.iUnion Set.Ici PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup iInf	—	sSup_iUnion_Iic
sSup_iUnion_Iic 📖	mathematical	—	SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set.iUnion Set.Iic PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder iSup	—	csSup_eq_csSup_of_forall_exists_le Set.mem_range_self Set.mem_iUnion_of_mem le_rfl
subset_Icc_csInf_csSup 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder BddAbove	Set Set.instHasSubset Set.Icc InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	csInf_le le_csSup

---

← Back to Index