SetNotation

📁 Source: Mathlib/Order/SetNotation.lean

Statistics

Metric	Count
Definitions InfSet, sInf, iInter, iUnion, iUnion_delab, instInfSet, instSupSet, sInter, sInter_delab, sUnion, «term⋂_,_», «term⋂₀_», «term⋃_,_», «term⋃₀_», SupSet, sSup, iInf, iInf_delab, iSup, iSup_delab, «term⨅_,_», «term⨆_,_»	22
Theorems iInf_eq_iInter, iSup_eq_iUnion, mem_iInter, mem_iUnion, mem_sInter, mem_sUnion, sInf_eq_sInter, sSup_eq_sUnion, infSet_to_nonempty, supSet_to_nonempty	10
Total	32

InfSet

Definitions

Name	Category	Theorems
sInf 📖	CompOp	637 math math: sInf_univ, sInf_image2_eq_sInf_sSup, Set.Iic.coe_sInf, continuous_sInf_dom₂, PolynormableSpace.sInf, OrderIso.map_csInf, StarSubalgebra.coe_sInf, SetTheory.PGame.grundyValue_eq_sInf_moveLeft, sInfHomClass.map_sInf, Ideal.eq_jacobson_iff_sInf_maximal, Real.sSup_smul_of_nonpos, IsGLB.sInf_eq, ENNReal.add_sInf, csSup_image2_eq_csInf_csInf, gauge_def', csInf_of_not_bddBelow, nhds_sInf, Ordinal.sInf_compl_lt_lift_ord_succ, Antitone.sInf, continuousMul_sInf, SimpleGraph.sInf_adj, Subfield.mem_sInf, Submodule.span_sInf_le, eq_sInf_coatoms, NonUnitalSubring.coe_sInf, inf_eq_bot_of_bot_mem, DirectedOn.subset_Icc_csInf_csSup, ProperCone.dual_sUnion, sInf_pair, le_sInf_iff, UpperSet.mem_sInf_iff, AntitoneOn.map_sSup_of_continuousWithinAt, Set.Finite.lt_csInf_iff, RightOrdContinuous.map_sInf, le_csInf_iff, uniformContinuous_sInf_rng, uniformContinuous_sInf_dom, csInf_mem, sInf_union, Ordinal.log_def, sInf_lt_iff, Bornology.IsBounded.subset_Icc_sInf_sSup, Ideal.IsHomogeneous.sInf, AffineSubspace.mem_sInf_iff, ContinuousLinearMap.nnnorm_def, PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical, OrderIso.map_csInf', DividedPowers.SubDPIdeal.sInf_carrier_def, isLeast_csInf, compl_sInf, Subalgebra.op_sInf, Interval.coe_sInf, Real.ediam_eq, csInf_insert, continuousVAdd_sInf, Algebra.mem_sInf, ULift.up_sInf, csInf_singleton, Int.csInf_mem, csInf_zero, Monotone.csInf_image_le, Set.Nonempty.eq_Icc_iff_int, MeasureTheory.Measure.restrict_sInf_eq_sInf_restrict, ContinuousAlternatingMap.norm_def, toDual_sInf, Real.sInf_of_not_bddBelow, NonUnitalAlgebra.sInf_toNonUnitalSubsemiring, RingOfIntegers.exponent_eq_sInf, NonUnitalStarAlgebra.mem_sInf, AddSubmonoid.addUnits_sInf, IsCompact.isLeast_sInf, IsLeast.csInf_mem, csInf_eq_of_forall_ge_of_forall_gt_exists_lt, WithTop.sInf_empty, csInf_lt_iff, sInf_sup_le_iInf_sup, Finset.inf_id_eq_sInf, Int.csInf_eq_least_of_bdd, Real.sInf_le_sSup, Filter.HasBasis.limsInf_eq_iSup_sInf, AddGroupTopology.toTopologicalSpace_sInf, Filter.sSup_lowerBounds, Pi.addOrderOf_eq_sInf, Ideal.jacobson_bot_polynomial_le_sInf_map_maximal, Con.sInf_toSetoid, WithBot.coe_sInf', Ideal.sInf_isPrime_of_isChain, Real.sInf_smul_of_nonneg, Monotone.sInf, convexHull_toCone_eq_sInf, subset_sInf_of_not_bddBelow, IsClosed.sInf_mem, toDual_sSup, Subsemiring.op_sInf, Ordinal.card_sInf_range_compl_le_lift, NonUnitalStarAlgebra.coe_sInf, Filter.blimsup_eq, AddSubgroup.unop_sInf, Function.Periodic.sInf_add_zsmul_le_integral_of_pos, Filter.HasBasis.limsup_eq_sInf_univ_of_empty, PUnit.sInf_eq, Sublattice.mem_sInf, Nat.sInf_eq_zero, MeasureTheory.Measure.sInf_caratheodory, sSup_image2_eq_sInf_sInf, SimpleGraph.Colorable.chromaticNumber_eq_sInf, isUniformAddGroup_sInf, ProperCone.innerDual_sUnion, compl_sSup', LieSubmodule.sInf_toSubmodule, Filter.HasBasis.limsup_eq_ite, continuousNeg_sInf, CompleteLattice.le_sInf, AddSubgroup.op_sInf, ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow, OrderIso.map_sInf_eq_sInf_symm_preimage, Pi.Lex.sInf_apply, csInf_div, Filter.HasBasis.limsup_eq_sInf_iUnion_iInter, le_csInf, AffineSubspace.affineSpan_eq_sInf, Ordinal.card_sInf_range_compl_le, regularSpace_sInf, sInf_image2_eq_sInf_sInf, Algebra.sInf_toSubsemiring, Algebra.sInf_toSubmodule, RingCon.ringConGen_eq, Subsemiring.coe_sInf, Monotone.rightLim_eq_sInf, topologicalAddGroup_sInf, Ideal.comap_sInf', CategoryTheory.Coverage.toGrothendieck_eq_sInf, ciInf_of_not_bddBelow, Nimber.add_def, Setoid.quotient_mk_sInf_eq, ProfiniteGrp.closedSubgroup_eq_sInf_open, sInf_le_sInf, csInf_le_of_le, Nat.nth_zero, Set.Nonempty.ordConnected_iff_of_bdd', csInf_Ioc, CompleteSublattice.coe_sInf', Ideal.eq_jacobson_iff_sInf_maximal', Submonoid.op_sInf, csInf_mul, IsConnected.Ioo_csInf_csSup_subset, isJacobsonRing_iff_sInf_maximal, BoundedContinuousFunction.dist_eq, sInf_le_sInf_of_subset_insert_top, LieSubalgebra.sInf_coe, sInf_eq_argmin_on, sInf_image, sInf_sub, TopologicalSpace.Closeds.mem_sInf, UniformSpace.sInf_le, CompleteSublattice.sInfClosed, ClosedSubmodule.coe_sInf, FirstOrder.Language.Substructure.coe_sInf, IsLeast.csInf_eq, Submodule.mem_set_smul_def, ciInf_eq_univ_of_not_bddBelow, RingCon.sInf_toSetoid, Sublocale.sInf_mem, subset_sInf_emptyset, IsCompact.sInf_mem, WithBot.sInf_eq, Ordinal.succ_log_def, SimpleGraph.dist_eq_sInf, Nat.sInf_mem, csSup_lowerBounds_eq_csInf, ContinuousOn.sInf_image_Icc_le, essSup_eq_sInf, LieSubalgebra.sInf_toSubmodule, ArchimedeanClass.stdPart_eq_sInf, MeasureTheory.hitting_eq_end_iff, Ordinal.enumOrd_zero, IntermediateField.sInf_toSubalgebra, sSup_inv, AddSubsemigroup.op_sInf, BoundedContinuousFunction.norm_eq, MonotoneOn.tendsto_nhdsGT, ENat.sInf_eq_zero, sInf_prod, Int.csInf_eq_leastOfBdd, MeasureTheory.hittingAfter_def, Ideal.Filtration.sInf_N, Monotone.map_csInf, ciInf_eq_ite, sInf_mul, induced_sInf, sInf_neg, csInf_le', Function.minimalPeriod_piMap, SetTheory.PGame.grundyValue_eq_sInf_moveRight, Setoid.sInf_equiv, IsCoatom.sInf_le, Subsemiring.unop_sInf, sInf_inv, Int.csInf_of_not_bddBelow, Filter.liminf_eq_sSup_sInf, Submonoid.mem_sInf, TwoSidedIdeal.sInf_ringCon, CompleteSublattice.sInfClosed', ContinuousOn.image_uIcc_eq_Icc, AddSubmonoid.mem_sInf, continuousInv_sInf, DirectedOn.csInf_le_iff, Setoid.sInf_iff, Con.conGen_eq, Ideal.mem_sInf, DirectedOn.csInf_le_csSup, NonUnitalSubsemiring.mem_sInf, ofDual_sInf, ContinuousOn.image_Icc, cbiInf_eq_of_not_forall, SimpleGraph.Subgraph.sInf_adj, Subsemiring.sInf_toAddSubmonoid, LowerSet.coe_sInf, AntitoneOn.map_csSup_of_continuousWithinAt, Subsemigroup.coe_sInf, continuousSMul_sInf, CompleteSemilatticeInf.le_sInf, le_sInf_inter, csInf_Ioi, LieSubalgebra.coe_sInf, IsCompact.lt_sInf_iff_of_continuous, AddSubmonoid.coe_sInf, WithTop.coe_sInf', unary_relation_sInf_iff, Real.le_sInf, sInf_apply, CompleteSublattice.mem_sInf, CategoryTheory.GrothendieckTopology.mem_sInf, sInf_sUnion, Submonoid.units_sInf, Nat.sInf_def, sInf_image2, Real.sInf_neg, MeasureTheory.hitting_def, HomogeneousIdeal.toIdeal_sInf, AddSubmonoid.unop_sInf, ENNReal.sub_eq_sInf, AddSubsemigroup.coe_sInf, Finset.Nonempty.csInf_eq_min', NonUnitalSubring.sInf_toSubsemigroup, Antitone.map_csSup_of_continuousAt, GroupTopology.toTopologicalSpace_sInf, GaloisConnection.u_csInf, ContinuousLinearMap.norm_def, MeasureTheory.Measure.sInf_apply, UniformSpace.le_sInf, Sublocale.coe_sInf, DirectedOn.le_csInf_iff, Subring.op_sInf, AddSubsemigroup.unop_sInf, MeasureTheory.Measure.inf_apply, Subring.unop_sInf, sInf_one, ContinuousOn.isBigOWith_rev_principal, AddSubsemigroup.mem_sInf, SimpleGraph.Subgraph.edgeSet_sInf, Sublocale.sInf_mem', Real.diam_eq, isGLB_iff_sInf_eq, sSup_lowerBounds_eq_sInf, Ideal.comap_sInf, eq_Icc_of_connected_compact, continuous_sInf_dom, MonotoneOn.csInf_eq_of_subset_of_forall_exists_le, hnot_eq_sInf_codisjoint, Subgroup.unop_sInf, isUniformGroup_sInf, sInf_mem_closure, UniformSpace.toTopologicalSpace_sInf, sInf_sup_eq, csInf_upperBounds_range, Filter.ker_sInf, csInf_eq_bot_of_bot_mem, DirectedOn.csInf_eq_of_forall_ge_of_forall_gt_exists_lt, sInf_eq_iInf, gc_Ici_sInf, Filter.sInf_neBot_of_directed', Set.sInf_eq_sInter, Cardinal.sInf_eq_zero_iff, sInf_iUnion_Ici, gauge_def, Digraph.sInf_adj, AddCon.coe_sInf, topologicalGroup_sInf, ContinuousOn.image_uIcc, Nat.nth_eq_sInf, Real.sInf_nonpos, Order.PFilter.sInf_gc, OrderIso.map_csInf_of_directedOn, Real.sInf_nonneg, RightOrdContinuous.map_sInf', Ordinal.cof_eq_sInf_lsub, Pi.Lex.le_sInf_apply, sdiff_eq_sInf, csInf_le_csSup, uniformContinuous_sInf_dom₂, Set.Icc.coe_sInf, MonotoneOn.map_csInf, sInf_le_sInf_of_isCoinitialFor, quotient_norm_mk_eq, DirectedOn.le_csInf, SimpleGraph.edist_eq_sInf, MonotoneOn.tendsto_nhdsWithin_Ioo_right, Antitone.map_sSup_of_continuousAt, Ideal.radical_eq_sInf, AntitoneOn.sInf_image_Icc, Subfield.sInf_toSubring, csSup_inv, CompleteLattice.isCoatomistic_iff, Submodule.sInf_coe, CategoryTheory.Subfunctor.sInf_obj, GaloisInsertion.l_sInf_u_image, sInf_eq_iInf', DirectedOn.csInf_lt_of_lt, Measurable.sInf, Subgroup.op_sInf, isGLB_sInf, csInf_image2_eq_csSup_csInf, NonUnitalSubsemiring.sInf_toAddSubmonoid, CategoryTheory.Subgroupoid.mem_sInf, IsGLB.csInf_eq, GaloisCoinsertion.u_sInf_l_image, Set.Nonempty.ordConnected_iff_of_bdd, csInf_Ico, ClosureOperator.sInf_isClosed, sSup_div, le_csInf_iff', IsCompact.isGLB_sInf, csInf_le_iff, Nucleus.sInf_apply, ENat.coe_sInf, eq_Icc_csInf_csSup_of_connected_bdd_closed, continuousAdd_sInf, WithBot.sInf_empty, sInf_zero, LocallyConvexSpace.sInf, Pi.orderOf_eq_sInf, SimpleGraph.Subgraph.sInf_adj_of_nonempty, Subring.sInf_toAddSubgroup, MeasureTheory.hittingAfter_eq_sInf, LowerSet.Iic_sInf, WithTop.isGLB_sInf, Subgroup.mem_sInf, isGLB_csInf, Subsemigroup.mem_sInf, sInf_image2_eq_sSup_sSup, csInf_Ioo, MeasureTheory.OuterMeasure.sInf_apply, Function.minimalPeriod_eq_sInf_n_pos_IsPeriodicPt, Cardinal.succ_def, CompleteSemilatticeInf.sInf_le, LieSubmodule.sInf_toSubmodule_eq_iInf, Concept.intent_sInf, MonotoneOn.sInf_image_Icc, RingCon.coe_sInf, GaloisConnection.u_csInf_of_directedOn, Pi.Colex.le_sInf_apply, AddMonoid.exponent_eq_sInf, Nat.sInf_le, csInf_one, csInf_eq_univ_of_not_bddBelow, le_csInf_iff'', Subfield.coe_sInf, Cardinal.sInf_empty, sSup_neg, continuous_map_sInf, AddSubmonoid.op_sInf, Submonoid.unop_sInf, AntitoneOn.tendsto_nhdsLT, Real.sInf_empty, csInf_neg, LowerSet.mem_sInf_iff, CompleteDistribLattice.MinimalAxioms.iInf_sup_le_sup_sInf, sInf_le, sSup_sub, ClosedSubmodule.mem_sInf, Real.sInf_univ, sInf_image2_eq_sSup_sInf, Subsemigroup.op_sInf, Antitone.tendsto_nhdsLT, Ideal.map_sInf, Nat.sInf_empty, RightOrdContinuous.map_csInf, NormedAddGroupHom.IsQuotient.norm, Ordinal.lift_card_sInf_compl_le, AddCon.addConGen_eq, Antitone.le_map_sInf, AffineSubspace.direction_sInf, WithTop.sInf_eq, ConvexOn.hasDerivWithinAt_sInf_slope_of_mem_interior, Nat.sInf_upward_closed_eq_succ_iff, MeasurableSpace.measurableSet_sInf, IsCompact.continuous_sInf, csInf_Icc, CategoryTheory.Sieve.sInf_apply, sInf_insert, BooleanSubalgebra.mem_sInf, MeasureTheory.hittingBtwn_eq_sInf, CategoryTheory.Subfunctor.Subpresheaf.sInf_obj, AffineSubspace.direction_sInf_of_mem, MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrict, ENNReal.sInf_add, CategoryTheory.Pretopology.isGLB_sInf, Subsemigroup.unop_sInf, sup_sInf_le_iInf_sup, Nimber.mul_def, Sublattice.coe_sInf, DirectedOn.csInf_le_csInf, ConditionallyCompleteLattice.le_csInf, Real.sInf_le_iff, MeasureTheory.hittingBtwn_eq_end_iff, DirectedOn.csInf_le, CategoryTheory.Pretopology.mem_sInf, StarSubalgebra.sInf_toSubalgebra, FirstOrder.Language.ClosedUnder.sInf, sInf_add, Setoid.eqvGen_eq, Submodule.mem_sInf, csInf_upperBounds_eq_csSup, csInf_union, subset_Icc_csInf_csSup, Real.sInf_smul_of_nonpos, Cardinal.lift_sInf, Set.Iic_sInf, Order.succ_eq_csInf, DirectedOn.csInf_le_of_le, ConditionallyCompletePartialOrder.isGLB_csInf_of_directed, sSup_image2_eq_sSup_sInf, sInf_diff_singleton_top, le_sInf, CategoryTheory.GrothendieckTopology.isGLB_sInf, ciInf_neg, Monoid.exponent_eq_sInf, NonUnitalSubring.sInf_toAddSubgroup, IntermediateField.sInf_toSubfield, Monotone.map_sInf_le, Filter.sInf_neBot_of_directed, LieSubmodule.coe_sInf, NonUnitalAlgebra.mem_sInf, le_csInf_inter, csSup_div, AddSubgroup.mem_sInf, BoundedContinuousFunction.norm_eq_of_nonempty, csInf_lt_of_lt, Ordinal.sInf_compl_lt_ord_succ, MeasureTheory.OuterMeasure.sInf_apply', Finset.inf_eq_sInf_image, BoundedContinuousFunction.nndist_eq, nilradical_eq_sInf, Real.sInf_nonpos', Con.coe_sInf, StarSubalgebra.mem_sInf, LowerSet.compl_sInf, Submodule.CoFG.sInf, sInf_empty, iInf_of_isEmpty, Algebra.adjoin_eq_sInf, InfClosed.sInf_mem_of_nonempty, ConditionallyCompletePartialOrderInf.isGLB_csInf_of_directed, SchwartzMap.seminorm_apply, Finset.inf'_id_eq_csInf, Nat.eq_Ici_of_nonempty_of_upward_closed, WithTop.isGLB_sInf', csInf_sub, NNReal.sInf_empty, Subring.sInf_toSubmonoid, sInf_eq_of_forall_ge_of_forall_gt_exists_lt, MeasureTheory.Measure.sub_def, sup_sInf_eq, CompleteLattice.sInf_le, BooleanSubalgebra.coe_sInf, SimpleGraph.sInf_adj_of_nonempty, NonUnitalSubsemiring.sInf_toSubsemigroup, untrop_sum_eq_sInf_image, Filter.eq_sInf_of_mem_iff_exists_mem, MeasureTheory.OuterMeasure.sInf_eq_boundedBy_sInfGen, NonUnitalAlgebra.coe_sInf, AddSubgroup.coe_sInf, sInf_upperBounds_eq_csSup, BooleanSubalgebra.sInf_mem, CategoryTheory.Precoverage.toGrothendieck_eq_sInf, IsClosed.csInf_mem, Finset.inf'_eq_csInf_image, sInf_upperBounds_eq_sSup, UpperSet.coe_sInf, Finset.Nonempty.csInf_mem, NonUnitalSubsemiring.coe_sInf, OrderIso.map_sInf, sSup_image2_eq_sInf_sSup, Ideal.sInf_minimalPrimes, Filter.limsInf_principal_eq_sInf, OrderHom.map_sInf_subset_fixedPoints_le, csInf_image2_eq_csSup_csSup, sInfHom.map_sInf', Prod.swap_sInf, sInf_image', csInf_eq_csInf_of_forall_exists_le, exists_seq_tendsto_sInf, Filter.limsup_eq_sInf_sSup, Pi.Colex.sInf_apply, csSup_image2_eq_csSup_csInf, Subring.mem_sInf, isJacobsonRing_iff_sInf_maximal', ULift.down_sInf, Order.Ideal.mem_sInf, sInf_Prop_eq, NonUnitalSubring.mem_sInf, TopologicalSpace.Closeds.coe_sInf, Convex.toCone_eq_sInf, Subsemiring.sInf_toSubmonoid, csInf_image2_eq_csInf_csInf, csInf_Ici, SimpleGraph.Subgraph.neighborSet_sInf, ofDual_sSup, OrderHom.sInf_apply, Filter.limsup_eq, IsCompact.exists_sInf_image_eq, sInf_le_of_le, ContinuousMultilinearMap.norm_def, csInf_image2_eq_csInf_csSup, csInf_le_csInf', sInf_eq_top, compl_sInf', FirstOrder.Language.Substructure.mem_sInf, ConvexCone.coe_sInf, NonUnitalStarAlgebra.sInf_toNonUnitalSubalgebra, Ideal.IsHomogeneous.radical_eq, csSup_sub, NormedAddGroupHom.norm_def, UpperSet.compl_sInf, PointedCone.dual_sUnion, csInf_le, Real.isGLB_sInf, Int.absNorm_under_eq_sInf, Filter.limsInf_eq_iSup_sInf, CategoryTheory.Subgroupoid.sInf_isNormal, csInf_univ, Submodule.span_biInter, ENNReal.toNNReal_sInf, SimpleGraph.Finsubgraph.coe_sInf, CategoryTheory.Subgroupoid.mem_sInf_arrows, GaloisConnection.u_csInf_of_directedOn', Algebra.coe_sInf, Nat.nth_count_eq_sInf, ENNReal.inv_sInf, Monotone.le_csInf_image, sInf_within_of_ordConnected, subset_sInf_def, Submonoid.coe_sInf, NonUnitalAlgebra.sInf_toSubmodule, Prod.fst_sInf, MeasureTheory.hitting_eq_sInf, ClosedSubmodule.toSubmodule_sInf, sInf_range, Ideal.homogeneousHull_eq_sInf, sInf_le_sSup, Filter.limsInf_principal_eq_csSup, IsPreconnected.mem_intervals, csSup_image2_eq_csInf_csSup, IsClosed.isLeast_csInf, binary_relation_sInf_iff, csInf_le_csInf, Real.sSup_neg, Projectivization.Subspace.span_eq_sInf, InfClosed.sInf_mem, csInf_add, csInf_mem_closure, sInf_singleton, IntermediateField.coe_sInf, GaloisConnection.u_sInf, Order.Coframe.MinimalAxioms.sup_sInf_eq, Submodule.restrictScalars_sInf, R1Space.sInf, Monotone.tendsto_nhdsGT, Set.Nonempty.eq_Icc_iff_nat, AddCon.sInf_toSetoid, LieSubalgebra.sInf_glb, csInf_inv, Real.sInf_def, Subfield.isGLB_sInf, Int.csInf_of_not_bdd_below, MeasureTheory.hittingBtwn_def, Ring.jacobson_eq_sInf_isMaximal, Submodule.span_sInf, Order.Coframe.MinimalAxioms.iInf_sup_le_sup_sInf, csInf_pair, Submodule.CoFG.sInf_of_finite, sInf_div, Order.Ideal.coe_sInf, sInf_eq_bot, trop_sInf_image, Subring.coe_sInf, OrderIso.map_csInf_of_directedOn', ConvexOn.rightDeriv_eq_sInf_slope_of_mem_interior, SimpleGraph.Subgraph.verts_sInf, ENNReal.coe_sInf, Prod.snd_sInf, Concept.extent_sInf, continuous_sInf_rng, Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici, Order.Coframe.MinimalAxioms.sInf_sup_eq, Ideal.comap_jacobson, Real.lt_sInf_add_pos, CategoryTheory.Pretopology.sInf_ofGrothendieck, Subsemiring.mem_sInf, ConditionallyCompleteLattice.csInf_le, LieSubmodule.sInf_coe, DirectedOn.isGLB_csInf, Submodule.coe_sInf, IsPreconnected.Ioi_csInf_subset, AntitoneOn.tendsto_nhdsWithin_Ioo_left, GaloisConnection.u_csInf', WithTop.coe_sInf, Order.succ_eq_sInf, Set.Nonempty.csInf_mem, upperClosure_eq_Ici_csInf, AffineSubspace.coe_sInf, Ordinal.sInf_empty, MeasureTheory.Filtration.sInf_def, Setoid.sInf_def, IsCompact.exists_sInf_image_eq_and_le, csSup_neg, sInf_le_iff, Subalgebra.unop_sInf, CompleteSublattice.coe_sInf, ConvexCone.mem_sInf, Subgroup.coe_sInf, sInf_sup_sInf, NNReal.coe_sInf, TwoSidedIdeal.mem_sInf, ENNReal.toReal_sInf, Int.csInf_empty

Set

Definitions

Name	Category	Theorems
iInter 📖	CompOp	718 math math: iInter₂_div_subset, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, LowerSemicontinuousOn.inter_biInter_preimage_Iic_eq_empty_iff_exists_finset, countable_bInter_mem, MeasureTheory.Measure.haar.nonempty_iInter_clAddPrehaar, Finset.set_biInter_finset_image, MeasureTheory.mem_generateSetAlgebra_elim, StarSubalgebra.coe_sInf, ProbabilityTheory.Kernel.iIndepSet_iff_meas_biInter, ProbabilityTheory.IndepSets.bInter, compl_iInter₂, LinearMap.polar_iUnion, ContinuousMap.hasBasis_nhds, TopologicalSpace.Closeds.iInf_def, setOf_isOpen_iSup, MulAction.IsBlock.of_subset, bergelson, iInter₂_mono', MeasureTheory.IsSetRing.iInter_le_mem, countable_iInter_mem, NonUnitalSubring.coe_sInf, Metric.closedBall_eq_bInter_ball, Ideal.isHomogeneous_iff_subset_iInter, biInter_image2, Concept.extent_sSup, Filter.mem_iInf, ProbabilityTheory.Kernel.iIndep.meas_biInter, Ordinal.not_bddAbove_fp_family, add_iInter₂_subset, iInter_dissipate, LinearMap.polar_eq_iInter, fixedPoints_subgroup_iSup, ProbabilityTheory.iIndepFun_iff, div_iInter_subset, ProbabilityTheory.iIndep.meas_biInter, image_sInter_subset, sInter_union_sInter, Topology.IsConstructible.iInter, iUnion_eq_compl_iInter_compl, iInter₂_smul_subset, SimpleGraph.Subgraph.neighborSet_iInf, univ_pi_eq_iInter, convexHull_eq_iInter, small_biInter, sInter_smul_subset, biInter_union, Seminorm.closedBall_iSup, compl_iInter, ProbabilityTheory.iIndepFun_iff_measure_inter_preimage_eq_mul, iInter_eq_if, Metric.exists_forall_closedEBall_subset_aux₂, iInter_smul_subset, sub_sInter_subset, Filter.EventuallyEq.biInter, biInter_mono, iInter_unpair, tangentConeAt_eq_biInter_closure, Interval.coe_sInf, biInter_inter, Directed.Ici_ciSup, iInter_plift_up, ProbabilityTheory.iIndepFun.measure_inter_preimage_eq_mul, surjOn_iInter_iInter, biUnion_iInter_of_pairwise_disjoint, Interval.coe_iInf₂, Filter.HasBasis.iInf, AbsConvex.iInter, Filter.EventuallyEq.iInter, small_iInter', lowerPolar_iUnion₂, Filter.EventuallyLE.biInter, Iic_iInf, Iic_ciInf, biInter_le_succ', biInter_insert, mapsTo_iInter_iInter, Finite.interior_sInter, sInter_prod, nhdsKer_iInter_subset, nonempty_iInter_Iic_iff, image2_sInter_subset_left, Filter.iInf_principal_finset, subset_iInter_iff, IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal, IsSemilinearSet.biInter_finset, IsRelUpperSet.iInter, image_iInter₂_subset, TopologicalSpace.Closeds.coe_iInf, isClosed_biInter, fixedPoints_addSubmonoid_iSup, Matroid.closure_biInter_eq_biInter_closure_of_biUnion_indep, mem_generatePiSystem_iUnion_elim, Finset.set_biInter_insert_update, iInf_eq_iInter, IntermediateField.coe_iInf, iInter_const, iInter_eq_compl_iUnion_compl, smul_sInter_subset, interior_iInter₂_subset, Finset.eventuallyEq_iInter, add_iInter_subset, MeasureTheory.tendsto_measure_biInter_gt, image2_sInter_subset_right, sub_iInter₂_subset, Filter.ker_def, IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe, ordConnected_iInter, dissipate_def, sInter_neg, upperBounds_iUnion, gauge_le_eq, Concept.extent_iInf, generateFrom_iInter_of_generateFrom_eq_self, LocallyFinite.exists_finset_nhds_support_subset, dense_iInter_of_Gδ, iInter_congr, NonUnitalStarAlgebra.coe_sInf, MulAction.fixed_eq_iInter_fixedBy, MeasureTheory.Egorov.measure_inter_notConvergentSeq_eq_zero, omegaLimit_def, AlgebraicGeometry.Scheme.zeroLocus_iUnion, biInter_finsetSigma', Concept.intent_sSup, sInter_vadd_subset, Real.singleton_eq_inter_Icc, ENNReal.iInter_Ici_coe_nat, ProbabilityTheory.Kernel.iIndepSet.meas_biInter, union_distrib_iInter_left, ProbabilityTheory.iCondIndep_iff, IsGδ.biInter_of_isOpen, ProbabilityTheory.iCondIndepFun_iff_condExp_inter_preimage_eq_mul, iInter₂_mono, Finite.measurableSet_biInter, disjointed_eq_inter_compl, Concept.intent_iInf, SetRel.isRefl_iInter, ProbabilityTheory.iIndepSets.meas_iInter, iInter_iInter_eq_right, Algebra.coe_iInf, iInter₂_vadd_subset, prod_indicator_apply, Finset.nullMeasurableSet_biInter, union_iInter, iInter₂_comm, Filter.iInf_principal', iInter₂_subset, UpperSemicontinuousOn.inter_biInter_preimage_Ici_eq_empty_iff_exists_finset, biInter_le_eq_iInter, Metric.biInter_gt_ball, Finset.set_biInter_coe, IsTransitiveRel.iInter, iInf_eq_dif, biInter_finsetSigma, biInter_pair, image2_iInter_subset_left, Filter.HasBasis.limsup_eq_sInf_iUnion_iInter, Finset.eventuallyLE_iInter, LieSubalgebra.engel_carrier, biInter_univ, LieSubmodule.iInf_coe, Metric.exists_forall_closedEBall_subset_aux₁, iInter_eq_iInter_finset, Subsemiring.coe_sInf, IsRetrocompact.biInter, smul_set_iInter_subset, iInter_univ, biInter_sigma, biInter_lt_eq_iInter, ProbabilityTheory.iIndepFun.meas_biInter, sInter_inv, IsSemilinearSet.biInter, biInter_finsetSigma_univ, ProbabilityTheory.iIndepSets_iff, iInter_mul_subset, Metric.cthickening_eq_iInter_thickening, isLowerSet_iInter₂, mem_iInter_of_mem, union_distrib_iInter₂_right, mem_iInter₂, iInter₂_union_iInter₂, InjOn.image_iInter_eq, definable_finset_biInter, biInter_eq_iInter, subset_iInter, Antitone.piecewise_eventually_eq_iInter, LieSubalgebra.sInf_coe, PartitionOfUnity.exists_finset_nhds_support_subset, balanced_iInter, biInter_lt_succ', ProbabilityTheory.Kernel.iIndepSets.meas_biInter, surjOn_iInter, smul_set_iInter₂_subset, biInter_ge, iInter_mono'', closure_eq_uniformity, FirstOrder.Language.Substructure.coe_sInf, iInter_psigma', dense_biInter_of_isOpen, Concept.intent_iSup, biInter_const, isClopen_iInter_of_finite, EventuallyEq.countable_bInter, SimpleGraph.Subgraph.edgeSet_iInf, iInter_iUnion_of_antitone, Filter.exists_iInter_of_mem_iInf, sInter_eq_iInter, Submodule.iInf_coe, dense_iInter_of_isOpen, Bornology.isCobounded_iInter, vadd_iInter₂_subset, MeasureTheory.IsSetRing.biInter_mem, AlgebraicGeometry.Scheme.zeroLocus_def, isExtreme_biInter, EMetric.exists_forall_closedBall_subset_aux₂, Ordinal.IsClosedBelow.iInter, ProbabilityTheory.Kernel.IndepSets.iInter, vsub_iInter₂_subset, absorbs_iInter, iUnion_iInter_of_monotone, nhdsSet_iInter_le, subset_iInter₂, mapsTo_iInter, iUnion_iInter_of_antitone, IsGδ.eq_iInter_nat, subset_iInter₂_iff, vadd_iInter_subset, MeasureTheory.IsSetAlgebra.biInter_mem, insert_iInter, ProbabilityTheory.Kernel.IndepSets.bInter, iInter_union, mapsTo_iInter₂_iInter₂, iInter₂_mul_subset, MeasureTheory.tendsto_setIntegral_of_antitone, IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed, AddSubmonoid.coe_iInf, biInter_iUnion, NonUnitalSubring.coe_iInf, Finsupp.supported_iInter, preimage_val_iInter, IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed, Filter.sInter_comap_sets, Bornology.isCobounded_biInter_finset, Finset.measurableSet_biInter, iInter_of_empty, IsRelLowerSet.iInter₂, biInter_subset_of_mem, PrimeSpectrum.zeroLocus_bUnion, Filter.EventuallyLE.iInter, Subfield.coe_iInf, IsSymmetricRel.iInter, mul_iInter₂_subset, LowerSet.coe_sInf, Metric.closure_eq_iInter_cthickening, Absorbs.iInter, Subsemigroup.coe_sInf, sInter_sub_subset, Finset.set_biInter_inter, ProbabilityTheory.iCondIndepSets_singleton_iff, div_iInter₂_subset, infClosed_iInter, interior_iInter_subset, MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le, LieSubalgebra.coe_sInf, Finite.eventuallyLE_iInter, MeasureTheory.tendsto_measure_iInter_le, biInter_and, Submodule.coe_finsetInf, ProbabilityTheory.iIndepSet.meas_biInter, iInter_add_subset, AddSubmonoid.coe_sInf, union_distrib_iInter₂_left, Antitone.tendsto_indicator, PrimeSpectrum.zeroLocus_iSup, isUpperSet_iInter₂, nonempty_iInter, Concept.extent_iSup, Finset.set_biInter_insert, Metric.cthickening_eq_iInter_cthickening', BaireSpace.baire_property, interior_sInter_subset, SetRel.isSymm_iInter, supClosed_iInter, iInter_union_of_monotone, CategoryTheory.Functor.toPreimages_map, Filter.sInter_lift'_sets, Subsemiring.isHomogeneous_iff_subset_iInter, ciSup_mem_iInter_Icc_of_antitone_Icc, sInter_eq_biInter, iInter₂_subset_of_subset, image2_iInter₂_subset_left, sInter_image2, AddSubsemigroup.coe_sInf, Iic_iInf₂, EventuallyEq.countable_iInter, bergelson', compl_iUnion₂, ProbabilityTheory.iIndepFun.cond, iInter_iInter_eq_left, starConvex_iInter₂, Filter.mem_biInf_principal, Monotone.ciSup_mem_iInter_Icc_of_antitone, Monotone.measure_iInter, ProbabilityTheory.CondIndepSets.bInter, biSup_iInter_of_pairwise_disjoint, generateFrom_iInter, Filter.mem_iInf_finset, biInter_subset_biInter_left, iInter_halfSpaces_eq, mem_iInter, iInter_plift_down, vsub_iInter_subset, SimpleGraph.Subgraph.edgeSet_sInf, Interval.coe_iInf, nonempty_iInter_Ici_iff, Submodule.coe_iInf, interior_iInter₂_lt_nat, ProbabilityTheory.iCondIndepSet_iff, Antitone.iInter_comp_tendsto_atTop, sInter_vsub_subset, Matroid.closure_iInter_eq_iInter_closure_of_iUnion_indep, ordConnected_iInter', EventuallyLE.countable_bInter, isCompact_iff_finite_subfamily_closed, ProbabilityTheory.Kernel.iIndepFun.measure_inter_preimage_eq_mul, Finset.inf_set_eq_iInter, sInter_iUnion, Filter.hasBasis_iInf_principal_finite, AddAction.IsBlock.of_subset, MeasureTheory.integral_biUnion_eq_sum_powerset, sInter_div_subset, mapsTo_iInter₂, Filter.ker_iInf, EMetric.exists_forall_closedBall_subset_aux₁, Filter.ker_sInf, iInter₂_sub_subset, NonUnitalAlgebra.coe_iInf, Subgroup.coe_iInf, LowerSet.coe_iInf₂, lowerPolar_iUnion, iUnion_iInter_ge_nat_add, LocallyFinite.iInter_compl_mem_nhds, ProbabilityTheory.iIndepSets.meas_biInter, compl_iUnion, Antitone.tendsto_setIntegral, LowerSet.coe_iInf, Ici_iSup₂, Finite.interior_biInter, ProbabilityTheory.cond_iInter, isOpen_iInter_of_finite, IsGδ.iInter, iInter_sum, smul_iInter_subset, stableUnderGeneralization_iInter, Filter.biInter_finset_mem, CategoryTheory.Subfunctor.Subpresheaf.iInf_obj, smul_set_iInter, iInter_inter, omegaLimit_eq_biInter_inter, UniformSpace.ball_iInter, bijOn_iInter, Submodule.coe_torsionBySet, fixedPoints_submonoid_iSup, Submodule.sInf_coe, Filter.HasBasis.iInf', IsRelUpperSet.iInter₂, Finite.nullMeasurableSet_biInter, SetRel.isTrans_iInter, indicator_iInter_apply, MeasureTheory.AnalyticSet.iInter, Ici_sSup, biInter_sigma', PrimeSpectrum.zeroLocus_iUnion, biInter_image, Filter.EventuallyLE.cardinal_bInter, inter_iInter, Matroid.Indep.closure_iInter_eq_biInter_closure_of_forall_subset, Finite.eventuallyEq_iInter, Topology.IsLocallyConstructible.iInter, absConvexHull_eq_iInter, biInter_empty, UpperSet.coe_iSup, Matroid.Indep.inter_isBasis_iInter, balanced_iInter₂, ProbabilityTheory.iCondIndepSets_iff, iInter_setOf, iInter_exists, MeasureTheory.NullMeasurableSet.iInter, IsSemilinearSet.iInter, NonUnitalSubsemiring.coe_iInf, ProbabilityTheory.iIndep_iff, EventuallyLE.countable_iInter, Filter.sInter_lift_sets, AddAction.IsBlock.iInter, sInter_mul_subset, Metric.cthickening_eq_iInter_thickening', ProjectiveSpectrum.zeroLocus_iUnion, image_iInter, ProjectiveSpectrum.zeroLocus_bUnion, iInter_union_iInter, iInter_eq_const, image2_iInter_subset_right, IsTopologicalBasis.iInf, iInter₂_vsub_subset, ordConnected_biInter, ProbabilityTheory.Kernel.iIndep.meas_iInter, NonUnitalStarAlgebra.coe_iInf, Concept.intent_sInf, isClopen_iInter, Filter.EventuallyEq.cardinal_iInter, LinearMap.polar_eq_biInter_preimage, Filter.cardinal_iInter_mem, interior_sInter, MeasureTheory.tendsto_measure_iInter_atTop, isOpen_biInter_finset, iInter_sigma', stableUnderSpecialization_iInter, biInter_and', Representation.invariants_eq_inter, isOpen_iInter, Subfield.coe_sInf, mulIndicator_iInter_apply, BooleanSubalgebra.coe_iInf, Metric.cthickening_eq_iInter_cthickening, interior_iInter₂_le_nat, convex_iInter₂, image_val_iInter, iInter_subtype, MeasureTheory.Measure.haar.nonempty_iInter_clPrehaar, isClopen_biInter_finset, Metric.cthickening_eq_iInter_thickening'', MeasurableSet.biInter, sInter_prod_sInter, iInter_or, BaireMeasurableSet.iInter, biInter_range, Finset.iInter_mem_sets, AbsConvex.iInter₂, sym2_iInter, definable_biInter_finset, Filter.HasBasis.liminf_eq_sSup_iUnion_iInter, Filter.iInter_mem, mul_sInter_subset, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, Real.iInter_Iic_rat, Antitone.measure_iInter, UpperSet.coe_iSup₂, iInter_subset_of_subset, iInter_sub_subset, ProbabilityTheory.iCondIndepFun_iff, Filter.iInf_principal_finite, Metric.closure_eq_iInter_thickening', MeasureTheory.tendsto_measure_iInter_atBot, Filter.HasBasis.biInter_biUnion_ball, Monotone.iInter_comp_tendsto_atBot, iInter_neg, preimage_sInter, MeasurableSet.iInter_of_antitone, inter_biInter, SimpleGraph.Subgraph.verts_iInf, AddSubgroup.coe_iInf, MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat, Finset.support_prod_subset, biInter_le_succ, image2_sInter_right_subset, iInter_subset_iInter₂, iUnion_iInter_subset, prod_indicator, Sublattice.coe_sInf, iInter_eq_iInter_finset', TopologicalSpace.Closeds.iInf_mk, ProbabilityTheory.iIndepSet_iff, Filter.biInter_mem, PrimeSpectrum.zeroLocus_iUnion₂, diff_iUnion, Absorbs.biInter, sInter_range, iInter_iInter_eq', isTopologicalBasis_biInter_Ioi_Iio_of_generateFrom, ConvexBody.iInter_smul_eq_self, Filter.sSup_sets_eq, AddAction.fixed_eq_iInter_fixedBy, prod_indicator_const, iInter_inter_distrib, ProbabilityTheory.iIndepFun.meas_iInter, ProbabilityTheory.CondIndepSets.iInter, upperPolar_iUnion₂, add_sInter_subset, biInter_basis_nhds, Iic_sInf, Filter.EventuallyLE.cardinal_iInter, biInter_ge_eq_iInf, isGδ_iff_eq_iInter_nat, iInter₂_union, isExtreme_iInter, Ici_ciSup, iInter_false, bijOn_iInter_of_directed, Directed.Iic_ciInf, biInter_dissipate, interior_iInter, image_iInter₂, biInter_gt_eq_iInf, CategoryTheory.PreGaloisCategory.autEmbedding_range, isUpperSet_iInter, LieSubmodule.coe_sInf, Metric.closure_eq_iInter_cthickening', image_projection_prod, Filter.iInter_mem', Filter.mem_iInf_of_finite, iInter_subset, lowerBounds_iUnion, CategoryTheory.Subfunctor.iInf_obj, BijOn.iInter_congr, closure_eq_inter_uniformity, MeasurableSet.iInter_of_antitone_of_frequently, ProjectiveSpectrum.zeroLocus_iSup_homogeneousIdeal, sInter_add_subset, sInter_image, Seminorm.closedBall_eq_biInter_ball, ProbabilityTheory.iIndepSet_iff_meas_biInter, StarSubalgebra.coe_iInf, FirstOrder.Language.Theory.CompleteType.iInter_setOf_subset, prod_indicator_const_apply, ConvexCone.coe_iInf, fixedPoints_addSubgroup_iSup, MeasureTheory.NullMeasurableSet.biInter, iInter_Iic_eq_empty_iff, IsRetrocompact.iInter, Filter.iInf_principal, iInter₂_eq_empty_iff, isLindelof_iff_countable_subfamily_closed, setOf_liouville_eq_iInter_iUnion, nhdsKer_sInter_subset, eq_closed_inter_nat, preimage_iInter, BooleanSubalgebra.coe_sInf, ProbabilityTheory.Kernel.iIndepFun.meas_iInter, Filter.cardinal_bInter_mem, Filter.HasBasis.ker, starConvex_iInter, iInter_true, connectedComponent_eq_iInter_isClopen, biInter_lt_succ, NonUnitalAlgebra.coe_sInf, isLowerSet_iInter, AddSubgroup.coe_sInf, Submodule.finset_inf_coe, ProbabilityTheory.Kernel.iIndepFun.meas_biInter, ProbabilityTheory.iIndep.meas_iInter, Finite.isOpen_biInter, Submonoid.coe_iInf, iInter_psigma, Antitone.mulIndicator_eventuallyEq_iInter, Directed.measure_iInter, vsub_sInter_subset, NonUnitalSubsemiring.coe_sInf, biInter_subset_biUnion, image2_iInter₂_subset_right, iInter_mono, iInter_vsub_subset, Sublattice.coe_iInf, Finset.set_biInter_singleton, AffineSubspace.coe_iInf, Antitone.iInter_nat_add, ProbabilityTheory.Kernel.iIndepSets_singleton_iff, preimage_iInter₂, iInter_comm, Filter.mem_iInf', mem_iInter₂_of_mem, setOf_liouville_eq_irrational_inter_iInter_iUnion, sub_iInter_subset, Seminorm.ball_finset_sup_eq_iInter, Antitone.tendsto_mulIndicator, RCLike.iInter_halfSpaces_eq, CategoryTheory.Functor.toPreimages_obj, iInter_eq_empty_iff, isClopen_iInter₂, dense_biInter_of_Gδ, TopologicalSpace.Closeds.coe_sInf, pi_def, PrimitiveSpectrum.hull_iSup, SimpleGraph.Subgraph.neighborSet_sInf, vadd_set_iInter, LocallyFinite.exists_finset_nhds_mulSupport_subset, ENNReal.iInter_Ioi_coe_nat, vadd_sInter_subset, iInter_Iio_of_not_bddBelow_range, iInter₂_add_subset, ProjectiveSpectrum.zeroLocus_iSup_ideal, MeasureTheory.measureReal_biUnion_eq_sum_powerset, setOf_isOpen_sSup, dense_iInter_of_isOpen_nat, iInter_iInter_eq_or_left, Matroid.IsFlat.iInter, iInter_coe_set, UpperSet.coe_sSup, iInter₂_congr, iInter_div_subset, Filter.HasBasis.biInter_mem, ConvexCone.coe_sInf, InjOn.image_biInter_eq, Subsemiring.coe_iInf, Finite.absorbs_biInter, Filter.HasBasis.tangentConeAt_eq_biInter_closure, Finset.set_biInter_option_toFinset, Finset.indicator_biUnion_eq_sum_powerset, Finite.Set.finite_iInter, connectedComponent_subset_iInter_isClopen, iInter_congr_of_surjective, piiUnionInter_singleton_left, biInter_singleton, AddSubsemigroup.coe_iInf, ProbabilityTheory.Kernel.iIndepFun.cond_iInter, Submodule.span_biInter, omegaLimit_iInter, ProbabilityTheory.IndepSets.iInter, Algebra.coe_sInf, iInter_star, FirstOrder.Language.Substructure.coe_iInf, smul_set_sInter_subset, iInter_inv, Submonoid.coe_sInf, Antitone.indicator_eventuallyEq_iInter, IsRelLowerSet.iInter, Metric.biInter_gt_closedBall, pi_iUnion_eq_iInter_pi, smul_iInter₂_subset, isSublattice_iInter, Filter.biInter_mem', eq_closed_inter_countable, iInter_ite, Topology.IsConstructible.biInter, Matroid.closure_sInter_eq_biInter_closure_of_sUnion_indep, setOf_forall, Finite.isClopen_biInter, MeasurableSet.iInter, iInter_dite, iInter_union_of_antitone, union_distrib_iInter_right, small_iInter, IsGδ.biInter, omegaLimit_eq_iInter, union_iInter₂, Ici_iSup, Ideal.coe_piOrderIso_apply, iInter_congr_Prop, sInter_prod_sInter_subset, LieSubmodule.coe_iInf, vadd_set_iInter₂_subset, ProbabilityTheory.Kernel.iIndepSets.meas_iInter, iInter_subset_iUnion, MeasureTheory.AECover.biInter_Ici_aecover, iInter_ge_eq_iInter_nat_add, Function.Surjective.iInter_comp, mul_iInter_subset, diff_iInter, mem_biInter, isClosed_iInter, small_biInter', Filter.iSup_sets_eq, omegaLimit_eq_iInter_inter, Order.Ideal.coe_sInf, vadd_set_sInter_subset, BaireMeasurableSet.biInter, mem_generatePiSystem_iUnion_elim', Subring.coe_sInf, balancedCore_eq_iInter, biInter_le, Subsemigroup.coe_iInf, Subring.coe_iInf, interior_iInter_of_finite, Finset.set_biInter_biUnion, nonempty_iInter₂, Finset.support_prod, SimpleGraph.Subgraph.verts_sInf, Seminorm.closedBall_finset_sup_eq_iInter, image_iInter_subset, Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subset, convex_iInter, prod_sInter, stdSimplex_eq_inter, Concept.extent_sInf, image2_sInter_left_subset, iInter_mono', iInter_vadd_subset, iInter_and, Filter.EventuallyEq.cardinal_bInter, iInter_iUnion_of_monotone, LieSubmodule.sInf_coe, PointedCone.dual_eq_iInter_dual_singleton, div_sInter_subset, Submodule.coe_sInf, BijOn.iInter_comp, IsGδ.iInter_of_isOpen, Metric.closure_eq_iInter_thickening, iInter_eq_univ, biInter_finsetSigma_univ', Dynamics.dynEntourage_eq_inter_Ico, inter_iInter_nat_succ, ProbabilityTheory.iIndepSets_singleton_iff, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus, prod_iInter, AffineSubspace.coe_sInf, Matroid.Indep.inter_isBasis_biInter, Ordinal.derivFamily_eq_enumOrd, iInter_sigma, IsTopologicalBasis.iInf_induced, vadd_set_iInter_subset, isOpen_iInter₂, iInter_subset_dissipate, upperPolar_iUnion, iInter_option, Subgroup.coe_sInf, MulAction.IsBlock.iInter, Finset.interior_iInter, inter_eq_iInter, Bornology.isCobounded_biInter, ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul
iUnion 📖	CompOp	1354 math math: Ultrafilter.finite_biUnion_mem_iff, finite_diff_iUnion_Ioo, iUnion_Ioi, iUnion_vadd, Equiv.Perm.support_closure_subset_union, iUnion_eq_range_sigma, DoubleCoset.doubleCoset_union_rightCoset, HahnSeries.SummableFamily.isPWO_iUnion_support', iUnion_inv, Metric.thickening_eq_biUnion_ball, VitaliFamily.FineSubfamilyOn.measure_diff_biUnion, Cardinal.mk_iUnion_Ordinal_le_of_le, Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ, pairwise_iUnion, Topology.RelCWComplex.Subcomplex.union', range_sigma_eq_iUnion_range, Subring.coe_sSup_of_directedOn, Ideal.Filtration.submodule_closure_single, biUnion_univ_pi, smul_set_iUnion₂, MeasureTheory.mem_generateSetAlgebra_elim, iUnion_Ioc_right, Ideal.Filtration.submodule_eq_span_le_iff_stable_ge, CategoryTheory.Presieve.uncurry_bind, AddAction.isTopologicallyTransitive_iff_dense_iUnion_preimage, AlgebraicGeometry.Scheme.zeroLocus_iInf, MeasureTheory.VectorMeasure.of_iUnion_nonneg, LocallyFinite.isClosed_iUnion, ENNReal.iUnion_Iio_coe_nat, subset_iUnion₂, LowerAdjoint.closure_iUnion₂_closure, compl_iInter₂, IndexedPartition.iUnion, EMetric.hausdorffEdist_iUnion_le, Metric.AreSeparated.finset_iUnion_right_iff, contDiffOn_iUnion_iff_of_isOpen, Subalgebra.coe_iSup_of_directed, iUnion_Iic_eq_Iio_iSup, finite_cover_nhds, Finset.set_biUnion_biUnion, MulAction.isTopologicallyTransitive_iff_dense_iUnion_preimage, IsGδ.biUnion, iUnion_iUnion_eq_right, iUnion_range_eq_sUnion, Subalgebra.spectrum_sUnion_connectedComponentIn, vadd_set_iUnion₂, image_val_iUnion, LinearMap.polar_iUnion, biUnion_diff_biUnion_subset, Finset.closure_biUnion, biUnion_preimage_singleton, PrimeSpectrum.eq_biUnion_of_isOpen, AddSubsemigroup.closure_iUnion, iUnion_mul_left_image, SetRel.comp_iUnion, TopologicalSpace.Opens.coe_iSup, volume_iUnion_setOf_liouvilleWith, Submodule.iUnion_ssubset_of_forall_ne_top_of_card_lt, iUnion_Iic, biUnion_finsetSigma, biUnion_singleton, IsOpen.iUnion_preimage_vadd, small_biUnion, PrimeSpectrum.iUnion_range_specComap_comp_evalRingHom, Finset.indicator_biUnion, FirstOrder.Language.Theory.isSatisfiable_directed_union_iff, Finite.biUnion', SimpleGraph.Subgraph.neighborSet_sSup, SimpleGraph.iUnion_connectedComponentSupp, iUnion_nonempty_index, Bornology.isBounded_biUnion, balanced_iUnion₂, iUnion_Ioc_eq_Ioi_self_iff, totallyBounded_biUnion, nhdsWithin_biUnion, surjOn_iUnion, finite_iUnion, AlgebraicGeometry.Scheme.Cover.iUnion_range, IsGδ.dense_sUnion_interior_of_closed, Monotone.indicator_eventuallyEq_iUnion, Finset.coe_biUnion, Finset.set_biUnion_insert_update, biUnion_le_succ', MeasureTheory.lintegral_iUnion₀, iUnion_eq_compl_iInter_compl, MeasureTheory.measure_biUnion, Filter.iInf_sets_eq, AddCircle.coe_real_preimage_closedBall_eq_iUnion, smul_set_sUnion, AddSubgroup.iSup_eq_closure, biUnion_ge_eq_iUnion, nonempty_iUnion, isPiSystem_iUnion_of_directed_le, iUnion_sub_left_image, Filter.EventuallyLE.iUnion, MeasureTheory.tendsto_measure_iUnion_atBot, MeasureTheory.lintegral_biUnion_finset₀, biUnion_lt_succ, Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller, compl_iInter, Metric.hausdorffEDist_iUnion_le, IsSemilinearSet.biUnion_finset, QuotientGroup.preimage_image_mk, sUnion_inter_sUnion, ProjectiveSpectrum.vanishingIdeal_iUnion, MeasureTheory.OuterMeasure.isCaratheodory_iUnion, ENNReal.tsum_iUnion_le_tsum, AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp, Matroid.disjointSigma_indep_iff, MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top, MeasureTheory.measure_biUnion_le, MeasureTheory.ProbabilityMeasure.exists_lt_measure_biUnion_of_isOpen, SetRel.image_sUnion, QuotientAddGroup.univ_eq_iUnion_vadd, convexJoin_singleton_left, iUnion₂_subset, indicator_iUnion_apply, TopologicalSpace.IsOpenCover.iSup_set_eq_univ, iUnion_Ioc_map_succ_eq_Ioi, iUnion_mono'', MeasureTheory.measure_biUnion_lt_top, iUnion_vsub_left_image, IntermediateField.coe_iSup_of_directed, sUnion_range, Finset.set_encard_biUnion_le, iUnion_neg_vadd, MeasureTheory.ae_restrict_biUnion_iff, iSup_mulIndicator, isMeagre_biUnion, Submonoid.coe_iSup_of_directed, DoubleCoset.doubleCoset_union_leftCoset, Geometry.SimplicialComplex.vertices_eq, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_f, iUnion_dite, MeasureTheory.SeparableSpace.exists_measurable_partition_diam_le, Dynamics.coverEntropy_iUnion_le, AddAction.univ_eq_iUnion_orbit, biUnion_iInter_of_pairwise_disjoint, iUnion_ite, IsRetrocompact.iUnion, Matroid.closure_iUnion_closure_eq_closure_iUnion, IsPreconnected.biUnion_of_chain, Filter.biInf_sets_eq, SigmaCompactSpace_iff_exists_compact_covering, LindelofSpace.elim_nhds_subcover, MeasureTheory.measure_iUnion_null, stableUnderSpecialization_iUnion, Topology.RelCWComplex.cellFrontier_subset_base_union_finite_closedCell, refinement_of_locallyCompact_sigmaCompact_of_nhds_basis, Finset.set_biUnion_coe, lowerPolar_iUnion₂, MeasureTheory.lintegral_biUnion_finset, iUnion_subset, Bornology.isBounded_iUnion, setOf_liouvilleWith_subset_aux, isUpperSet_iUnion₂, Directed.measure_iUnion, ProbabilityTheory.CondIndepSets.iUnion, Finset.nullMeasurableSet_biUnion, iUnion_div_left_image, eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open, Besicovitch.exists_closedBall_covering_tsum_measure_le, Finset.isLindelof_biUnion, MeasureTheory.Measure.haar.index_elim, Topology.RelCWComplex.Subcomplex.union, biUnion_range_succ_disjointed, ProbabilityTheory.Kernel.IndepSets.biUnion, isClopen_iUnion, exists_partition_approximatesLinearOn_of_hasFDerivWithinAt, MeasureTheory.ae_restrict_biUnion_eq, Topology.RelCWComplex.coe_skeletonLT, MeasureTheory.lintegral_biUnion, iUnion_eq_univ_iff, Finset.set_biUnion_finset_image, TopologicalSpace.Opens.iSup_mk, Besicovitch.exist_disjoint_covering_families, biUnion_inter_of_pairwise_disjoint, HahnSeries.SummableFamily.support_hsum_subset, Finset.subset_set_biUnion_of_mem, Subfield.coe_iSup_of_directed, Encodable.iUnion_decode₂_cases, Finset.indicator_biUnion_apply, Real.borel_eq_generateFrom_Iio_rat, TopologicalSpace.isOpen_iUnion_countable, generateFrom_iUnion_isOpen, Monotone.tendsto_mulIndicator, MeasureTheory.Measure.mkMetric_apply, Real.iUnion_Iic_rat, iUnion_Ioo_right, TopologicalSpace.countable_cover_nhdsWithin, Ioc_subset_biUnion_Ioc, Topology.CWComplex.iUnion_openCell_eq_skeletonLT, LocallyFinite.closure_iUnion, iUnion_unpair_prod, IsGLB.biUnion_Ici_eq_Ici, HahnSeries.SummableFamily.coeff_hsum_mul, IsConnected.iUnion_of_reflTransGen, iUnion_add_right_image, iUnion_subset_iff, Function.iUnion_pnat_ptsOfPeriod, closure_iUnion₂_lt_nat, iUnion_smul, Metric.iUnion_ball_nat_succ, convexJoin_iUnion_right, nhdsSet_iUnion, SimpleGraph.Subgraph.neighborSet_iSup, biUnion_associatedPrimes_eq_compl_regular, iInter_eq_compl_iUnion_compl, iUnion_prod_of_monotone, biUnion_Ici_Ico_map_succ, omegaLimit_iUnion, linearIndepOn_iUnion_of_directed, AddSubsemigroup.coe_iSup_of_directed, biUnion_finsetSigma_univ, Real.borel_eq_generateFrom_Ioo_rat, mulIndicator_iUnion_apply, Ideal.subset_union_prime', continuousOn_iUnion_iff_of_isOpen, Submonoid.iSup_eq_closure, iUnion_closure_compactCovering, MeasureTheory.tendsto_measure_iUnion_atTop, indicator_biUnion_finset_eventuallyEq, Pi.quasispectrum_eq, AEMeasurable.iUnion, upperBounds_iUnion, ENNReal.tsum_biUnion_le, eventually_nhdsSet_iUnion₂, iUnion_congr_of_surjective, AlgebraicGeometry.Scheme.zeroLocus_biInf, Submonoid.coe_sSup_of_directedOn, Topology.RelCWComplex.union_iUnion_openCell_eq_complex, IsSemilinearSet.biUnion, pi_diff_pi_subset, IndexedPartition.piecewise_preimage, MonoidAlgebra.support_gen_of_gen', NumberField.mixedEmbedding.iUnion_negAt_plusPart_ae, TopologicalSpace.NonemptyCompacts.isCompact_biUnion_coe_of_isCompact, Profinite.NobelingProof.GoodProducts.range_equiv_factorization, Pi.spectrum_eq, MeasureTheory.integrableOn_finset_iUnion, isLowerSet_iUnion₂, Filter.iInf_sets_eq_finite', iUnion_inter_subset, CategoryTheory.Subfunctor.Subpresheaf.iSup_obj, Topology.RelCWComplex.union', MeasureTheory.integrableOn_finite_iUnion, Subring.coe_iSup_of_directed, sUnion_eq_iUnion, subset_iUnion_of_subset, MeasureTheory.FiniteMeasure.restrict_biUnion_finset, IsSemilinearSet.iUnion, AffineSubspace.span_iUnion, biUnion_self, AlgebraicGeometry.Scheme.zeroLocus_iUnion, biUnion_prod', surjOn_iUnion₂_iUnion₂, IsRetrocompact.biUnion, Subfield.closure_iUnion, UniformSpace.isCover_iff_subset_iUnion_ball, Finset.sup_set_eq_biUnion, NFA.evalFrom_iUnion₂, Submodule.iInf_colon_iSup, MeasureTheory.measure_biUnion_toMeasurable, MeasureTheory.OuterMeasure.iInf_apply', sigma_eq_biUnion, MeasureTheory.IsSetSemiring.disjointOfUnion_props, Finsupp.span_le_supported_biUnion_support, closure_iUnion, coe_biUnionEqSigmaOfDisjoint_symm_apply, linearIndepOn_biUnion_of_directed, iUnion_union_distrib, Cardinal.mk_iUnion_le_sum_mk_lift, sUnion_vsub, MeasureTheory.integral_biUnion_finset, IsCompact.finite_cover_balls, mul_iUnion, SetRel.sUnion_comp, AddSubgroup.coe_iSup_of_directed, Ideal.iSup_eq_span, ENNReal.tsum_biUnion, Countable.biUnion, Directed.convex_iUnion, iUnion_Iio, NFA.acceptsFrom_iUnion₂, Topology.RelCWComplex.iUnion_openCell_eq_skeleton, PiNat.iUnion_cylinder_update, Cardinal.mk_iUnion_eq_sum_mk, MeasureTheory.VectorMeasure.hasSum_of_disjoint_iUnion, Dense.Iio_eq_biUnion, Subsemiring.coe_iSup_of_directed, iUnion_prod', Topology.RelCWComplex.Subcomplex.union_closedCell, nonempty_biUnion, iUnion_compactCovering, isPiSystem_iUnion_of_monotone, discreteTopology_iUnion_fintype, MeasureTheory.FiniteMeasure.tendsto_measure_iUnion_accumulate, IsConnected.biUnion_of_chain, MeasurableSpace.generateFrom_iUnion_measurableSet, IsOpen.iUnion_smul, iUnion_plift_up, AbsolutelyContinuousOnInterval.tendsto_volume_totalLengthFilter_nhds_zero, image2_iUnion₂_right, Filter.HasBasis.limsup_eq_sInf_iUnion_iInter, Bornology.isVonNBounded_iUnion, absorbs_biUnion_finset, fixingAddSubgroup_iUnion, biUnion_iUnion, subset_iUnion₂_of_subset, IsCompact.exists_finite_cover_smul, NonUnitalSubsemiring.coe_iSup_of_directed, iUnion_Iic_eq_Iio_of_lt_of_tendsto, biUnion_empty_finset, hasSum_sum_disjoint, ENNReal.Ioo_zero_top_eq_iUnion_Ico_zpow, sphere_pi, HahnSeries.SummableFamily.isPWO_iUnion_support, iUnion_sigma, SetRel.preimage_eq_biUnion, disjoint_iUnion_left, Metric.thickening_biUnion, differentiableOn_iUnion_iff_of_isOpen, Sigma.univ, iUnion_source_chartAt, ENNReal.iUnion_Iic_coe_nat, BoxIntegral.Prepartition.iUnion_def, iUnion_disjointed, Finite.measurableSet_biUnion, union_finset_finite_of_range_finite, union_iUnion, Metric.dense_iff_iUnion_ball, Cardinal.mk_biUnion_le_lift, mem_iUnion₂_of_mem, biUnion_le, Subgroup.leftCoset_cover_const_iff_surjOn, mem_iUnion, Countable.isLindelof_biUnion, LowerSet.coe_sSup, univ_subtype, sub_iUnion₂, Monoid.CoprodI.mclosure_iUnion_range_of, IsRelLowerSet.iUnion₂, MeasureTheory.lintegral_iUnion_le, QuotientAddGroup.preimage_image_mk, Finset.wellFoundedOn_bUnion, biUnion_Ico_eq_Iio_self_iff, biUnion_empty, Metric.AreSeparated.finite_iUnion_left, Real.isPiSystem_Iic_rat, encard_iUnion_of_finite, isLowerSet_iUnion, isClosed_iUnion, vsub_sUnion, IsConnected.biUnion_of_reflTransGen, IsOpen.exists_iUnion_isClosed, linearIndepOn_id_iUnion_finite, subset_biUnion_of_mem, Metric.dense_iUnion_range_toInductiveLimit, MeasureTheory.Measure.restrict_biUnion_le, Finset.set_biUnion_singleton, MeasureTheory.ae_restrict_iUnion_eq, sUnion_image2, BoxIntegral.Box.iUnion_Ioo_of_tendsto, prod_eq_biUnion_right, countable_cover_nhds_interior, EventuallyLE.countable_bUnion, Antitone.iUnion_comp_tendsto_atBot, MeasureTheory.measure_iUnion_null_iff, MeasureTheory.integral_fintype_iUnion, Function.mulSupport_iSup, Cardinal.card_iUnion_lt_iff_forall_of_isRegular, Finite.bddAbove_biUnion, Submodule.iSup_span, LowerSet.coe_iSup, biUnion_range, iUnion_Icc_intCast, IsCompactOpenCovered.exists_mem_of_isBasis, iUnion_coe_set, starConvex_iUnion₂, Metric.iUnion_ball_nat, StableUnderSpecialization.Union_eq, Finite.closure_biUnion, DifferentiableOn.iUnion_of_isOpen, isClopen_iUnion_of_finite, Real.borel_eq_generateFrom_Ioi_rat, image_eq_iUnion, QuotientGroup.univ_eq_iUnion_smul, isLindelof_iff_countable_subcover, Cardinal.mk_iUnion_le_sum_mk, absorbs_iUnion, iUnion_Ioc_add_zsmul, exists_spanning_measurableSet_le, iInter_iUnion_of_antitone, iUnion_add, isCompact_iff_finite_subcover, Polynomial.bUnion_roots_finite, MeasureTheory.Measure.restrict_iUnion, iUnion_Ioc_add_intCast, IsCompact.exists_finite_cover_vadd, iUnion_mul, tendsto_mulIndicator_biUnion_finset, MulAction.univ_eq_iUnion_orbit, iUnion_prod_const, MeasureTheory.preVariation.Finset.sup_measurableSetSubtype_eq_biUnion, iUnion_singleton_eq_range, dense_sUnion_interior_of_closed, prod_self_eq_iUnion_perm, IsCompact.cthickening_eq_biUnion_closedBall, biUnion_insert, connectedComponents_preimage_image, MeasureTheory.measure_biUnion_eq_iSup, biUnion_of_singleton, iSup_eq_iUnion, iUnion₂_prod_const, biUnion_univ, Besicovitch.exist_finset_disjoint_balls_large_measure, DenseRange.iUnion_uniformity_ball, NFA.evalFrom_eq_biUnion_singleton, Finite.iUnion, iUnion_iInter_of_monotone, TopologicalSpace.NoetherianSpace.iUnion, isSigmaCompact_iUnion_of_isCompact, mdifferentiableOn_iUnion_iff_of_isOpen, PrimeSpectrum.iUnion_range_comap_comp_evalRingHom, Finite.Set.finite_iUnion, iUnion_eq_range_psigma, iUnion_Ico_add_intCast, MeasureTheory.measureReal_biUnion_finset, Topology.CWComplex.Subcomplex.union, iUnion_iInter_of_antitone, ContinuousOn.iUnion_of_isOpen, Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux, MeasureTheory.IsSetAlgebra.biUnion_mem, SetRel.comp_sUnion, PairwiseDisjoint.biUnion, image_sigma_eq_iUnion, Antitone.measure_iUnion, iUnion_diff, TopologicalSpace.Opens.isBasis_sigma, mul_sUnion, CompactExhaustion.iUnion_eq, Topology.CWComplex.iUnion_openCell_eq_complex, MeasureTheory.OuterMeasure.iInf_apply, IsClopen.biUnion_connectedComponent_eq, Matroid.sum'_ground_eq, MeasureTheory.IsFundamentalDomain.iUnion_smul_ae_eq, Directed.strictConvex_iUnion, exists_locallyFinite_iUnion_eq_ball_radius_lt, IsOpen.dense_iUnion_preimage_vadd, biInter_iUnion, BijOn.iUnion_comp, iUnion_image_preimage_sigma_mk_eq_self, definable_finset_biUnion, iUnion₂_comm, Real.isTopologicalBasis_Ioo_rat, MeasureTheory.VectorMeasure.m_iUnion', Bornology.isBounded_biUnion_finset, Icc_diff_pi_univ_Ioc_subset, IsCompact.closure_eq_biUnion_inseparable, Ico_eq_locus_Ioc_eq_iUnion_Ioo, MeasureTheory.Measure.restrict_iUnion_apply, AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty, iUnion_mono', iUnion_Icc_zsmul, Finset.asymptoticCone_biUnion, sUnion_neg, orthonormal_iUnion_of_directed, Topology.IsConstructible.iUnion, Finite.isClopen_biUnion, PrimeSpectrum.zeroLocus_bUnion, MeasureTheory.OuterMeasure.biInf_apply, refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set, Cardinal.mk_iUnion_eq_sum_mk_lift, biUnion_associatedPrimes_eq_zero_divisors, iUnion_Ico_add_zsmul, iUnion_Icc_add_zsmul, Infinite.iUnion₂, IsOpen.dense_iUnion_preimage_smul, tendsto_indicator_biUnion_finset, Filter.EventuallyLE.cardinal_iUnion, LieSubmodule.span_iUnion, IsLUB.iUnion_Iio_eq, biUnion_lt_succ', eq_open_union_nat, convexJoin_iUnion_left, biUnion_const, Finite.Set.finite_biUnion', asymptoticCone_iUnion_of_finite, generateFrom_iUnion, Topology.CWComplex.union', image2_iUnion_right, Icc_diff_pi_univ_Ioo_subset, iUnion_Ico_eq_Iio_self_iff, MeasureTheory.measurableCylinders_nat, LocallyFinite.nhdsWithin_iUnion, biUnion_union, iUnion_union, EMetric.infEdist_biUnion, Finset.set_ncard_biUnion_le, MeasureTheory.IsAddFundamentalDomain.iUnion_vadd_ae_eq, Real.isPiSystem_Iio_rat, vsub_iUnion, Absorbs.biUnion_finset, biUnion_prod, UpperSet.coe_iInf₂, biUnion_sigma', MeasureTheory.ProbabilityMeasure.tendsto_measure_iUnion_accumulate, Dynamics.coverEntropy_biUnion_finset, iUnion_star, iUnion_ge_eq_iUnion_nat_add, MeasureTheory.ae_eq_restrict_biUnion_finset_iff, MeasureTheory.FiniteMeasure.apply_iUnion_le, IsChain.pairwiseDisjoint_iUnion₂, Function.support_iInf, Topology.CWComplex.cellFrontier_subset_finite_closedCell, setOf_exists, MeasureTheory.FinMeasAdditive.map_iUnion_fin_meas_set_eq_sum, MeasureTheory.measure_iUnion₀, Real.isPiSystem_Ioi_rat, TopologicalSpace.countable_cover_nhds, disjoint_iUnion_right, MeasureTheory.Measure.m_iUnion, IsPreconnected.iUnion_of_reflTransGen, TopCat.GlueData.range_fromOpenSubsetsGlue, ProperCone.dual_iUnion, iUnion_div, countable_cover_nhdsWithin_of_sigmaCompact, Real.borel_eq_generateFrom_Ici_rat, starConvex_iUnion, isClosed_iUnion_of_finite, iUnion_le_nat, Real.isPiSystem_Ici_rat, MeasureTheory.ae_eq_restrict_biUnion_iff, Finset.eventuallyLE_iUnion, ProbabilityTheory.Kernel.IndepSets.iUnion, countable_cover_nhds, Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ, MeasureTheory.StronglyMeasurable.exists_spanning_measurableSet_norm_le, iUnion_op_vadd_set, Metric.cthickening_eq_biUnion_closedBall, eq_open_union_countable, bUnion_mem_nhdsSet, MeasureTheory.OuterMeasure.ofFunction_eq_iInf_mem, eventually_nhdsSet_iUnion, MeasureTheory.measureReal_iUnion_fintype, IsLindelof.elim_nhds_subcover', compl_iUnion₂, iUnion_image_sup_right, Subgroup.exists_leftTransversal_of_FiniteIndex, IsProperSemilinearSet.biUnion, PMF.support_bind, vadd_iUnion₂, SetRel.IsCover.subset_iUnion_ball, algebraicIndependent_iUnion_of_directed, Finset.mulIndicator_biUnion_apply, Metric.thickening_iUnion, MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion, Topology.RelCWComplex.iUnion_skeletonLT_eq_complex, mem_biUnion, prod_eq_biUnion_left, iUnion_accumulate, MeasureTheory.preVariation.iUnion, iUnion_inv_smul, iUnion_Icc_add_intCast, prod_iUnion, Dynamics.coverEntropy_iUnion_of_finite, Filter.EventuallyLE.cardinal_bUnion, aestronglyMeasurable_iUnion_iff, iUnion_range_eq_iUnion, vadd_set_sUnion, mem_iUnion₂, iUnion_const, iUnion_div_right_image, biUnion_range_preimage_singleton, IsClosed.cthickening_eq_biUnion_closedBall, NonUnitalSubalgebra.coe_iSup_of_directed, sUnion_eq_biUnion, sigmaToiUnion_bijective, image_iUnion₂, dimH_bUnion, contMDiffOn_iUnion_iff_of_isOpen, Encodable.iUnion_decode₂, Ideal.Filtration.submodule_span_single, disjoint_iUnion₂_right, SimpleGraph.Subgraph.edgeSet_sSup, IsProperSemilinearSet.biUnion_finset, sized_iUnion₂, Subsemiring.closure_iUnion, sUnion_vadd, BoxIntegral.Box.biUnion_coe_eq_coe, iUnion_inter, discreteTopology_iUnion_finite, EMetric.infEdist_iUnion, Topology.CWComplex.mapsTo', accumulate_def, iUnion_smul_right_image, sInter_iUnion, MeasureTheory.integral_biUnion_eq_sum_powerset, image_iUnion, AddSubmonoid.coe_iSup_of_directed, MeasureTheory.LocallyIntegrableOn.exists_countable_integrableOn, AbsolutelyContinuousOnInterval.tendsto_volume_restrict_totalLengthFilter_disjWithin_nhds_zero, BoxIntegral.Prepartition.iUnion_biUnion, asymptoticCone_biUnion, Monotone.piecewise_eventually_eq_iUnion, AddSubmonoid.coe_sSup_of_directedOn, MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint, Filter.EventuallyEq.cardinal_iUnion, encard_iUnion_le_of_finite, MeasureTheory.Measure.FiniteSpanningSetsIn.spanning, MeasureTheory.measure_iUnion, ZFSet.coe_iUnion, Function.bUnion_ptsOfPeriod, iUnion_nonempty_self, sInf_iUnion_Ici, IsLUB.biUnion_Iic_eq_Iio, iUnion₂_inter, iUnion_Ioo_of_mono_of_isGLB_of_isLUB, AlgebraicGeometry.isCompactOpen_iff_eq_finset_affine_union, lowerPolar_iUnion, iUnion_iInter_ge_nat_add, ENNReal.iUnion_Icc_coe_nat, ZFSet.iUnion_vonNeumann, MeasureTheory.OuterMeasure.iUnion_nat, sSup_iUnion, compl_iUnion, Multipliable.tprod_finset_bUnion_disjoint, iUnion_Ioc_zsmul, MeasureTheory.Measure.haar.addIndex_defined, Topology.RelCWComplex.iUnion_cellFrontier_subset_skeleton, exists_closed_cover_approximatesLinearOn_of_hasFDerivWithinAt, TopologicalSpace.isSeparable_iUnion, definable_biUnion_finset, MeasureTheory.NullMeasurableSet.biUnion, Finite.Set.finite_biUnion'', coe_snd_unionEqSigmaOfDisjoint, iUnion_smul_set, AddSubsemigroup.iSup_eq_closure, IsOpen.iUnion_vadd, Finite.absorbs_biUnion, isClopen_biUnion_finset, Subgroup.coe_iSup_of_directed, biUnion_Iic_disjointed, MeasureTheory.VectorMeasure.of_biUnion_finset, add_sUnion, mul_iUnion₂, coe_lowerClosure, isLUB_iUnion_iff_of_isLUB, subset_iUnion, IsOpen.dense_iUnion_smul, QuotientGroup.preimage_image_mk_eq_iUnion_image, MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup, MeasureTheory.IsSetSemiring.sUnion_disjointOfUnion, TopologicalSpace.IsSeparable.iUnion, Submodule.span_eq_iUnion_nat, iUnion_plift_down, iUnion₂_add, TopologicalSpace.CompactOpens.coe_finsetSup, TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion, SimpleGraph.Subgraph.edgeSet_iSup, HahnSeries.SummableFamily.coeff_smul, Finset.isWF_bUnion, inter_iUnion₂, Finset.coe_disjiUnion, IsCompact.elim_nhds_subcover, Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT, MeasureTheory.ae_restrict_biUnion_finset_iff, isSigmaCompact_iUnion, Submodule.iSup_eq_span, AddSubgroup.leftCoset_cover_const_iff_surjOn, biUnion_gt_eq_iUnion, Finite.isLindelof_biUnion, iUnion_mul_right_image, Finset.eventuallyEq_iUnion, Metric.iUnion_inter_closedBall_nat, countable_iUnion, MeasureTheory.VectorMeasure.of_disjoint_iUnion, Submodule.span_iUnion, DFinsupp.add_closure_iUnion_range_single, biUnion_and, IsCompact.closure_eq_biUnion_closure_singleton, HahnSeries.SummableFamily.isPWO_iUnion_support_powers, asymptoticCone_sUnion, small_iUnion, VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae, iUnion_neg, iSup_iUnion, div_sUnion, exists_seq_cover_iff_countable, AbsolutelyContinuousOnInterval.biUnion_uIoc_subset_of_mem_disjWithin, finite_cover_balls_of_compact, add_iUnion, ENNReal.iUnion_Ico_coe_nat, isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis, MeasureTheory.MeasurablySeparable.iUnion, Finset.isCompact_biUnion, Function.Embedding.sigmaSet_range, iUnion_Ici_eq_Ioi_of_lt_of_tendsto, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens, iUnion₂_mono, FirstOrder.Language.Substructure.iSup_eq_closure, iUnion_subset_iUnion_const, Topology.IsLocallyConstructible.iUnion, PMF.support_bindOnSupport, iUnion_eq_const, ProbabilityTheory.IndepSets.bUnion, IsPreconnected.biUnion_of_reflTransGen, PrimeSpectrum.zeroLocus_iUnion, iUnion_of_empty, FirstOrder.Language.Theory.isSatisfiable_iUnion_iff_isSatisfiable_iUnion_finset, MeasurableSpace.DynkinSystem.has_iUnion_nat, MeasureTheory.VectorMeasure.of_iUnion_nonpos, Function.support_iSup, iUnion_iUnion_eq_left, MeasureTheory.IsSetRing.iUnion_le_mem, infinite_iUnion, ProbabilityTheory.IndepSets.iUnion, iUnion_iUnion_eq_or_left, MeasureTheory.OuterMeasure.isCaratheodory_iUnion_lt, iUnion_psigma', Cardinal.mk_biUnion_le, ncard_iUnion_le_of_fintype, MeasureTheory.VectorMeasure.restrict_le_restrict_iUnion, TopologicalSpace.IsOpenCover.isTopologicalBasis, MeasureTheory.ae_restrict_biUnion_finset_eq, MeasurableSpace.generateFrom_iUnion_countablePartition, VitaliFamily.covering, IsCompact.elim_nhds_subcover_nhdsSet, IsCompact.elim_nhdsWithin_subcover, IsPreconnected.iUnion_of_chain, isMeagre_iUnion, MeasureTheory.measure_iUnion_le, MeasureTheory.Measure.restrict_biUnion_finset, iUnion_vsub, iUnion₂_subset_iUnion, tendstoLocallyUniformlyOn_biUnion, Matroid.disjointSigma_isBasis_iff, Topology.RelCWComplex.cellFrontier_subset_finite_openCell, iUnion_comm, MeasureTheory.Measure.haar.addIndex_elim, vadd_sUnion, EventuallyLE.countable_iUnion, MeasureTheory.ProbabilityMeasure.apply_iUnion_le, BoxIntegral.Box.iUnion_coe_splitCenterBox, Topology.IsLocallyConstructible.biUnion, Monotone.iUnion_nat_add, aemeasurable_iUnion_iff, MeasureTheory.addContent_biUnion_eq, ProjectiveSpectrum.zeroLocus_iUnion, Filter.EventuallyEq.biUnion, ProjectiveSpectrum.zeroLocus_bUnion, iUnion_smul_eq_setOf_exists, Finite.ncard_biUnion, Cardinal.mk_iUnion_le_lift, compact_covered_by_add_left_translates, MeasureTheory.preVariation.sum_le_preVariationFun_iUnion', ProbabilityTheory.IndepSets.biUnion, BoxIntegral.Prepartition.iUnion_biUnionTagged, iUnion_image_right, iUnion_Ico_intCast, MeasureTheory.SimpleFunc.lintegral_restrict_iUnion_of_directed, NonUnitalSubring.coe_sSup_of_directedOn, AlgebraicGeometry.isCompactOpen_iff_eq_basicOpen_union, Subsemigroup.closure_iUnion, PointedCone.dual_iUnion, tsum_iUnion_decode₂, FiniteExhaustion.iUnion_eq', FirstOrder.Language.Substructure.closure_iUnion, Topology.CWComplex.union, MonoidAlgebra.support_gen_of_gen, iUnion_op_smul_set, MeasureTheory.OuterMeasure.sInf_apply, MeasureTheory.iUnion_spanningSets, Finset.sUnion_disjiUnion, NumberField.mixedEmbedding.iUnion_negAt_plusPart_union, finite_diff_iUnion_Ioo', IntermediateField.iSup_eq_adjoin, SimpleGraph.set_walk_length_succ_eq, MeasureTheory.AEDisjoint.iUnion_right_iff, IsLindelof.elim_nhds_subcover, isOpen_iUnion, Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT, Filter.EventuallyLE.biUnion, IsGLB.biUnion_Ioi_eq, MeasureTheory.measure_biUnion_finset_le, Finset.isPWO_bUnion, Vitali.exists_disjoint_covering_ae, Int.image_fract, IsCompact.elim_nhds_subcover', Ideal.subset_union_prime_finite, Topology.IsConstructible.biUnion, UpperSet.coe_iInf, lowerClosure_iUnion, coe_unionEqSigmaOfDisjoint_symm_apply, pairwise_iUnion₂, Finite.ncard_biUnion_le, div_iUnion₂, fixingSubgroup_iUnion, iUnion_eq_iUnion_finset, MeasureTheory.Measure.restrict_iUnion_ae, NonUnitalSubsemiring.closure_iUnion, Besicovitch.exists_disjoint_closedBall_covering_ae, HomogeneousIdeal.irrelevant_eq_span, iUnion_congr, biUnion_mono, mapsTo_iUnion₂_iUnion₂, union_iUnion_nat_succ, MeasureTheory.Measure.restrict_finset_biUnion_congr, Finite.isCompact_biUnion, Finite.closure_sUnion, IsPiSystem.tendsto_probabilityMeasure_biUnion, Filter.HasBasis.totallyBounded_iff, SimpleGraph.Subgraph.verts_iSup, Metric.infEDist_iUnion, prod_iUnion₂, closure_iUnion_of_finite, iUnion_image_left, coe_snd_biUnionEqSigmaOfDisjoint, MeasureTheory.AEDisjoint.iUnion_left_iff, iUnion_pi_of_monotone, MeasureTheory.Content.innerContent_iUnion_nat, NonUnitalSubring.closure_iUnion, MeasureTheory.OuterMeasure.boundedBy_apply, Finset.mulSupport_prod, vadd_set_iUnion, sub_iUnion, IsCompact.elim_nhdsWithin_subcover', IntermediateField.adjoin_iUnion, Metric.AreSeparated.finite_iUnion_right_iff, MeasureTheory.Measure.restrict_biUnion_finset_congr, AddSubgroup.closure_iUnion, insert_iUnion, sUnion_smul, TopologicalSpace.IsTopologicalBasis.sigma, Topology.CWComplex.cellFrontier_subset_finite_openCell, convexHull_eq_union_convexHull_finite_subsets, PolishSpace.IsClopenable.iUnion, iUnion_Icc_left, union_support_maximal_linearIndependent_eq_range_basis, sUnion_image, image2_sUnion_left, Filter.HasBasis.liminf_eq_sSup_iUnion_iInter, TopologicalSpace.Opens.iSup_def, isComplete_iUnion_separated, MeasureTheory.Measure.restrict_biUnion, FirstOrder.Language.distinctConstantsTheory_eq_iUnion, MeasureTheory.measureReal_iUnion_fintype_le, MeasureTheory.lintegral_iUnion, ENNReal.tsum_biUnion', iSup_indicator, AddAction.isTopologicallyTransitive_iff_dense_iUnion, MeasureTheory.measure_biUnion_finset₀, SigmaCompactSpace.exists_compact_covering, AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty, ENNReal.iUnion_Ioo_coe_nat, AddAction.quotient_preimage_image_eq_union_add, Filter.EventuallyEq.iUnion, Function.mulSupport_iInf, IsPiSystem.tendsto_measureReal_biUnion, ContDiffOn.iUnion_of_isOpen, Summable.tsum_finset_bUnion_disjoint, Topology.RelCWComplex.mapsTo, Topology.CWComplex.iUnion_openCell_eq_skeleton, MeasureTheory.measure_biUnion_finset, TopologicalSpace.Clopens.coe_finset_sup, iUnion_Ioc_left, Submodule.iSup_eq_span', Finite.bddBelow_biUnion, Matroid.IsBasis.isBasis_iUnion, MeasureTheory.projectiveFamilyContent_iUnion_le, ProbabilityTheory.CondIndepSets.bUnion, iUnion_inter_of_monotone, MeasureTheory.OuterMeasure.isCaratheodory_sum, Filter.HasBasis.biInter_biUnion_ball, NonUnitalStarSubalgebra.coe_iSup_of_directed, SetRel.preimage_iUnion, MeasureTheory.LocallyIntegrableOn.exists_nat_integrableOn, MDifferentiableOn.iUnion_of_isOpen, smul_iUnion₂, TopologicalSpace.Opens.coe_sSup, mem_iUnion_of_mem, MeasureTheory.integrableOn_iUnion_of_summable_integral_norm, Dynamics.coverEntropy_biUnion_le, hasCardinalLT_iUnion, sUnion_mul, sub_sUnion, iUnion_option, iUnion_iInter_subset, iUnion_vadd_right_image, BoxIntegral.Prepartition.iUnion_def', coe_upperClosure, Subfield.coe_sSup_of_directedOn, Metric.totallyBounded_iff, MeasureTheory.Measure.restrict_biUnion_congr, finite_iUnion_of_subsingleton, biUnion_associatedPrimes_eq_compl_nonZeroDivisors, iInf_iUnion, Encodable.iUnion_decode₂_disjoint_on, finite_cover_nhds_interior, image2_iUnion_left, PrimeSpectrum.zeroLocus_iUnion₂, iUnion_eq_empty, Filter.iInf_sets_eq_finite, IsClopen.biUnion_connectedComponentIn, EMetric.totallyBounded_iff, diff_iUnion, toFinset_iUnion, ncard_iUnion_of_finite, Submodule.coe_iSup_of_directed, HahnSeries.SummableFamily.sum_vAddAntidiagonal_eq, iUnion_true, Monotone.tendsto_indicator, iUnion_eq_if, gauge_lt_eq', Subsemiring.coe_sSup_of_directedOn, sUnion_add, Function.Surjective.iUnion_comp, AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, SetRel.image_eq_biUnion, nhdsKer_biUnion, upperPolar_iUnion₂, TopologicalSpace.isOpen_biUnion_countable, inter_iUnion, iUnion_subtype, exists_locallyFinite_subset_iUnion_ball_radius_lt, MeasureTheory.Measure.restrict_iUnion_apply_ae, biUnion_accumulate, Metric.biUnion_lt_closedBall, MeasureTheory.integrableOn_iUnion_of_summable_norm_restrict, sigmaToiUnion_injective, isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis, TopologicalSpace.IsOpenCover.iUnion_inter, MulAction.isTopologicallyTransitive_iff_dense_iUnion, MeasureTheory.IsSetRing.biUnion_mem, iUnion₂_mono', totallyBounded_iff_subset, iUnion_exists, preimage_sUnion, MeasurableSpace.measurableSet_iUnion, ShrinkingLemma.PartialRefinement.subset_iUnion, PairwiseDisjoint.finite_biUnion_iff, fixingSubmonoid_iUnion, iUnion_finset_eq_set, iUnion_Ico_right, MeasureTheory.Measure.hausdorffMeasure_apply, Submodule.span_biUnion, MeasurableSpace.generateFrom_iUnion_memPartition, iUnion_vsub_right_image, MeasureTheory.OuterMeasure.IsMetric.finset_iUnion_of_pairwise_separated, biUnion_eq_iUnion, Dynamics.coverEntropyInf_iUnion_le, smul_set_iUnion, IsLUB.biUnion_Iio_eq, iUnion₂_mul, Submodule.iInf_colon_iUnion, FirstOrder.Language.age_directLimit, accumulate_subset_iUnion, Algebra.adjoin_iUnion, iUnion_sum, iUnion_false, iUnion₂_congr, exists_clopen_partition_of_clopen_cover, Dense.biUnion_uniformity_ball, AddSubsemigroup.coe_sSup_of_directed_on, Metric.biUnion_lt_ball, lowerBounds_iUnion, finprod_mem_iUnion, MeasureTheory.OuterMeasure.sInf_apply', NFA.evalFrom_iUnion, Absorbs.biUnion, MeasurableSet.biUnion, MeasureTheory.NullMeasurableSet.iUnion, Ideal.univ_eq_iUnion_image_add, MeasurableSpace.generateMeasurableRec_omega_one, MeasurableSpace.DynkinSystem.has_iUnion, mapsTo_iUnion₂, ContMDiffOn.iUnion_of_isOpen, Finsupp.supported_iUnion, Metric.IsCover.subset_iUnion_closedBall, FirstOrder.Language.Theory.CompleteType.iInter_setOf_subset, iUnion_Ico_left, Metric.isCover_iff_subset_iUnion_closedEBall, Monotone.iUnion_comp_tendsto_atTop, Disjoint.exists_uniform_thickening, Finset.set_biUnion_union, MeasureTheory.measure_iUnion_fintype_le, iUnion_Ici_eq_Ioi_iInf, TopologicalSpace.IsTopologicalBasis.open_eq_iUnion, MeasureTheory.tendsto_measure_iUnion_accumulate, isClopen_iUnion₂, Bornology.isVonNBounded_biUnion, BoxIntegral.TaggedPrepartition.iUnion_def, mapsTo_iUnion_iUnion, Finite.eventuallyLE_iUnion, iUnion_sub_right_image, IsConnected.iUnion_of_chain, Finite.encard_biUnion, iUnion₂_sub, iUnion_sigma', Subsemigroup.coe_iSup_of_directed, SSet.degenerate_eq_iUnion_range_σ, iUnion_mono, countable_cover_nhds_of_sigmaCompact, Infinite.iUnion, dimH_iUnion, vadd_iUnion, TopologicalSpace.IsOpenCover.exists_finite_clopen_cover, Topology.RelCWComplex.iUnion_skeleton_eq_complex, pairwise_iUnion₂_iff, Finset.set_biUnion_option_toFinset, setOf_liouville_eq_iInter_iUnion, biUnion_subset_biUnion_left, Monotone.measure_iUnion, iUnion_inter_of_antitone, IsRelUpperSet.iUnion, AddSubmonoid.closure_iUnion, hasProd_prod_disjoint, preimage_iUnion, exists_finite_cover_balls_of_isCompact_closure, iUnion_psigma, Metric.AreSeparated.finset_iUnion_left, tprod_iUnion_decode₂, MeasureTheory.Measure.haar.index_defined, ENNReal.iUnion_Ioc_coe_nat, QuotientAddGroup.preimage_image_mk_eq_iUnion_image, countable_iUnion_iff, MeasurableSpace.iSup_generateFrom, mapsTo_iUnion, Monotone.mulIndicator_eventuallyEq_iUnion, Finite.Set.finite_biUnion, Dynamics.coverEntropyInf_biUnion_le, MeasureTheory.preVariation.sum_le_preVariationFun_iUnion, Finite.biUnion, iUnion_univ_pi_of_monotone, convexHull_eq_union, LowerSet.coe_iSup₂, AddMonoidAlgebra.support_gen_of_gen, Matroid.IsCircuit.strong_multi_elimination, isOpen_biUnion, totallyBounded_iUnion, NFA.evalFrom_biUnion, Finite.nullMeasurableSet_biUnion, Matroid.IsCircuit.strong_multi_elimination_insert, Finite.eventuallyEq_iUnion, Metric.isCover_iff_subset_iUnion_closedBall, FiniteExhaustion.iUnion_eq, iUnion_Ico_map_succ_eq_Ici, MeasureTheory.measureReal_biUnion_finset_le, FreeGroup.Orbit.duplicate, ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal, PMF.support_seq, iUnion₂_vsub, ZFSet.toSet_iUnion, isGLB_iUnion_iff_of_isLUB, iUnion_eq_iUnion_finset', biUnion_lt_eq_iUnion, Ideal.subset_union_prime, iUnion_empty, LieSubalgebra.span_iUnion, MeasureTheory.integrableOn_finite_biUnion, MeasureTheory.AnalyticSet.iUnion, iUnion₂_vadd, totallyBounded_iff_subset_finite_iUnion_nhds_one, UpperSet.coe_sInf, sUnion_iUnion, biUnion_ge, finprod_mem_biUnion, isCompact_iUnion, MeasurableSet.iUnion, IsCompact.elim_nhds_subcover_nhdsSet', vsub_iUnion₂, Finset.prod_indicator_biUnion_sub_indicator, biInter_subset_biUnion, iUnion_congr_Prop, Countable.biUnion_iff, biUnion_and', CategoryTheory.Subfunctor.iSup_obj, biUnion_finsetSigma', sUnion_div, iUnion_and, NonUnitalSubring.coe_iSup_of_directed, MeasureTheory.measureReal_biUnion_finset₀, biUnion_le_eq_iUnion, NFA.acceptsFrom_iUnion, biUnion_Ioc_eq_Ioi_self_iff, HomogeneousIdeal.irrelevant_eq_closure, smul_iUnion, upperClosure_iUnion, SetRel.preimage_sUnion, DoubleCoset.union_quotToDoubleCoset, Ideal.iUnion_minimalPrimes, MeasureTheory.measure_iUnion_eq_iSup_accumulate, iUnion_vadd_set, surjOn_iUnion_iUnion, AddSubgroup.exists_leftTransversal_of_FiniteIndex, TotallyBounded.exists_subset, Ideal.Quotient.quotient_ring_saturate, MeasurableSpace.generateFrom_iUnion_memPartition_le, MeasurableSet.iUnion_of_monotone, mulIndicator_biUnion_finset_eventuallyEq, IsLUB.biUnion_Iic_eq_Iic, union_eq_iUnion, MeasureTheory.addContent_biUnion_le, setOf_liouville_eq_irrational_inter_iInter_iUnion, Submonoid.closure_iUnion, sSup_iUnion_Iic, Metric.ediam_iUnion_mem_option, partialSups_eq_biUnion_range, isClosed_biUnion_finset, Polynomial.rootSet_prod, iUnion_of_singleton_coe, iUnion_univ_pi, iUnion₂_eq_univ_iff, iUnion_prod, preimage_iUnion₂, Matroid.closure_biUnion_congr, image2_eq_iUnion, iUnion₂_subset_iff, BoxIntegral.Prepartition.iUnion_ofWithBot, MeasurableSpace.generateMeasurableRec_omega1, MeasureTheory.OuterMeasure.IsCaratheodory.biUnion_of_finite, isClosed_iUnion₂, Subgroup.closure_iUnion, range_eq_iUnion, RealRMK.range_cut_partition, Int.preimage_fract, MeasureTheory.OuterMeasureClass.measure_iUnion_nat_le, Besicovitch.exists_disjoint_closedBall_covering_ae_aux, PairwiseDisjoint.biUnion_finset, sized_iUnion, Subsemigroup.iSup_eq_closure, SimpleGraph.Subgraph.verts_sSup, iUnion_setOf, Disjoint.exists_uniform_thickening_of_basis, finsum_mem_biUnion, Ico_subset_biUnion_Ico, Metric.isCover_iff_subset_iUnion_emetricClosedBall, Filter.ker_sSup, iUnion₂_div, sSupIndep_iUnion_of_directed, iUnion_Ioc_intCast, biUnion_pair, Metric.AreSeparated.finset_iUnion_right, BaireMeasurableSet.iUnion, MeasureTheory.OuterMeasure.biInf_apply', MeasureTheory.OuterMeasure.isCaratheodory_iUnion_of_disjoint, MeasureTheory.VectorMeasure.m_iUnion, MeasureTheory.measureReal_biUnion_eq_sum_powerset, pairwiseDisjoint_iUnion, sigmaToiUnion_surjective, NonUnitalSubsemiring.coe_sSup_of_directedOn, TopologicalSpace.Compacts.isCompact_biUnion_coe_of_isCompact, encard_iUnion_le_of_fintype, bind_def, MeasureTheory.SimpleFunc.support_eq, Finset.set_biUnion_preimage_singleton, Cardinal.mk_biUnion_le_of_le, ProperCone.innerDual_iUnion, MeasureTheory.squareCylinders_eq_iUnion_image, Monotone.biUnion_Ico_Ioc_map_succ, biUnion_image2, sUnion_sub, iUnion_vadd_eq_setOf_exists, Real.borel_eq_generateFrom_Iic_rat, Topology.CWComplex.mapsTo, MulAction.quotient_preimage_image_eq_union_mul, iUnion_of_singleton, Matroid.disjointSigma_isBase_iff, directedOn_iUnion, gauge_lt_eq, BaireMeasurableSet.biUnion, FirstOrder.Ring.mvPolynomial_zeroLocus_definable, MeasureTheory.VectorMeasure.restrict_le_restrict_countable_iUnion, Filter.generate_iUnion, Finset.indicator_biUnion_eq_sum_powerset, nhdsKer_sUnion, biUnion_finsetSigma_univ', Submodule.colon_iUnion, SetRel.image_iUnion, MeasureTheory.OuterMeasure.f_iUnion, stableUnderGeneralization_iUnion, bijOn_iUnion_of_directed, IsRelUpperSet.iUnion₂, iUnion_eq_dif, iUnion_Iic_eq_Iic_iSup, smul_sUnion, einfsep_iUnion_mem_option, Metric.finite_approx_of_totallyBounded, MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat, MeasureTheory.ae_restrict_iUnion_iff, SimpleGraph.killCopies_def, Finset.set_biUnion_insert, Dense.Ioi_eq_biUnion, Matroid.disjointSigma_ground_eq, Matroid.closure_biUnion_closure_eq_closure_biUnion, Finset.partiallyWellOrderedOn_bUnion, iUnion_Iio_eq_univ_iff, CompactSpace.elim_nhds_subcover, iUnion_Ici_eq_Ici_iInf, MeasureTheory.measure_biUnion_null_iff, Filter.isOpen_iff, MeasureTheory.OuterMeasure.iUnion_eq_of_caratheodory, MeasureTheory.lintegral_biUnion₀, IsCompact.nhdsSet_basis_uniformity, Cardinal.mk_iUnion_Ordinal_lift_le_of_le, closure_iUnion₂_le_nat, Finite.encard_biUnion_le, Topology.CWComplex.Subcomplex.union_closedCell, EventuallyEq.countable_iUnion, discreteTopology_biUnion_finset, pi_iUnion_eq_iInter_pi, Subsemigroup.coe_sSup_of_directed_on, iUnion_sub, Finset.apply_union_le_sum, iUnion_or, MeasureTheory.Measure.sum_restrict_le, Metric.iUnion_closedBall_nat, Filter.ker_iSup, biUnion_sigma, MeasureTheory.integral_iUnion_fintype, Finset.support_sum, biUnion_diff_biUnion_eq, LocallyFinite.continuousOn_iUnion, Finite.isClosed_biUnion, MeasureTheory.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint, AddMonoidAlgebra.support_gen_of_gen', MeasureTheory.LocallyIntegrable.exists_nat_integrableOn, Metric.AreSeparated.finite_iUnion_left_iff, ENNReal.tsum_iUnion_le, MeasureTheory.measure_iUnion_toMeasurable, SimpleGraph.ConnectedComponent.biUnion_supp_eq_supp, EMetric.totallyBounded_iff', ProbabilityTheory.Kernel.IndepSets.bUnion, Union_closure_singleton_eq_iff, MeasureTheory.OuterMeasure.ofFunction_apply, Pairwise.biUnion_injective, MeasurableSet.iUnion_of_monotone_of_frequently, biUnion_Ici_Ioc_map_succ, disjoint_iUnion₂_left, Cardinal.mk_biUnion_le_of_le_lift, SetRel.iUnion_comp, tendstoLocallyUniformlyOn_iUnion, IsGδ.iUnion, Filter.EventuallyEq.cardinal_bUnion, iUnion_vadd_left_image, MeasureTheory.Measure.restrict_iUnion_congr, AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_basicOpen, Finset.measurableSet_biUnion, iUnion_smul_left_image, iInter_subset_iUnion, finite_iUnion_iff, totallyBounded_iff_subset_finite_iUnion_nhds_zero, MeasureTheory.setLIntegral_iUnion_of_directed, iUnion₂_smul, PrimeSpectrum.vanishingIdeal_iUnion, diff_iInter, Absorbs.iUnion, IsOpen.dense_iUnion_vadd, iUnion_Icc_right, Subgroup.iSup_eq_closure, Matroid.closure_iUnion_congr, TopologicalSpace.IsTopologicalBasis.exists_countable_biUnion_of_isOpen, inj_on_iUnion_of_directed, sUnion_inv, Metric.cthickening_subset_iUnion_closedBall_of_lt, MeasureTheory.ae_eq_restrict_iUnion_iff, MeasureTheory.AEStronglyMeasurable.iUnion, biUnion_le_succ, ENNReal.tsum_biUnion_le_tsum, isPreconnected_iUnion, Vitali.exists_disjoint_covering_ae', iUnion_Ioo_left, iUnion_inter_iUnion, iUnion_insert_eq_range_union_iUnion, closure_sUnion, iUnion_Ico_zsmul, Filter.iSup_principal, AlgebraicGeometry.QuasiCompactCover.exists_isAffineOpen_of_isCompact, isLindelof_iUnion, convexJoin_singleton_right, stableUnderSpecialization_iff_Union_eq, nhdsWithin_iUnion, Cardinal.mk_iUnion_le, biUnion_image, iUnion_unpair, Projectivization.Subspace.span_iUnion, Filter.hasBasis_iSup, Cardinal.card_biUnion_lt_iff_forall_of_isRegular, nhdsKer_iUnion, Cardinal.iSup_mk_le_mk_iUnion, TopologicalSpace.IsOpenCover.exists_finite_nonempty_disjoint_clopen_cover, Metric.AreSeparated.finset_iUnion_left_iff, CompactExhaustion.iUnion_eq', biUnion_Ioc_disjointed_of_monotone, IsOpen.iUnion_preimage_smul, iUnion_Iic_of_not_bddAbove_range, IsGLB.biUnion_Ici_eq_Ioi, finsum_mem_iUnion, compact_covered_by_mul_left_translates, add_iUnion₂, iUnion_Ici, Topology.RelCWComplex.disjoint_base_iUnion_openCell, LocallyFinite.continuousOn_iUnion', Topology.RelCWComplex.union, Infinite.biUnion, iUnion_image_inf_left, Profinite.NobelingProof.GoodProducts.union, balanced_iUnion, Metric.infEDist_biUnion, MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀, iInter_iUnion_of_monotone, image2_sUnion_right, Filter.iInf_eq_generate, fixingAddSubmonoid_iUnion, EventuallyEq.countable_bUnion, IsRelLowerSet.iUnion, IsGLB.iUnion_Ioi_eq, isSigmaCompact_biUnion, Submodule.span_iUnion₂, seq_def, Matroid.closure_biUnion_closure_eq_closure_sUnion, iUnion_image_inf_right, div_iUnion, BijOn.iUnion_congr, IndexedPartition.range_piecewise, Ideal.span_iUnion, AddSubmonoid.iSup_eq_closure, Submodule.coe_iSup_of_chain, iUnion₂_inter_iUnion₂, surjOn_iUnion₂, IsChain.pairwise_iUnion₂, MeasureTheory.measure_iUnion_congr_of_subset, iUnion_iUnion_eq', Real.isPiSystem_Ioo_rat, Matroid.IsRkFinite.iUnion, MeasureTheory.Measure.restrict_iUnion_le, iUnion_add_left_image, MeasurableSpace.iUnion_mem_generateMeasurableRec, Topology.RelCWComplex.disjoint_interior_base_iUnion_closedCell, MeasureTheory.measure_biUnion₀, image2_iUnion₂_left, upperPolar_iUnion, ncard_iUnion_le_of_finite, CategoryTheory.MorphismProperty.toSet_iSup, LowerAdjoint.closure_iUnion_closure, EMetric.diam_iUnion_mem_option, ProbabilityTheory.CondIndepSets.biUnion, Subring.closure_iUnion, MeasureTheory.AECover.biUnion_Iic_aecover, Finset.mulIndicator_biUnion, MeasureTheory.integral_finset_biUnion, IndexedPartition.range_piecewise_subset, iUnion_image_sup_left, isUpperSet_iUnion
iUnion_delab 📖	CompOp	—
instInfSet 📖	CompOp	8 math math: iInf_eq_iInter, ClosedSubmodule.coe_sInf, sInf_eq_sInter, CategoryTheory.Subfunctor.sInf_obj, ClosedSubmodule.coe_iInf, CategoryTheory.Subfunctor.Subpresheaf.sInf_obj, FirstOrder.Language.ClosedUnder.sInf, IntermediateField.coe_sInf
instSupSet 📖	CompOp	6 math math: CategoryTheory.Subfunctor.sSup_obj, iSup_eq_iUnion, image_sSup, sSup_eq_sUnion, sSupHom.setImage_toFun, CategoryTheory.Subfunctor.Subpresheaf.sSup_obj
sInter 📖	CompOp	156 math math: sInter_eq_univ, AddGroupFilterBasis.t2Space_iff, cardinal_sInter_mem, Submodule.span_sInf_le, Finset.inf_id_set_eq_sInter, image_sInter_subset, sInter_union_sInter, Filter.mem_countableGenerate_iff, sInter_smul_subset, Matroid.fundCircuit_eq_sInter, FilterBasis.ker_filter, compl_sInter, sub_sInter_subset, sInter_empty, Finite.interior_sInter, sInter_prod, image2_sInter_subset_left, Finite.sInter, smul_sInter_subset, image2_sInter_subset_right, sInter_neg, Topology.IsConstructible.sInter, sInter_vadd_subset, Filter.mem_cardinaleGenerate_iff, stableUnderGeneralization_sInter, isOpen_sInter, MeasurableSet.sInter, GroupFilterBasis.t2Space_iff_sInter_subset, Balanced.sInter, Finite.absorbs_sInter, sInter_inv, sInter_insert, isIrreducible_iff_sInter, sInter_eq_iInter, CountableInterFilter.countable_sInter_mem, IsExposed.sInter, starConvex_sInter, FiniteInter.finiteInter_mem, IsRelLowerSet.sInter, nhdsSet_sInter_le, small_sInter, Filter.sInter_comap_sets, isLowerSet_sInter, sInter_sub_subset, AbsConvex.sInter, interior_sInter_subset, alexandrovDiscrete_iff, Filter.sInter_lift'_sets, sInter_eq_biInter, sInter_image2, sInter_subset_of_mem, sInter_union, Matroid.closure_def', sInter_vsub_subset, IsRelUpperSet.sInter, sInter_pair, AlexandrovDiscrete.isOpen_sInter, Topology.IsLocallyConstructible.sInter, sInter_iUnion, absConvex_closed_sInter, sInter_div_subset, sInf_eq_sInter, IsGδ.sInter, preimage_val_sInter_eq_sInter, Matroid.closure_def, sInter_diff_singleton_univ, LinearMap.sInter_polar_finite_subset_eq_polar, isSublattice_sInter, mapsTo_sInter, dense_sInter_of_Gδ, nonempty_sInter, Filter.sInter_lift_sets, sInter_mul_subset, TopologicalSpace.isTopologicalBasis_of_subbasis, interior_sInter, preimage_val_sInter, Filter.hasBasis_generate, small_sInter', Ordinal.IsClosedBelow.sInter, BaireMeasurableSet.sInter, sUnion_eq_compl_sInter_compl, sInter_prod_sInter, compl_sUnion, isExtreme_sInter, mul_sInter_subset, Finite.measurableSet_sInter, IsSymmetricRel.sInter, ZFSet.toSet_sInter, mem_sInter, NormedSpace.sInter_polar_eq_closedBall, preimage_sInter, nhdsKer_def, sInter_singleton, isClosed_sInter, image2_sInter_right_subset, IsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed, sInter_range, add_sInter_subset, Filter.mem_generate_iff, MeasureTheory.Measure.support_eq_sInter, Filter.generate_neBot_iff, subset_sInter_iff, stableUnderGeneralization_iff_exists_sInter_eq, supClosed_sInter, Filter.sInter_mem, IsSemilinearSet.sInter, sInter_add_subset, sInter_image, ZFSet.coe_sInter, IsRetrocompact.sInter, nhdsKer_sInter_subset, Finite.isOpen_sInter, subset_sInter, dense_sInter_of_isOpen, isUpperSet_sInter, Filter.generate_eq_generate_inter, SetRel.IsSymm.sInter, PrimitiveSpectrum.hull_sSup, vsub_sInter_subset, infClosed_sInter, isClopen_sInter, vadd_sInter_subset, Finite.nullMeasurableSet_sInter, Bornology.isCobounded_sInter, convex_closed_sInter, convex_sInter, sInter_subset_sInter, Filter.sInter_nhds, Absorbs.sInter, AddGroupFilterBasis.t2Space_iff_sInter_subset, smul_set_sInter_subset, Matroid.closure_sInter_eq_biInter_closure_of_sUnion_indep, mem_residual_iff, IsTransitiveRel.sInter, Matroid.Indep.inter_isBasis_sInter, sInter_eq_compl_sUnion_compl, MeasureTheory.NullMeasurableSet.sInter, sInter_prod_sInter_subset, sInter_mono, sInter_eq_empty_iff, stableUnderSpecialization_sInter, CardinalInterFilter.cardinal_sInter_mem, vadd_set_sInter_subset, SetRel.IsTrans.sInter, countable_sInter_mem, Filter.FilterBasis.ofSets_sets, Matroid.Indep.closure_sInter_eq_biInter_closure_of_forall_subset, prod_sInter, image2_sInter_left_subset, Finite.dense_sInter, div_sInter_subset, image_val_sInter, GroupFilterBasis.t2Space_iff, SetRel.IsRefl.sInter, Filter.mem_cardinalGenerate_iff, ordConnected_sInter
sInter_delab 📖	CompOp	—
sUnion 📖	CompOp	219 math math: Cardinal.mk_sUnion_le, TopologicalSpace.IsTopologicalBasis.open_eq_sUnion, dimH_sUnion, iUnion_range_eq_sUnion, MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_disjointOfDiffUnion, finprod_mem_sUnion, ProperCone.dual_sUnion, algebraicIndependent_sUnion_of_directed, iSupIndep_sUnion_of_directed, MeasureTheory.Measure.restrict_sUnion_congr, EquicontinuousOn.tendsto_uniformOnFun_iff_pi', Finite.nullMeasurableSet_sUnion, exists_sUnion, smul_set_sUnion, sUnion_inter_sUnion, compl_sInter, SetRel.image_sUnion, sUnion_range, Countable.isLindelof_sUnion, Finite.measurableSet_sUnion, Algebra.sSup_def, generateFrom_sUnion, Scott.isOpen_sUnion, nhdsWithin_sUnion, MeasurableSpace.sUnion_countablePartition, pairwise_sUnion, TopologicalSpace.NoetherianSpace.exists_finite_set_isClosed_irreducible, Matroid.IsCircuit.strong_multi_elimination_set, sUnion_eq_iUnion, sUnion_memPartition, MeasurableSet.sUnion, MeasureTheory.IsSetSemiring.disjointOfUnion_props, Finite.Set.finite_sUnion, ProperCone.innerDual_sUnion, sUnion_vsub, EquicontinuousOn.inducing_uniformOnFun_iff_pi', SetRel.sUnion_comp, Countable.sUnion_iff, Bornology.isVonNBounded_covers, finsum_mem_sUnion, Finite.sUnion, sUnion_insert, IsProperSemilinearSet.sUnion, alexandrovDiscrete_iff_isClosed, vsub_sUnion, sUnion_image2, starConvex_sUnion, Infinite.sUnion, sUnion_finite_eq_univ, disjoint_sUnion_left, isClosed_sUnion, isPreconnected_sUnion, directedOn_sUnion, image_sUnion, IntermediateField.sSup_def, MeasureTheory.IsSetSemiring.sUnion_disjointOfDiff, Bornology.sUnion_bounded_univ, MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq, SetRel.comp_sUnion, mul_sUnion, MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiffUnion, EquicontinuousOn.isClosed_range_pi_of_uniformOnFun', NonUnitalSubring.closure_sUnion, subset_sUnion_of_subset, sUnion_singleton, BaireMeasurableSet.sUnion, sUnion_neg, sUnion_irreducibleComponents, surjOn_sUnion, ZFSet.coe_sUnion, partialSups_eq_sUnion_image, DirectedOn.convex_sUnion, TopologicalSpace.IsTopologicalBasis.open_iff_eq_sUnion, pairwiseDisjoint_sUnion, IsChain.pairwise_sUnion, sUnion_mem_empty_univ, sInf_sUnion, IsChain.pairwiseDisjoint_sUnion, mapsTo_sUnion, MeasureTheory.IsSetSemiring.diff_eq_sUnion', vadd_set_sUnion, sUnion_subset, sUnion_eq_biUnion, Setoid.sUnion_classes, isSigmaCompact_sUnion_of_isCompact, MeasureTheory.IsSetSemiring.sUnion_union_disjointOfDiffUnion_of_subset, sUnion_vadd, MeasureTheory.Measure.compl_support_eq_sUnion, sUnion_subset_iff, Subfield.closure_sUnion, Subsemiring.closure_sUnion, MeasureTheory.IsSetSemiring.sUnion_insert_disjointOfDiff, DirectedOn.strictConvex_sUnion, orthonormal_sUnion_of_directed, add_sUnion, Finite.isCompact_sUnion, MeasureTheory.IsSetSemiring.sUnion_disjointOfUnion, MeasureTheory.NullMeasurableSet.sUnion, sSup_eq_sUnion, MeasureTheory.IsSetSemiring.sUnion_disjointOfDiffUnion_subset, Submodule.span_sSup, MeasurableSpace.measurableSet_generateFrom_memPartition_iff, lowerClosure_sUnion, stableUnderGeneralization_sUnion, asymptoticCone_sUnion, stableUnderSpecialization_sUnion, div_sUnion, exists_seq_cover_iff_countable, Bornology.isVonNBounded_sUnion, EquicontinuousOn.comap_uniformOnFun_eq, sUnion_mono_subsets, Absorbs.sUnion, SimpleGraph.induce_sUnion_connected_of_pairwise_not_disjoint, IsSemilinearSet.sUnion, MeasurableSpace.measurableSet_generateFrom_countablePartition_iff, sUnion_subset_sUnion, stableUnderSpecialization_iff_exists_sUnion_eq, vadd_sUnion, Bornology.isBounded_sUnion, sUnion_mono, Finset.sUnion_disjiUnion, mem_sUnion_of_mem, NonUnitalSubsemiring.closure_sUnion, sUnion_mono_supsets, Finite.closure_sUnion, Pi.induced_restrict_sUnion, disjoint_sUnion_right, UniformOnFun.edist_def, nonempty_sUnion, sUnion_eq_compl_sInter_compl, sUnion_smul, MeasureTheory.IsSetSemiring.subset_of_diffUnion_disjointOfDiffUnion, compl_sUnion, sUnion_image, image2_sUnion_left, TopologicalSpace.Closeds.coe_sSup, TopologicalSpace.isOpen_sUnion_countable, UniformOnFun.uniformContinuous_restrict_toFun, upperClosure_sUnion, isLowerSet_sUnion, isSigmaCompact_sUnion, sUnion_mul, sub_sUnion, sUnion_pair, Order.isIdeal_sUnion_of_directedOn, sUnion_add, preimage_val_sUnion, sSup_sUnion, closure_sUnion_irreducibleComponents_diff_singleton, isMeagre_iff_countable_union_isNowhereDense, MeasureTheory.measure_sUnion₀, preimage_sUnion, IsRelLowerSet.sUnion, Order.isIdeal_sUnion_of_isChain, subset_sUnion_of_mem, sUnion_isCompact_eq_univ, Pi.uniformSpace_comap_restrict_sUnion, sUnion_diff_singleton_empty, Setoid.IsPartition.sUnion_eq_univ, small_sUnion, IsPreconnected.sUnion_directed, Finite.isLindelof_sUnion, sUnion_union, PSet.toSet_sUnion, IsRetrocompact.sUnion, MeasureTheory.IsSetSemiring.disjointOfUnion_subset_of_mem, sUnion_iUnion, UniformOnFun.edist_eq_restrict_sUnion, isUpperSet_sUnion, sUnion_div, SetRel.preimage_sUnion, ZFSet.toSet_sUnion, tendstoLocallyUniformlyOn_sUnion, MeasureTheory.measure_sUnion, MeasureTheory.Measure.exists_ae_subset_biUnion_countable, mem_sUnion, isOpen_sUnion, TopologicalSpace.isOpen_sUnion, Ultrafilter.finite_sUnion_mem_iff, sUnion_eq_univ_iff, prod_sUnion, sUnion_sub, nhdsKer_sUnion, PointedCone.dual_sUnion, TopologicalSpace.IsTopologicalBasis.open_eq_sUnion', subset_powerset_iff, smul_sUnion, iInf_sUnion, Topology.IsConstructible.sUnion, sUnion_eq_empty, sUnion_powerset_gc, Bornology.sUnion_isVonNBounded_eq_univ, IsRelUpperSet.sUnion, Matroid.IsBasis.isBasis_sUnion, TopologicalSpace.IsTopologicalBasis.sUnion_eq, sInter_eq_compl_sUnion_compl, sUnion_empty, IsGδ.sUnion, Topology.IsLocallyConstructible.sUnion, sUnion_inv, Finset.sup_id_set_eq_sUnion, isClopen_sUnion, closure_sUnion, iSup_sUnion, totallyBounded_sUnion, MeasureTheory.IsSetSemiring.sUnion_union_sUnion_disjointOfDiffUnion_of_subset, MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiff, image_val_sUnion, ContinuousMap.compactOpen_eq_generateFrom, image2_sUnion_right, EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi', Matroid.closure_biUnion_closure_eq_closure_sUnion, MeasureTheory.measure_sUnion_null_iff, Subring.closure_sUnion, sUnion_prod_const, Countable.sUnion, eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open, Finite.absorbs_sUnion, linearIndepOn_sUnion_of_directed
«term⋂_,_» 📖	CompOp	—
«term⋂₀_» 📖	CompOp	—
«term⋃_,_» 📖	CompOp	—
«term⋃₀_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInf_eq_iInter 📖	mathematical	—	iInf Set instInfSet iInter	—	—
iSup_eq_iUnion 📖	mathematical	—	iSup Set instSupSet iUnion	—	—
mem_iInter 📖	mathematical	—	Set instMembership iInter	—	—
mem_iUnion 📖	mathematical	—	Set instMembership iUnion	—	—
mem_sInter 📖	mathematical	—	Set instMembership sInter	—	—
mem_sUnion 📖	mathematical	—	Set instMembership sUnion	—	—
sInf_eq_sInter 📖	mathematical	—	InfSet.sInf Set instInfSet sInter	—	—
sSup_eq_sUnion 📖	mathematical	—	SupSet.sSup Set instSupSet sUnion	—	—

SupSet

Definitions

Name	Category	Theorems
sSup 📖	CompOp	596 math math: SimpleGraph.Finsubgraph.coe_sSup, IsClosed.sSup_mem, dirSupClosed_iff_forall_sSup, sInf_image2_eq_sInf_sSup, Subsemiring.mem_sSup_of_directedOn, csSup_pair, AddCon.sSup_eq_addConGen, Subring.coe_sSup_of_directedOn, Filter.liminf_eq, isFullyInvariant_iff_sSup_isotypicComponents, Filter.HasBasis.liminf_eq_ite, FirstOrder.Language.Substructure.mem_sSup_of_directedOn, Real.sSup_smul_of_nonpos, IntermediateField.sSup_toSubfield, csSup_image2_eq_csInf_csInf, ENat.sSup_eq_top_of_infinite, unary_relation_sSup_iff, Subfield.mem_sSup_of_directedOn, ContinuousLinearMap.sSup_unit_ball_eq_norm, Pi.Lex.sSup_apply_le, Monotone.leftLim_eq_sSup, Nat.sSup_def, csSup_le_iff, DirectedOn.subset_Icc_csInf_csSup, ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm, ContinuousOn.le_sSup_image_Icc, csSup_le', Concept.extent_sSup, sSup_univ, Real.sSup_empty, SimpleGraph.Subgraph.neighborSet_sSup, Set.Icc.coe_sSup, ENat.smul_sSup, isLUB_iff_sSup_eq, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup, DirectedOn.csSup_eq_of_forall_le_of_forall_lt_exists_gt, continuous_sSup_dom, AntitoneOn.tendsto_nhdsGT, Nat.sSup_of_not_bddAbove, Subalgebra.op_sSup, isClosed_sSup_iff, Bornology.IsBounded.subset_Icc_sInf_sSup, sSup_Iio_eq_self_iff_isSuccPrelimit, sSup_eq_bot, Ideal.mem_sSup_of_mem, IsCompactlyGenerated.BooleanGenerators.sSup_inter, Subring.mem_sSup_of_directedOn, subset_sSup_emptyset, NNReal.coe_sSup, Nat.sSup_mem, Real.ediam_eq, sSup_Prop_eq, RingCon.sSup_def, ClosedSubmodule.coe_sSup, Algebra.sSup_def, sup_eq_top_of_top_mem, sSup_inf_sSup, Real.add_neg_lt_sSup, cbiSup_eq_of_not_forall, RootPairing.coe_chainBotCoeff_eq_sSup, Subsemigroup.mem_sSup_of_mem, sSupHomClass.map_sSup, Set.Nonempty.eq_Icc_iff_int, ConvexOn.univ_sSup_of_countable_affine_eq, toDual_sInf, sSup_disjoint_iff, IsCompact.sSup_mem, UpperSet.compl_sSup, PUnit.sSup_eq, Filter.frequently_sSup, sSup_prod, MonotoneOn.tendsto_nhdsLT, sSup_empty, ENNReal.toNNReal_sSup, ENNReal.inv_sSup, NonUnitalSubring.mem_sSup_of_directedOn, MeasurableSpace.measurableSet_sSup, Real.sInf_le_sSup, lt_csSup_iff, Real.tendsto_atTop_csSup_of_monotoneOn_bddAbove_nat_Ici, Antitone.sSup, Filter.sSup_lowerBounds, sSup_insert, ContinuousLinearMap.sSup_sphere_eq_nnnorm, GaloisConnection.l_csSup', Prod.swap_sSup, DirectedOn.csSup_le, DirectedOn.disjoint_sSup_left, WithTop.coe_sSup, OrderIso.map_csSup_of_directedOn, IsCompact.sSup_lt_iff_of_continuous, Submonoid.coe_sSup_of_directedOn, ENat.sSup_eq_zero, sSup_atoms_le_eq, toDual_sSup, csSup_eq_top_of_top_mem, sSup_union, CompleteSublattice.sSupClosed', Pi.Colex.sSup_apply, csSup_Icc, Real.sSup_smul_of_nonneg, Concept.intent_sSup, AddSubsemigroup.unop_sSup, CompleteLatticeHom.map_sSup', Ordinal.Principal.sSup, sSup_image2_eq_sInf_sInf, Ideal.Filtration.sSup_N, CompleteSemilatticeSup.le_sSup, compl_sSup', OrderHom.sSup_apply, DirectedOn.isLUB_sSup, CategoryTheory.Sieve.sSup_apply, csSup_le_csSup', sSup_isotypicComponents, CompleteAtomicBooleanAlgebra.eq_setOf_le_sSup_and_isAtom, DirectedOn.le_csSup_of_le, ENNReal.sSup_div, continuous_sSup_rng, Submodule.submodule_eq_sSup_le_nonzero_spans, csInf_div, Real.sSup_nonpos, AntitoneOn.tendsto_nhdsWithin_Ioo_right, Order.Frame.MinimalAxioms.sSup_inf_eq, ENNReal.coe_sSup, sSup_image2, csSup_image2_eq_csSup_csSup, ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove, csSup_le_iff', Ordinal.sSup_eq_bsup, Cardinal.lift_sSup, Monotone.tendsto_nhdsLT, Int.csSup_eq_greatestOfBdd, Submonoid.mem_sSup_of_directedOn, IsCompact.isLUB_sSup, sSup_singleton, LowerSet.coe_sSup, compl_sSup, Set.Nonempty.ordConnected_iff_of_bdd', Hyperreal.isSt_sSup, Submonoid.op_sSup, CategoryTheory.Subfunctor.sSup_obj, UpperSet.Ici_sSup, Set.Finite.csSup_lt_iff, IsConnected.Ioo_csInf_csSup_subset, DirectedOn.sSup_inf_eq, IsGreatest.csSup_mem, Subsemigroup.mem_sSup_of_directed_on, sInf_sub, sSup_compact_eq_top, Real.sSup_nonneg, IsQuantale.sSup_mul_distrib, Filter.eventually_sSup, ENat.mul_sSup, csSup_mul, Submodule.isOrtho_sSup_right, Subgroup.mem_sSup_of_directedOn, Antitone.tendsto_nhdsGT, compl_eq_sSup_disjoint, SupClosed.sSup_mem_of_nonempty, AddSubgroup.mem_sSup_of_directedOn, csSup_lowerBounds_eq_csInf, Ordinal.sSup_ord, csSup_one, ConvexOn.sSup_of_countable_affine_eq, sSup_inv, GroupSeminorm.sSup_of_not_bddAbove, ENat.coe_sSup, RootPairing.coe_chainTopCoeff_eq_sSup, BooleanSubalgebra.sSup_mem, sSup_mul, Setoid.sSup_def, isOpen_sSup_iff, Monotone.le_csSup_image, IntermediateField.sSup_def, RingCon.sSup_eq_ringConGen, OrderIso.map_sSup_eq_sSup_symm_preimage, iSup_inf_le_sSup_inf, sInf_neg, Partition.sSup_eq', Subring.op_sSup, HomogeneousIdeal.toIdeal_sSup, Set.image_sSup, Metric.ediam_eq_sSup, sInf_inv, Filter.liminf_eq_sSup_sInf, Finset.sup'_eq_csSup_image, SimpleGraph.Subgraph.sSup_adj, inf_sSup_eq, csSup_Ioo, LeftOrdContinuous.map_sSup', lowerClosure_eq_Iic_csSup, ContinuousOn.image_uIcc_eq_Icc, OrderHom.le_map_sSup_subset_fixedPoints, LieAlgebra.IsSemisimple.sSup_atoms_eq_top, ConvexOn.real_univ_sSup_of_countable_affine_eq, binary_relation_sSup_iff, ENat.add_sSup, csSup_Ioc, DirectedOn.csInf_le_csSup, NNReal.sSup_of_not_bddAbove, iSupIndep_def'', IsPreconnected.Iio_csSup_subset, ofDual_sInf, ContinuousOn.image_Icc, sSup_diff_singleton_bot, GaloisConnection.l_csSup_of_directedOn, csSup_eq_of_is_forall_le_of_forall_le_imp_ge, NonarchAddGroupSeminorm.sSup_of_not_bddAbove, Finset.Nonempty.csSup_mem, GaloisConnection.l_sSup, exists_seq_tendsto_sSup, WithTop.coe_sSup', IsLUB.sSup_eq, Submodule.restrictScalars_sSup, Antitone.map_sSup_le, DirectedOn.sSup_le, Antitone.map_csInf_of_continuousAt, UpperSet.mem_sSup_iff, coinduced_sSup, Set.Nonempty.csSup_mem, iSupIndep_def', Submodule.toAddSubmonoid_sSup, csSup_empty, OrderIso.map_csSup', AddSubgroup.ofAddUnits_sSup, Real.sInf_neg, Subalgebra.unop_sSup, Seminorm.sSup_empty, sSup_atoms_eq_top, IsSemisimpleModule.finite_tfae, GaloisInsertion.l_sSup_u_image, csSup_of_not_bddAbove, AddSubsemigroup.op_sSup, LinearPMap.domain_sSup, le_csSup_iff', le_sSup_of_le, ContinuousLinearMap.sSup_sphere_eq_norm, Algebra.sSup_toSubsemiring, sSup_eq_bot', Pi.Colex.sSup_apply_le, CompleteSublattice.coe_sSup', Order.pred_eq_sSup, Real.diam_eq, SimpleGraph.Subgraph.edgeSet_sSup, sSup_lowerBounds_eq_sInf, IsQuantale.mul_sSup_distrib, Subgroup.mem_sSup_of_mem, eq_Icc_of_connected_compact, sSup_image2_eq_sSup_sSup, Con.sSup_eq_conGen, AddSubmonoid.coe_sSup_of_directedOn, sSup_one, ciSup_eq_univ_of_not_bddAbove, AddSubmonoid.unop_sSup, sSup_iUnion, CompleteSemilatticeSup.sSup_le, Seminorm.coe_sSup_eq', ContinuousOn.isBigOWith_principal, DividedPowers.SubDPIdeal.sSup_carrier_def, TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompact, ContinuousOn.image_uIcc, Digraph.sSup_adj, Finset.Nonempty.csSup_eq_max', IsSemisimpleModule.sSup_simples_le, Submodule.sInf_orthogonal, le_csSup_iff, sSup_le_sSup_of_subset_insert_bot, AntitoneOn.map_sInf_of_continuousWithinAt, AddGroupSeminorm.coe_sSup_apply, Set.Iic.coe_sSup, csInf_le_csSup, Set.sSup_eq_sUnion, CompleteLattice.ωScottContinuous.sSup, WithBot.sSup_empty, sSupIndep.disjoint_sSup, AddSubgroup.op_sSup, Submodule.span_sSup, Filter.bliminf_eq, FrameHom.map_sSup', iSup_inf_le_inf_sSup, Ordinal.mem_closure_tfae, MonotoneOn.tendsto_nhdsWithin_Ioo_left, csSup_inv, Real.sSup_le, LieSubmodule.sSup_toSubmodule, MeasureTheory.OuterMeasure.sSup_apply, ConvexOn.real_univ_sSup_affine_eq, TwoSidedIdeal.sSup_ringCon, Set.Ici_sSup, ContinuousLinearMap.sSup_unit_ball_eq_nnnorm, csInf_image2_eq_csSup_csInf, IsClosed.csSup_mem, ConditionallyCompleteLattice.csSup_le, SimpleGraph.sSup_adj, Filter.HasBasis.liminf_eq_sSup_univ_of_empty, Prod.fst_sSup, AddCon.sSup_def, sSup_eq_iSup, Filter.limsSup_eq_iInf_sSup, IsSemisimpleModule.sSup_simples_eq_top, ENat.sSup_add, AddGroupSeminorm.coe_sSup_apply', FrameHomClass.map_sSup, Set.Nonempty.ordConnected_iff_of_bdd, Order.Frame.MinimalAxioms.inf_sSup_eq, LieSubmodule.sSup_image_lieSpan_singleton, csSup_insert, AddSubmonoid.op_sSup, ENNReal.mul_sSup, sSup_div, Real.sSup_univ, ConvexOn.hasDerivWithinAt_sSup_slope_of_mem_interior, Ideal.IsHomogeneous.sSup, Set.Infinite.Nat.sSup_eq_zero, ENNReal.sSup_mul, eq_Icc_csInf_csSup_of_connected_bdd_closed, add_sSup_distrib, essInf_eq_sSup, Filter.limsSup_principal_eq_csSup, le_csSup_of_le, Submodule.mem_sSup_of_mem, NonUnitalSubring.coe_sSup_of_directedOn, sInf_image2_eq_sSup_sSup, Order.pred_eq_csSup, ClosedSubmodule.toSubmodule_sSup, CStarModule.norm_eq_csSup, Int.csSup_of_not_bddAbove, AntitoneOn.map_csInf_of_continuousWithinAt, TopologicalSpace.Opens.mem_sSup, subset_sSup_of_not_bddAbove, CompletePartialOrder.scottContinuous, DirectedOn.le_csSup_iff, ULift.down_sSup, Int.csSup_eq_greatest_of_bdd, disjoint_sSup_iff, inf_sSup_eq_iSup_inf_sup_finset, GaloisConnection.l_csSup, Seminorm.coe_sSup_eq, Filter.join_principal_eq_sSup, ENNReal.add_sSup, Subsemiring.op_sSup, CompleteSublattice.sSupClosed, IsCompactlyGenerated.exists_sSup_eq, RootPairing.chainBotCoeff_eq_sSup, GroupSeminorm.coe_sSup_apply', sSup_neg, IsClosed.isGreatest_csSup, IsCompactlyGenerated.BooleanGenerators.sSup_le_sSup_iff_of_atoms, ConvexOn.univ_sSup_affine_eq, csInf_neg, TopologicalSpace.NoetherianSpace.exists_finite_set_closeds_irreducible, LieSubmodule.sSup_toSubmodule_eq_iSup, CompleteSublattice.coe_sSup, Filter.comap_sSup, ENat.sSup_mul, WithTop.sSup_eq, sSup_sub, ClosedSubmodule.mem_sSup, ConvexOn.leftDeriv_eq_sSup_slope_of_mem_interior, sInf_image2_eq_sSup_sInf, ConvexOn.real_sSup_of_countable_affine_eq, gc_sSup_Iic, Filter.HasBasis.liminf_eq_sSup_iUnion_iInter, Ideal.homogeneousCore'_eq_sSup, TopologicalSpace.Closeds.coe_sSup, sSup_mul_distrib, AddSubsemigroup.mem_sSup_of_mem, subset_sSup_def, IsLUB.csSup_eq, ConditionallyCompletePartialOrderSup.isLUB_csSup_of_directed, DirectedOn.lt_csSup_of_lt, Order.IsSuccLimit.sSup_Iio, le_sSup_iff, ENNReal.toReal_sSup, sSup_compact_le_eq, Submonoid.unop_sSup, LeftOrdContinuous.map_csSup, DirectedOn.le_csSup, ClosedSubmodule.sInf_orthogonal, csSup_singleton, DirectedOn.csSup_le_iff, csSup_eq_of_forall_le_of_forall_lt_exists_gt, Ordinal.IsNormal.map_sSup_of_bddAbove, Order.IsNormal.preimage_Iic, TopologicalSpace.Opens.coe_sSup, Monotone.le_map_sSup, Submodule.span_sSup', DirectedOn.csSup_le_csSup, Subfield.coe_sSup_of_directedOn, sSup_eq_top, WithTop.isLUB_sSup, ENNReal.smul_sSup, isOrderRightAdjoint_csSup, Int.csSup_mem, Subsemiring.coe_sSup_of_directedOn, ciSup_of_not_bddAbove, ENNReal.sSup_add, Ordinal.IsNormal.map_sSup, Setoid.sSup_eq_eqvGen, Filter.sSup_sets_eq, Set.exists_seq_iSup_eq_top_iff_countable, Finset.sup_eq_sSup_image, sSup_image, AddSubgroup.mem_sSup_of_mem, MeasureTheory.Filtration.sSup_def, MonotoneOn.csSup_eq_of_subset_of_forall_exists_le, RootPairing.chainTopCoeff_eq_sSup, csInf_upperBounds_eq_csSup, sSup_sUnion, LowerSet.compl_sSup, subset_Icc_csInf_csSup, ciSup_eq_ite, DirectedOn.inf_sSup_eq, Real.sInf_smul_of_nonpos, SupClosed.sSup_mem, lt_csSup_of_lt, CompleteLatticeHomClass.map_sSup, sSup_image2_eq_sSup_sInf, Finset.sup'_id_eq_csSup, mul_sSup_distrib, Submodule.span_biUnion, ULift.up_sSup, Real.sSup_def, CategoryTheory.MorphismProperty.sSup_iff, csSup_inter_le, OrderIso.map_csSup, OrderIso.map_sSup, csSup_div, sSup_pair, CategoryTheory.Subfunctor.Subpresheaf.sSup_obj, lt_sSup_iff, AddSubsemigroup.mem_sSup_of_directed_on, AddSubsemigroup.coe_sSup_of_directed_on, Submodule.isOrtho_sSup_left, Ideal.map_sSup, isLUB_sSup, Subgroup.unop_sSup, csSup_add, Filter.limsSup_principal_eq_sSup, csSup_Iio, ConditionallyCompleteLinearOrderBot.csSup_empty, ConditionallyCompleteLattice.le_csSup, IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top, csInf_sub, SimpleGraph.isAcyclic_sSup_of_isAcyclic_directedOn, scottContinuous_iff_map_sSup, IsCompact.continuous_sSup, Con.sSup_def, CompleteSublattice.mem_sSup, TopologicalSpace.Opens.isBasis_iff_cover, sSup_add, CompleteLattice.IsCompactElement.directed_sSup_lt_of_lt, AddSubmonoid.mem_sSup_of_mem, Submonoid.mem_sSup_of_mem, Order.IsSuccPrelimit.sSup_Iio, le_sSup, Submodule.mem_sSup_iff_exists_finset, sInf_upperBounds_eq_csSup, sInf_upperBounds_eq_sSup, PrimitiveSpectrum.hull_sSup, csSup_Iic, Order.Frame.MinimalAxioms.inf_sSup_le_iSup_inf, Function.Periodic.integral_le_sSup_add_zsmul_of_pos, Monotone.csSup_image_le, Partition.sSup_eq, Subgroup.ofUnits_sSup, GaloisConnection.l_csSup_of_directedOn', EMetric.diam_eq_sSup, sSup_image2_eq_sInf_sSup, IsAddQuantale.add_sSup_distrib, sSup_range, csInf_image2_eq_csSup_csSup, le_csSup, Measurable.sSup, sSup_eq_of_forall_le_of_forall_lt_exists_gt, Ideal.homogeneousCore_eq_sSup, csSup_mem_closure, csSup_eq_univ_of_not_bddAbove, CompletePartialOrder.lubOfDirected, Filter.limsup_eq_sInf_sSup, csSup_image2_eq_csSup_csInf, Filter.HasBasis.limsSup_eq_iInf_sSup, isLUB_csSup, CompleteLattice.isAtomistic_iff, sSup_simples_eq_top_iff_isSemisimpleModule, Real.le_sSup_iff, sSup_iUnion_Iic, sSup_le_iff, Subsemiring.unop_sSup, sSup_image', Submodule.mem_sSup_of_directed, GaloisCoinsertion.u_sSup_l_image, WithBot.coe_sSup', ContinuousLinearMap.sSup_unitClosedBall_eq_norm, AddSubgroup.unop_sSup, ofDual_sSup, SimpleGraph.Subgraph.verts_sSup, Filter.ker_sSup, CompleteLattice.le_sSup, CompleteLattice.sSup_le, NonUnitalSubsemiring.coe_sSup_of_directedOn, setOf_isOpen_sSup, sSup_le, sSup_inter_le, isOrderRightAdjoint_sSup, Int.csSup_of_not_bdd_above, csInf_image2_eq_csInf_csSup, Real.sSup_of_not_bddAbove, compl_sInf', UpperSet.coe_sSup, csSup_le_csSup, LieAlgebra.InvariantForm.atomistic, IsCompact.exists_sSup_image_eq, IsGreatest.csSup_eq, ENat.sSup_eq_zero', GroupSeminorm.coe_sSup_apply, csSup_sub, Pi.Lex.sSup_apply, MeasureTheory.OuterMeasure.ofFunction_eq_sSup, Real.isLUB_sSup, MeasureTheory.Submartingale.exists_ae_trim_tendsto_of_bdd, lt_csSup_iff', IsAddQuantale.sSup_add_distrib, Subring.unop_sSup, Subgroup.op_sSup, NonarchAddGroupSeminorm.coe_sSup_apply', NonUnitalSubsemiring.mem_sSup_of_directedOn, AddGroupSeminorm.sSup_of_not_bddAbove, IsCompact.isGreatest_sSup, Hyperreal.st_eq_sSup, Subsemigroup.coe_sSup_of_directed_on, sSup_le_sSup, iSup_of_empty', sSup_inf_eq, AlgebraicGeometry.Scheme.IdealSheafData.support_sSup, sInf_le_sSup, Subsemigroup.unop_sSup, DirectedOn.le_sSup, IsPreconnected.mem_intervals, csSup_lowerBounds_range, Subsemigroup.op_sSup, csSup_image2_eq_csInf_csSup, Finset.sup_id_eq_sSup, Real.sSup_neg, sSup_zero, OrderIso.map_csSup_of_directedOn', Antitone.map_sInf_of_continuousAt, DirectedOn.isLUB_csSup, MonotoneOn.sSup_image_Icc, csSup_le, LeftOrdContinuous.map_sSup, ConvexOn.sSup_affine_eq, DirectedOn.disjoint_sSup_right, Submodule.mem_sSup, Set.Nonempty.eq_Icc_iff_nat, eq_sSup_atoms, isLUB_csSup', Monotone.sSup, CompleteDistribLattice.MinimalAxioms.inf_sSup_le_iSup_inf, csInf_inv, Real.sInf_def, totallyBounded_sSup, Order.IsNormal.map_sSup, sSupHom.map_sSup', sSup_apply, csSup_zero, NonarchAddGroupSeminorm.coe_sSup_apply, sInf_div, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sSup, ConvexOn.real_sSup_affine_eq, csSup_union, Int.csSup_empty, LowerSet.mem_sSup_iff, WithTop.isLUB_sSup', AddSubmonoid.mem_sSup_of_directedOn, sSup_add_distrib, Seminorm.sSup_apply, sSup_le_sSup_of_isCofinalFor, PiTensorProduct.injectiveSeminorm_def, AntitoneOn.sSup_image_Icc, IsCompact.exists_sSup_image_eq_and_ge, IsAtom.le_sSup, WithBot.sSup_eq, sSup_eq_iSup', sSup_mem_closure, ArchimedeanClass.stdPart_eq_sSup, Prod.snd_sSup, ScottContinuous.map_sSup, sSup_within_of_ordConnected, csSup_neg, Real.sSup_nonneg', csSup_Ico, csSup_eq_csSup_of_forall_exists_le, ciSup_neg, Filter.mem_sSup, himp_eq_sSup

(root)

Definitions

Name	Category	Theorems
InfSet 📖	CompData	—
SupSet 📖	CompData	—
iInf 📖	CompOp	1230 math math: continuousNeg_iInf, Submonoid.units_iInf, Subsemigroup.map_iInf_comap_of_surjective, ENNReal.nhds_zero, Nat.iInf_le_succ', ProbabilityTheory.bayesRisk_of_subsingleton, Pi.uniformSpace_eq, map_nhdsWithin, biInf_gt_eq_iInf, ENNReal.iInf_div_of_ne, MeasureTheory.OuterMeasure.map_iInf, LieAlgebra.IsKilling.iInf_ker_weight_eq_bot, Filter.nhds_atBot, iInf_inf, OrderIso.map_csInf, Filter.HasBasis.liminf_eq_ite, Real.iInf_Ioi_eq_iInf_rat_gt, LieModule.iInf_lowerCentralSeries_eq_posFittingComp, Real.iInf_nonpos', AlgebraicGeometry.Scheme.zeroLocus_iInf, GroupTopology.toTopologicalSpace_iInf, Submonoid.comap_iInf, equicontinuousWithinAt_iInf_dom, Antitone.iInf, Subsemiring.comap_iInf, le_mul_ciInf, Real.iInf_of_isEmpty, isSaddlePointOn_value, uniformity_dist_of_mem_uniformity, iSupIndep.injOn_iInf, iInf_sum, ContinuousMap.compactOpen_eq_iInf_induced, MeasureTheory.iInf_mul_le_lintegral, AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply_mk, ENNReal.add_sInf, Algebra.mem_iInf, Language.reverse_iInf, nhds_sInf, AddSubmonoid.neg_iInf, IsMinOn.iInf_eq, Set.map_finite_iInf, ProbabilityTheory.IsMeasurableRatCDF.iInf_rat_gt_eq, le_iInf₂_add, norm_eq_iInf_iff_real_inner_le_zero, TopologicalSpace.Closeds.iInf_def, LowerSet.compl_iInf, CompletelyDistribLattice.MinimalAxioms.iSup_iInf_eq, CategoryTheory.ObjectProperty.preservesLimitsOfShape_eq_iSup, topologicalGroup_iInf, Submonoid.op_iInf, Nucleus.himp_apply, Ideal.iInf_pow_smul_eq_bot_of_isLocalRing, IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot, LinearMap.ker_pi, AddSubgroup.centralizer_eq_iInf, Real.iInf_nonneg, ClosureOperator.ofCompletePred_apply, FormalMultilinearSeries.radius_pi_eq_iInf, Filter.mem_iInf, Finset.inf'_univ_eq_ciInf, map_iInf₂, RightOrdContinuous.map_sInf, ENat.iInf_mul_of_ne, ciInf_sub, iInf_iInf_eq_right, R1Space.iInf, Subsemiring.mem_iInf, upperSemicontinuousAt_biInf, Real.iInf_of_not_bddBelow, TwoSidedIdeal.mem_iInf, Filter.hasBasis_biInf_principal, nhds_iInf, Submonoid.unop_iInf, Antitone.le_map_iInf₂, LieModule.posFittingComp_le_iInf_lowerCentralSeries, add_ciInf, SimpleGraph.Subgraph.neighborSet_iInf, iInf_psigma', Filter.iInf_sets_eq, FirstOrder.Language.Substructure.map_iInf_comap_of_surjective, SeminormFamily.filter_eq_iInf, AddSubmonoid.addUnits_iInf₂, Filter.mem_iInf_finite, iInf_of_empty, WithZeroTopology.nhds_zero, iInf_unpair, Set.unit_eq, ProjectiveSpectrum.vanishingIdeal_iUnion, Filter.prod_iInf_left, iInf_sup_iInf, inf_eq_iInf, TopologicalSpace.eq_induced_by_maps_to_sierpinski, iInf_false, DividedPowers.SubDPIdeal.sInf_carrier_def, le_ciInf_add_ciInf, LowerSet.compl_iInf₂, ContinuousLinearMap.nhds_zero_eq_of_basis, iInf_eq_top, Antitone.iInf_nat_add, DividedPowers.isSubDPIdeal_iInf, TruncatedWittVector.iInf_ker_truncate, iInf_prod', le_ciInf_mul_ciInf, WithTop.iInf_empty, ENat.iInf_toNat, Ideal.quotientInfToPiQuotient_inj, GaloisConnection.u_ciInf, biInf_lt_eq_iInf, Interval.coe_iInf₂, AddSubsemigroup.unop_iInf, Filter.HasBasis.iInf, Filter.iInf.isCountablyGenerated, Ideal.iInf_pow_smul_eq_bot_of_le_jacobson, Filter.biInf_sets_eq, Submodule.mem_iInf, ENNReal.ofReal_iInf, le_iInf_const, ClosedSubmodule.mem_iInf, generateFrom_sUnion, UniformOnFun.uniformity_eq_of_basis, HomogeneousIdeal.toIdeal_iInf, Subalgebra.centralizer_coe_iSup, Subgroup.op_iInf, Directed.ciInf_mono, ProbabilityTheory.bayesRisk_of_subsingleton', ofDual_iInf, Ideal.quotientInfToPiQuotient_surj, Real.iInf_mul_of_nonneg, Set.Iic_iInf, ENNReal.iInf_ennreal, DirectedOn.le_ciInf_set_iff, Set.Iic_ciInf, sup_biInf_le_biInf_sup, Submodule.spanRank_toENat_eq_iInf_encard, Sublocale.coe_iInf, iInf_iSup_ge_nat_add, biInf_sigma, Ideal.iInf_mul, ciInf_add, Filter.iInf_principal_finset, AddSubsemigroup.comap_iInf, TwoSidedIdeal.iInf_ringCon, AEMeasurable.iInf, Nat.iInf_lt_succ', UniformFun.uniformSpace_eq_iInf_precomp_of_cover, Set.BijOn.iInf_comp, AddSubmonoid.addUnits_sInf, generateFrom_iUnion_isOpen, iInf_ulift, MeasureTheory.Measure.mkMetric_apply, ENNReal.mul_iInf, Filter.iInf_neBot_iff_of_directed', TopologicalSpace.Closeds.coe_iInf, MeasureTheory.Measure.iInf_IicSnd_gt, Subfield.map_iInf, iInf_iSup_of_antitone, Finite.ciInf_le, Subsemiring.map_iInf, inf_biInf, Set.iInf_eq_iInter, Filter.map_atBot_eq, MeasureTheory.lintegral_iInf_ae, ENNReal.inv_sSup, MeasurableSpace.measurableSet_iInf, IntermediateField.coe_iInf, ENNReal.nhds_top', MeasureTheory.OuterMeasure.comap_iInf, Submodule.inf_iInf, iInf_apply, sInf_sup_le_iInf_sup, iInf_ite, Filter.liminf_eq_iSup_iInf_of_nat', MeasureTheory.lintegral_iInf', Cardinal.lift_iInf, LinearMap.iInf_ker_proj, nhds_eq_order, Order.succ_eq_iInf, Subgroup.finiteIndex_iInf, Filter.HasBasis.biInf_mem, Filter.bliminf_eq_iSup_biInf_of_nat, AddCon.coe_iInf, iInf_eq_iInf_finset', OrderHom.iInf_apply, Concept.extent_iInf, AlgebraicGeometry.Scheme.zeroLocus_biInf, AddSubgroup.index_iInf_le, iInf_option, Pi.uniformSpace_comap_precomp, LinearGrowth.linearGrowthInf_biInf, Finsupp.iInf_ker_lapply_le_bot, upperSemicontinuous_biInf, LowerSet.Iic_iInf, Ideal.comap_iInf, UniformOnFun.nhds_eq_of_basis, inf_iInf_nat_succ, LinearMap.iInf_ker_proj_le_iSup_range_single, Filter.iInf_sets_eq_finite', NonUnitalStarAlgebra.iInf_toNonUnitalSubalgebra, biInf_le_eq_of_antitone, AddSubmonoid.comap_iInf, LinearMap.ker_smul', tendsto_atBot_ciInf, PiTensorProduct.projectiveSeminorm_apply, LieSubmodule.mem_iInf, ENNReal.le_iInf₂_add_iInf₂, NNReal.natCast_iInf, Submonoid.comap_iInf_map_of_injective, isGLB_ciInf, iSup_iInf_le_iInf_iSup, NonUnitalSubsemiring.mem_iInf, Submodule.annihilator_iSup, GaloisCoinsertion.u_iInf_l, Filter.iInf_isMeasurablyGenerated, essInf_eq_ciInf, Pi.induced_restrict, Submodule.iInf_colon_iSup, MeasureTheory.OuterMeasure.iInf_apply', Subring.comap_iInf, Set.Finite.ciInf_mem_image, iInf_range', Concept.intent_iInf, nhds_eq_iInf_abs_sub, ProbabilityTheory.bayesRisk_eq_iInf_measure_of_subsingleton, Algebra.coe_iInf, cauchy_iInf_uniformSpace', MeasureTheory.OuterMeasure.restrict_iInf, iInf₂_eq_top, MeasureTheory.OuterMeasure.le_sum_caratheodory, ENNReal.iInf_div, Ideal.ker_Pi_Quotient_mk, Finset.iInf_insert, ContinuousLinearMap.iInf_rayleigh_eq_iInf_rayleigh_sphere, Filter.hasBasis_biInf_of_directed, Filter.iInf_principal', Filter.HasBasis.limsup_eq_ite, CompleteSublattice.coe_iInf, NonUnitalSubsemiring.comap_iInf, Filter.countable_biInf_principal_eq_seq_iInf, Submodule.comap_iInf_map_of_injective, ENat.iInf_mul', IntermediateField.iInf_toSubfield, MeasureTheory.OuterMeasure.map_iInf_comap, Order.Coframe.MinimalAxioms.iInf_sup_eq, Pi.Lex.sInf_apply, WithTop.coe_iInf, nhdsWithin_pi_univ_eq, iSup_iInf_of_monotone, AddSubmonoid.unop_iInf, FilterBasis.eq_iInf_principal, EReal.nhds_top', biInf_le_eq_iInf, ContinuousLinearMap.iInf_ker_proj, fixingAddSubgroup_iUnion, iInf₂_le, ENNReal.iInf_sum, Filter.mem_biInf_of_directed, iInf_range, Finset.iInf_coe, Pi.uniformSpace_comap_restrict, Set.BijOn.iInf_congr, Submodule.norm_eq_iInf_iff_inner_eq_zero, OrderIso.map_ciInf_of_directed, LieSubmodule.iInf_coe, LinearMap.isCompl_iSup_ker_pow_iInf_range_pow, Set.Finite.iSup_biInf_of_antitone, Ideal.comap_sInf', uniformEquicontinuousOn_iInf_rng, Ideal.isRadical_iInf, Hausdorffification.instIsHausdorff, ciInf_of_not_bddBelow, Filter.mem_iInf_of_iInter, Subgroup.mem_iInf, Submodule.dualCoannihilator_iSup_eq, continuous_iInf_rng, iInf_valuationSubring_superset, Antitone.map_iSup₂_le, Pi.uniformSpace_comap_precomp', AddSubmonoid.addUnits_iInf, compl_sSup, ciInf_mul, biInf_le_eq_inf, biInf_congr', Language.sub_iSup, le_iInf, nhds_order_unbounded, CompleteSublattice.coe_sInf', Pi.ker_ringHom, ENat.iInf_coe_lt_top, LinearMap.iSup_range_single_eq_iInf_ker_proj, NonUnitalAlgebra.mem_iInf, map_nhds, ciInf_le_ciSup, exists_eq_ciInf_of_finite, le_iInf_add, ENat.iInf_mul, StieltjesFunction.iInf_rat_gt_eq, CompleteAtomicBooleanAlgebra.iInf_iSup_eq, Filter.eq_biInf_of_mem_iff_exists_mem, Set.Nontrivial.infsep_eq_iInf, AffineSubspace.mem_iInf_iff, IsHausdorff.iInf_pow_smul, PseudoMetricSpace.dist_ofPreNNDist, sInf_image, Ideal.iInf_sup_eq_top, Submodule.biInf_comap_proj, MvPowerSeries.le_order_subst, Real.iSup_mul_of_nonpos, nhdsLE_eq_iInf_principal, ciInf_le', uniformEquicontinuous_iInf_rng, iInf_option_elim, Order.Coframe.MinimalAxioms.sup_iInf_eq, ENNReal.iInf_add_iInf, AEMeasurable.biInf, MeasureTheory.OuterMeasure.trim_eq_iInf', biInf_lt_iff, Filter.lift_iInf_le, Real.iInf_const_zero, SimpleGraph.chromaticNumber_eq_iInf, iInf_subtype, ClosedSubmodule.coe_sInf, iInf_sup_of_monotone, upperSemicontinuousOn_iInf, Filter.mem_iInf_finite', ciInf_eq_univ_of_not_bddBelow, Subfield.mem_iInf, AlgebraicGeometry.IsLocalIso.eq_iInf, Set.Finite.iSup_biInf_of_monotone, Ideal.iInf_span_singleton_natCast, ContDiffMapSupportedIn.uniformSpace_eq_iInf, SimpleGraph.Subgraph.edgeSet_iInf, AddSubsemigroup.op_iInf, Filter.HasAntitoneBasis.iInf_principal, MeasureTheory.Content.outerMeasure_eq_iInf, NonUnitalSubsemiring.map_iInf, biInf_ge_eq_of_monotone, essInf_count, Submodule.iInf_coe, GaloisConnection.u_iInf, ciInf_mem, LocalSubring.eq_iInf_of_isIntegrallyClosedIn, ciInf_le_of_le, le_iInf_mul, Submodule.iSup_dualAnnihilator_le_iInf, equicontinuous_iInf_rng, Set.iSup_iInf_of_monotone, Submodule.comap_iInf, isGLB_biInf, iInf_const_mono, le_iInf_iff, ENNReal.iInf_mul_of_ne, nhdsGE_eq_iInf_principal, CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq', LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute, DirectedOn.isGLB_ciInf_set, iInf_sigma', iInf_iSup_eq, MeasureTheory.OuterMeasure.map_iInf_le, Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo, Prod.iInf_mk, nhdsSet_iInter_le, CompletelyDistribLattice.iInf_iSup_eq, WithTop.iInf_coe_eq_top, Ideal.Filtration.iInf_N, ENNReal.add_iInf, ciInf_eq_ite, Set.infsep_eq_iInf, Submodule.norm_eq_iInf_iff_real_inner_eq_zero, LowerSet.mem_iInf₂_iff, iInf_congr, iInf₂_le_of_le, Filter.prod_iInf_right, PrimeSpectrum.iInf_localization_eq_bot, iInf_Prop_eq, ENNReal.inv_iSup, ConvexCone.mem_iInf, AddSubgroup.quotientiInfEmbedding_apply_mk, TopCat.nonempty_isLimit_iff_eq_induced, MeasureTheory.OuterMeasure.iInf_apply, iInf_eq_iInf_subseq_of_monotone, NonUnitalStarAlgebra.mem_iInf, Set.Finite.iInf_biSup_of_antitone, SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf, SimpleGraph.Finsubgraph.coe_iInf, CompletePseudometrizable.iInf, AddSubmonoid.coe_iInf, NonUnitalSubring.coe_iInf, iInf_le_iff, lt_iInf_iff, iInf_eq_of_tendsto, Monotone.iInf_comp_eq, SimpleGraph.Subgraph.iInf_adj, upperSemicontinuous_ciInf, OrderIso.map_iInf, ClosedSubmodule.orthogonal_eq_inter, Subsemigroup.op_iInf, Finsupp.supported_iInter, nhdsSet_sInter_le, Subgroup.normalCore_eq_iInf_conjAct, TopologicalSpace.nhds_generateFrom, Set.einfsep_insert, Order.Coframe.MinimalAxioms.sup_iInf₂_eq, Filter.blimsup_eq_iInf_biSup, iInf_subtype'', AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty, iInf_subtype', TopologicalSpace.secondCountableTopology_iInf, cbiInf_eq_of_not_forall, LieSubmodule.iInf_toSubmodule, LocallyConvexSpace.iInf, Subgroup.normal_iInf_normal, MeasureTheory.OuterMeasure.biInf_apply, Nat.iInf_le_succ, Subgroup.index_iInf_le, Subsemiring.sInf_toAddSubmonoid, Subfield.coe_iInf, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp, ENNReal.iInf_add, ProbabilityTheory.bayesRisk_const_of_nonempty, GroupSeminorm.inf_apply, ENNReal.mul_iInf', GaloisInsertion.l_biInf_u, iInf_mono, MeasureTheory.measure_iInter_eq_iInf_measure_iInter_le, ciInf_subsingleton, generateFrom_iUnion, Subring.op_iInf, uniformEquicontinuousOn_iInf_dom, MeasureTheory.Filtration.rightCont_apply, iInf_ne_top_subtype, EMetric.infEdist_biUnion, Filter.HasBasis.eq_biInf, Filter.map_iInf_eq, CategoryTheory.Limits.CompleteLattice.limitCone_isLimit_lift, ENNReal.iInf_add_iInf_of_monotone, nhdsLE_eq_iInf_inf_principal, UpperSet.coe_iInf₂, Antitone.map_sSup_le, Antitone.le_map_iInf, sInf_apply, Filter.iInf_neBot_iff_of_directed, Set.einfsep_insert_le, LinearMap.mem_span_iff_continuous_of_finite, ENat.sub_iSup, ENat.iInf_eq_top_of_isEmpty, le_iInf_comp, Function.support_iInf, Cardinal.ord_eq_Inf, sInf_sUnion, Filter.isCountablyGenerated_seq, le_ciInf_iff', Finset.iInf_biUnion, ENat.iInf_coe_eq_top, Submonoid.units_sInf, AddSubsemigroup.mem_iInf, ProperCone.dual_iUnion, Directed.ciInf_le, untrop_sum, Real.mul_iInf_of_nonneg, Set.Icc.coe_iInf, sInf_image2, GaloisInsertion.l_iInf_u, ClosedSubmodule.toSubmodule_iInf, iInf_le_iInf₂, mul_ciInf, Ideal.IsHomogeneous.iInf, ClosedSubmodule.iInf_orthogonal, MvPowerSeries.le_weightedOrder_subst, ENat.exists_eq_iInf, LieModule.iInf_lcs_le_of_isNilpotent_quot, IsCompact.measure_eq_iInf_isOpen, Directed.le_ciInf_iff, ContinuousMap.nhds_compactOpen_eq_iInf_nhds_induced, Real.smul_iInf_of_nonpos, HomogeneousIdeal.toIdeal_sInf, UniformOnFun.topologicalSpace_eq, iInf_sigma, MeasureTheory.OuterMeasure.ofFunction_eq_iInf_mem, Filter.antitone_seq_of_seq, biInf_congr, Set.Iic_iInf₂, MeasureTheory.Filtration.rightCont_def, NonUnitalSubring.sInf_toSubsemigroup, AddSubgroup.center_eq_infi', Filter.tendsto_iInf_iInf, AffineSubspace.direction_iInf_of_mem, GaloisConnection.u_csInf, dimH_eq_iInf, UpperSet.mem_iInf_iff, continuousAdd_iInf, ENNReal.le_iInf_mul, regularSpace_iInf, iInf_eq_iInf_finset, equicontinuous_iInf_dom, Filter.mem_biInf_principal, SimpleGraph.iInf_adj, iInf_sup_iInf_le, Con.coe_iInf, Monotone.map_iInf_le, Monotone.measure_iInter, nhds_def, biSup_iInter_of_pairwise_disjoint, compl_iSup, AddSubsemigroup.map_iInf_comap_of_surjective, Filter.mem_iInf_finset, compl_iInf, AddSubmonoid.mem_iInf, InfClosed.biInf_mem_of_nonempty, IsIntegrallyClosed.iInf, ciInf_eq_of_forall_ge_of_forall_gt_exists_lt, Directed.ciInf_le_of_le, Real.iInf_mul_of_nonpos, Equiv.iInf_comp, InfClosed.iInf_mem_of_nonempty, biInf_prod, Interval.coe_iInf, Module.End.disjoint_iInf_maxGenEigenspace, biInf_finsetSigma, upperSemicontinuous_iInf, UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover, Submodule.coe_iInf, SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf, WithTop.iInf_coe_lt_top, ENat.coe_iInf, iInf_uniformity, nhds_eq_iInf_mabs_div, iInf_eq_of_forall_ge_of_forall_gt_exists_lt, ENNReal.nhds_of_ne_top, ENNReal.inv_iInf, Submodule.map_iInf, LowerSet.Iic_iInf₂, Finset.ciInf_mem_image, Ideal.comap_sInf, Subgroup.normalClosure_eq_iInf, ENat.mul_iInf_of_ne, EMetric.infEdist_iUnion, le_iInf₂_iff, Filter.hasBasis_iInf_principal_finite, Subgroup.quotientiInfSubgroupOfEmbedding_apply_mk, Filter.ker_iInf, UniformSpace.toTopologicalSpace_sInf, sInf_sup_eq, biInf_finsetSigma', ENNReal.toNNReal_iInf, Finset.iInf_finset_image, Subalgebra.unop_iInf, MeasureTheory.inducedOuterMeasure_eq_iInf, MeasureTheory.lintegral_iInf, MeasureTheory.le_iInf_lintegral, NonUnitalAlgebra.coe_iInf, Ideal.ker_tensorProductMk_quotient, Subgroup.coe_iInf, NNReal.le_iInf_mul_iInf, ENNReal.le_iInf_mul_iInf, sInf_eq_iInf, Monotone.ciInf_comp_tendsto_atBot, nhdsWithin_eq, Filter.HasBasis.liminf_eq_iSup_iInf, Algebra.iInf_toSubsemiring, sInf_iUnion_Ici, Subgroup.finiteIndex_iInf', RootPairing.iInf_ker_root'_eq, LowerSet.coe_iInf₂, PolynormableSpace.iInf, Antitone.map_iSup_le, Ideal.iSup_iInf_eq_top_iff_pairwise, Set.Iic.coe_iInf, PseudoMetricSpace.uniformity_dist, Subsemigroup.comap_iInf_map_of_injective, Filter.lift_iInf_of_map_univ, Filter.comap_iInf, Equiv.iInf_congr, LowerSet.coe_iInf, MeasureTheory.Filtration.rightCont_eq_of_not_isMax, ProbabilityTheory.bayesRisk_le_iInf, Manifold.riemannianEDist_def, iInf_bool_eq, ciInf_div, Submodule.sInf_orthogonal, OrderIso.map_csInf_of_directedOn, Filter.mem_iInf_of_mem, Ideal.iInf_span_singleton, OrderHom.coe_iInf, iInf_image, iInf_split, IsGLB.iInf_eq, Finset.ciInf_eq_min'_image, Set.Iic.coe_biInf, Submodule.pi_liftQ_eq_liftQ_pi, AlgebraicGeometry.Scheme.IdealSheafData.support_iSup, CategoryTheory.Subfunctor.Subpresheaf.iInf_obj, WithBot.coe_iInf, ofDual_iSup, Filter.lift'_iInf, le_iInf₂, StarSubalgebra.mem_iInf, AddSubgroup.quotientiInfEmbedding_apply, Subsemigroup.mem_iInf, equicontinuousOn_iInf_rng, Filter.liminf_eq_iSup_iInf_of_nat, Subfield.sInf_toSubring, inf_iInf, sup_iInf_le_iInf_sup, IsUltraUniformity.iInf, iInf_eq_of_forall_le_of_tendsto, RootPairing.iInf_ker_coroot'_eq, biInf_ge_eq_inf, EReal.add_iInf_le_iInf_add, iInf_psigma, Filter.countable_biInf_eq_iInf_seq', Filter.HasBasis.iInf', le_ciInf, nhds_top_order, isGLB_ciInf_set, sInf_eq_iInf', AffineSubspace.direction_iInf, Pi.induced_precomp, Set.indicator_iInter_apply, Filter.HasBasis.eq_iInf, Submodule.neg_iInf, Module.End.mem_iInf_maxGenEigenspace_iff, UniformSpace.toTopologicalSpace_iInf, NonUnitalSubsemiring.sInf_toAddSubmonoid, AddSubgroup.finiteIndex_iInf, Antitone.ciInf_comp_tendsto_atTop, Nat.iInf_lt_succ, RingCon.coe_iInf, Subalgebra.op_iInf, Filter.limsSup_eq_iInf_sSup, smul_iInf_le, Filter.eq_iInf_of_mem_iff_exists_mem, Finset.iInf_union, Subsemigroup.map_iInf, trop_iInf, BooleanSubalgebra.mem_iInf, CompleteSpace.iInf, Algebra.iInf_toSubmodule, ciInf_add_ciInf_le_ciInf_add, Submodule.spanRank_toENat_eq_iInf_finset_card, Filter.map_biInf_eq, IntermediateField.map_iInf, isSaddlePointOn_iff', Ideal.instIsTwoSidedIInf, Filter.isCountablyGenerated_biInf_principal, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, ENNReal.mul_iInf_of_ne, Subgroup.relIndex_iInf_le, Nucleus.sInf_apply, NonUnitalSubsemiring.coe_iInf, Finset.untrop_sum, ENat.coe_sInf, AddSubsemigroup.comap_iInf_map_of_injective, map_iInf, iInf₂_comm, ciInf_eq_bot_of_bot_mem, iInf₂_mono', Set.einfsep_eq_iInf, Finset.iInf_insert_update, ULift.down_iInf, Seminorm.inf_apply, Subgroup.quotientiInfEmbedding_apply_mk, iInf_top, NonUnitalAlgebra.map_iInf, isUniformAddGroup_iInf, Subring.sInf_toAddSubgroup, LowerSet.Iic_sInf, Directed.ciInf_le_ciSup, iInf_lt_iff, Subspace.dualAnnihilator_iInf_eq, ENNReal.iInf_mul_iInf, Prod.fst_iInf, NNReal.le_mul_iInf, Ideal.iInf_pow_eq_bot_of_isLocalRing, uniformity_edist, ExpGrowth.expGrowthInf_iInf, PointedCone.dual_iUnion, completelyRegularSpace_iInf, Subgroup.quotientiInfEmbedding_apply, continuousSMul_iInf, MeasureTheory.OuterMeasure.sInf_apply, IsTopologicalBasis.iInf, MeasureTheory.iInf_le_lintegral, Filter.lift'_iInf_of_map_univ, AddSubgroup.op_iInf, upperSemicontinuousOn_ciInf, Ideal.mem_iInf, Filter.map_atTop_eq, iSup₂_iInf₂_le_iInf₂_iSup₂, iInf_union, uniformEquicontinuous_iInf_dom, SubMulAction.mem_iInf, CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq, iInf₂_mono, NonUnitalStarAlgebra.coe_iInf, LieSubmodule.sInf_toSubmodule_eq_iInf, iInf_iSup_of_monotone, AddSubgroup.unop_iInf, DirectedOn.ciInf_set_le, ENNReal.iInf_ne_top, UpperSet.coe_iInf, iInf_dite, Submodule.annihilator_span, NNReal.iInf_real_pos_eq_iInf_nnreal_pos, fixingSubgroup_iUnion, Finset.iInf_singleton, GaloisConnection.u_csInf_of_directedOn, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf, ClosedSubmodule.coe_iInf, SubAddAction.mem_iInf, AddSubgroup.comap_iInf, StieltjesFunction.length_eq, ciInf_le, MeasureTheory.Filtration.rightCont_eq, MeasureTheory.measure_eq_iInf', List.iInf_mem_map_of_exists_le_sInf_empty, ENNReal.iInf_mul', MeasureTheory.lintegral_iInf_directed_of_measurable, Directed.ciInf_eq_of_forall_ge_of_forall_gt_exists_lt, Pi.induced_restrict_sUnion, Set.mulIndicator_iInter_apply, BooleanSubalgebra.coe_iInf, Metric.infEDist_iUnion, LinearGrowth.linearGrowthInf_iInf, Filter.iInf_neBot_of_directed, IsGLB.ciInf_set_eq, MeasureTheory.Measure.iInf_rat_gt_prod_Iic, MeasurableSpace.map_iInf, MeasureTheory.OuterMeasure.boundedBy_apply, Ideal.sup_iInf_eq_top, equicontinuousAt_iInf_dom, AddSubmonoid.map_iInf_comap_of_surjective, iInf₂_sup_eq, LinearMap.eventually_iInf_range_pow_eq, nhdsWithin_pi_eq, PrimeSpectrum.nilradical_eq_iInf, MeasureTheory.OuterMeasure.restrict_biInf, UniformSpace.Completion.uniformity_dist, ENat.mul_iInf, CompleteDistribLattice.MinimalAxioms.iInf_sup_le_sup_sInf, Ideal.mem_iInf_smul_pow_eq_bot_iff, Hausdorffification.lift_comp_of, Set.Finite.iInf_biSup_of_monotone, Module.annihilator_pi, ProbabilityTheory.bayesRisk_le_iInf', Filter.liminf_eq_iSup_iInf, nhds_def', iInf_and, Filter.hasBasis_biInf_principal', Filter.nhds_iInf, NNReal.nhds_zero, ExpGrowth.expGrowthInf_biInf, SeminormFamily.withSeminorms_iff_nhds_eq_iInf, iSup_iInf_le, iInf_unique, biInf_sup_le_biInf_sup, Metric.uniformity_edist, LinearMap.IsSymmetric.hasEigenvalue_iInf_of_finiteDimensional, ENNReal.sub_iSup, AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty, Antitone.measure_iInter, AffineSubspace.direction_sInf, Function.mulSupport_iInf, WithBot.coe_biInf, isUniformGroup_iInf, iInf_eq_dif, upperClosure_sUnion, ClosedSubmodule.sInf_orthogonal, InfClosed.biInf_mem, Filter.lift_iInf_of_directed, iInf_congr_Prop, ProbabilityTheory.bayesRisk_const_of_neZero, Filter.iInf_principal_finite, MeasureTheory.measure_eq_iInf, MeasureTheory.le_iInf₂_lintegral, upperSemicontinuousOn_biInf, Submodule.iInf_orthogonal, himp_iInf_eq, GaloisInsertion.l_biInf_of_ul_eq_self, disjointed_eq_inf_compl, ENNReal.le_iInf_add_iInf, Filter.generate_eq_biInf, induced_to_pi, UniformSpace.comap_iInf, iSupIndep.iInf, ENNReal.iInf_mul, iInf_extend_top, ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt, continuousMul_iInf, ENNReal.toReal_iInf, SimpleGraph.Subgraph.verts_iInf, BooleanSubalgebra.comap_iInf, IntermediateField.normal_iInf, AffineSubspace.direction_sInf_of_mem, AddSubgroup.coe_iInf, ENNReal.sInf_add, iInf_iInf_eq_left, tendsto_atTop_ciInf, EReal.nhds_bot', Sublocale.iInf_mem, ENNReal.iInf_coe_lt_top, ENNReal.cinfi_ne_top, sup_sInf_le_iInf_sup, Prod.swap_iInf, ContinuousLinearMap.nhds_zero_eq, TopCat.induced_of_isLimit, IsSelfAdjoint.hasEigenvector_of_isMinOn, ProbabilityTheory.bayesRisk_const, Nucleus.iInf_apply, TopologicalSpace.Closeds.iInf_mk, iSup_himp_eq, NNReal.coe_iInf, HomogeneousIdeal.toIdeal_iInf₂, iInf_iUnion, OrderIso.map_ciInf, iInf_and', biInf_sigma', Antitone.map_iSup_of_continuousAt, iInf_image2, Filter.countable_biInf_eq_iInf_seq, Filter.iInf_sets_eq_finite, iInf_univ, SimpleGraph.chromaticNumber_eq_biInf, continuous_iInf_dom, EReal.nhds_bot, Antitone.iInf_comp_tendsto_atTop, Submodule.map_iInf_comap_of_surjective, Ideal.radical_iInf_le, AddSubgroup.map_iInf, NonUnitalSubring.mem_iInf, biInf_sup_biInf, ciInf_unique, iInf_sup_eq, Filter.tendsto_iInf', MaximalSpectrum.iInf_localization_eq_bot, RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root', aeSeq.iInf, Filter.HasBasis.blimsup_eq_iInf_iSup, Ideal.iInf_pow_eq_bot_of_isDomain, RightOrdContinuous.map_iInf, ENNReal.iInf₂_add, Filter.smallSets_iInf, upperSemicontinuousWithinAt_biInf, iInf_comm, CategoryTheory.ObjectProperty.preservesColimitsOfShape_eq_iSup, SimpleGraph.iInf_adj_of_nonempty, Ideal.isCoprime_biInf, AddSubgroup.quotientiInfAddSubgroupOfEmbedding_apply, AddSubgroup.center_eq_iInf, Ideal.map_iInf_comap_of_surjective, Filter.limsup_eq_iInf_iSup, cbiInf_eq_of_forall, MeasureTheory.OuterMeasure.top_apply', EMetric.nhds_eq, Monotone.iInf_comp_tendsto_atBot, Ideal.quotientInfToPiQuotient_mk', Measurable.iInf, NonUnitalSubring.comap_iInf, Submodule.iInf_colon, fixingSubmonoid_iUnion, MeasureTheory.Measure.hausdorffMeasure_apply, AffineSubspace.comap_supr, ciInf_neg, InfClosed.iInf_mem, Subgroup.quotientiInfSubgroupOfEmbedding_apply, Directed.Iic_ciInf, Filter.hasBasis_iInf_of_directed, Submonoid.mem_iInf, inducing_iInf_to_pi, NonUnitalSubring.sInf_toAddSubgroup, Filter.iInf_le_liminf, iInf_or, ProbabilityTheory.bayesRisk_discard, Monotone.map_sInf_le, iInf_singleton, essInf_count_eq_ciInf, isSaddlePointOn_iff, FirstOrder.Language.Substructure.comap_iInf, Filter.atTop_finset_eq_iInf, biInf_inf, Hausdorffification.lift_of, Submodule.iInf_colon_iUnion, ENNReal.sub_iInf, Submonoid.units_iInf₂, le_iInf_iSup, OrderIso.map_iInf₂, Filter.mem_iInf_of_finite, Function.Surjective.iInf_comp, Ideal.quotientInfToPiQuotient_mk, Pi.uniformSpace_comap_restrict_sUnion, Filter.tendsto_iInf, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt, ciInf_lt_iff, Subfield.comap_iInf, Set.measure_eq_iInf_isOpen, tendsto_atTop_iInf, biInf_const, exists_norm_eq_iInf_of_complete_convex, AddSubgroup.normal_iInf_normal, equicontinuousOn_iInf_dom, Function.Surjective.iInf_congr, Module.End.iInf_maxGenEigenspace_restrict_map_subtype_eq, Subgroup.map_iInf, ciInf_mul_ciInf_le_ciInf_mul, MeasureTheory.OuterMeasure.sInf_apply', CategoryTheory.Subfunctor.iInf_obj, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def, biInf_prod', iInf_sup_le_iInf_sup, IsCompact.measure_eq_biInf_integral_hasCompactSupport, iInf_plift_down, biInf_mono, Finset.inf_eq_iInf, StieltjesFunction.iInf_Ioi_eq, Nat.iInf_of_empty, le_ciInf_mul, StarSubalgebra.coe_iInf, ciInf_set_le, Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo, LowerSet.compl_sInf, Dense.ciInf', ConvexCone.coe_iInf, iInf_of_isEmpty, Submonoid.map_iInf, Filter.limsup_eq_iInf_iSup_of_nat', Submodule.starProjection_minimal, Real.le_iInf, Filter.iInf_principal, essInf_eq_iInf, Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo, AddSubmonoid.comap_iInf_map_of_injective, UpperSet.compl_iInf, equicontinuousWithinAt_iInf_rng, ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux_def', Module.annihilator_dfinsupp, Subgroup.center_eq_infi', Subring.sInf_toSubmonoid, Real.smul_iSup_of_nonpos, NNReal.mul_iInf, sup_sInf_eq, upperSemicontinuousAt_ciInf, le_ciInf_set_iff, Subgroup.center_eq_iInf, Subgroup.comap_iInf, ciInf_le_of_le', Filter.lift_iInf, Ideal.mul_iInf, GaloisConnection.u_ciInf_set, NNReal.iInf_mul, iInf_prod, AddSubmonoid.map_iInf, Subring.mem_iInf, iSup_iInf_of_antitone, iInf_eq_bot, Submonoid.inv_iInf, NonUnitalSubsemiring.sInf_toSubsemigroup, Antitone.map_ciSup_of_continuousAt, fixedPoints.gfp_eq_sInf_iterate, LinearMap.iSup_range_single_le_iInf_ker_proj, Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf, essInf_cond_count_eq_ciInf, iInf_nat_gt_zero_eq, LinearMap.IsSymmetric.LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute, ciInf_mono, nhds_bot_order, OrderIso.map_ciInf_set_of_directedOn, NNReal.iInf_empty, iInf₂_eq_bot, Filter.liminf_top_eq_iInf, FirstOrder.Language.Substructure.mem_iInf, Filter.mem_iInf_of_directed, EReal.nhds_top, FirstOrder.Language.Substructure.comap_iInf_map_of_injective, BooleanSubalgebra.biInf_mem, MeasureTheory.OuterMeasure.sInfGen_def, Submonoid.coe_iInf, LieModule.eventually_iInf_lowerCentralSeries_eq, Subring.unop_iInf, CategoryTheory.Limits.CompleteLattice.limit_eq_iInf, isGLB_iInf, Filter.nhds_nhds, Directed.measure_iInter, Set.iSup_iInf_of_antitone, SimpleGraph.Subgraph.iInf_adj_of_nonempty, Pi.induced_precomp', OrderIso.map_sInf, ENat.mul_iInf', Subsemigroup.unop_iInf, biInf_le_biSup, RightOrdContinuous.map_ciInf, Sublattice.coe_iInf, continuousInv_iInf, Finset.exists_inf_eq_iInf, Directed.isGLB_ciInf, Filter.liminf_top_eq_ciInf, NNReal.le_iInf_add_iInf, AffineSubspace.coe_iInf, BooleanSubalgebra.iInf_mem, Submodule.restrictScalars_iInf, Set.iInf_iSup_of_monotone, Cardinal.iInf_eq_zero_iff, sInf_image', upperClosure_iUnion, Finset.inf_univ_eq_iInf, Finsupp.lsingle_range_le_ker_lapply, Filter.mem_iInf', Equiv.biInf_comp, Filter.blimsup_eq_iInf_biSup_of_nat, ENNReal.hasProd_iInf_prod, Pi.Colex.sInf_apply, Filter.HasBasis.limsSup_eq_iInf_sSup, ENNReal.nhds_top, iInf_eq_if, Measurable.biInf, Subsemiring.unop_iInf, ENat.iInf_eq_zero, GaloisConnection.u_iInf₂, CategoryTheory.Limits.CompleteLattice.limitCone_cone_π_app, ContinuousMap.nhds_compactOpen, iInf_le_of_le, Filter.limsup_eq_iInf_iSup_of_nat, Subsemiring.sInf_toSubmonoid, Subring.eq_iInf_of_isIntegrallyClosedIn, CompleteSublattice.mem_iInf, Submodule.orthogonal_eq_inter, Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_iSup_maxGenEigenspace_eq_top_of_commute, sup_iInf₂_eq, IsCoatom.iInf_le, Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree, ENNReal.biInf_le_nhds, iInf_plift_up, Measurable.iInf_Prop, Set.integer_eq, Filter.nhds_atTop, uniformContinuous_iInf_rng, iInf_ge_eq_iInf_nat_add, withSeminorms_iInf, OrderHom.sInf_apply, iInf_insert, ENNReal.add_iInf₂, ProbabilityTheory.iInf_rat_gt_defaultRatCDF, le_add_ciInf, AddSubmonoid.op_iInf, le_iInf₂_mul, upperSemicontinuousAt_iInf, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf, upperSemicontinuousWithinAt_iInf, Submodule.comap_smul', Real.mul_iSup_of_nonpos, UniformFun.iInf_eq, MeasureTheory.OuterMeasure.biInf_apply', UpperSet.compl_iInf₂, Metric.infDist_eq_iInf, OrderIso.map_ciInf_set, nhdsWithin_pi_eq', Submodule.dualAnnihilator_iSup_eq, ProperCone.innerDual_iUnion, iInf_neg, toDual_iInf, iInf_lt_top, AddGroupTopology.toTopologicalSpace_iInf, IsLocalization.ideal_eq_iInf_comap_map_away, LieModule.iInf_lowerCentralSeries_eq_bot_of_isNilpotent, Metric.uniformity_edist_aux, AddSubsemigroup.map_iInf, Monotone.map_iInf₂_le, Subsemiring.coe_iInf, Algebra.map_iInf, Filter.generate_iUnion, NNReal.agm_eq_ciInf, cauchy_iInf_uniformSpace, IsGLB.ciInf_eq, ENNReal.iInf_gt_eq_self, UpperSet.compl_sInf, Submodule.colon_iUnion, iInf_sup_of_antitone, Digraph.iInf_adj, MeasureTheory.Filtration.rightCont_eq_of_neBot_nhdsGT, ContinuousMap.uniformSpace_eq_iInf_precomp_of_cover, IntermediateField.iInf_toSubalgebra, Subring.map_iInf, AddSubgroup.finiteIndex_iInf', iSup_iInf_ge_nat_add, toDual_iSup, UniformConvergenceCLM.nhds_zero_eq, Set.einfsep_iUnion_mem_option, AddSubsemigroup.coe_iInf, SimpleGraph.Finsubgraph.coe_sInf, iInf_sUnion, AffineSubspace.direction_sInf_of_mem_sInf, Sublattice.comap_iInf, Finset.iInf_option_toFinset, ULift.up_iInf, MeasureTheory.OuterMeasure.trim_eq_iInf, PolishSpace.iInf, ENNReal.coe_iInf, FirstOrder.Language.Substructure.coe_iInf, UniformOnFun.nhds_eq, Filter.bliminf_eq_iSup_biInf, induced_iInf, StarSubalgebra.map_iInf, TopologicalSpace.Closeds.mem_iInf, TopCat.limit_topology, sup_iInf_eq, Submonoid.map_iInf_comap_of_surjective, iInf_exists, iInf_eq_iInf_subseq_of_antitone, ClosedSubmodule.toSubmodule_sInf, ENat.toENNReal_iInf, RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot', Filter.HasBasis.limsup_eq_iInf_iSup, Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors, sInf_range, PseudoEMetricSpace.uniformity_edist, Real.mul_iInf_of_nonpos, MeasureTheory.OuterMeasure.map_biInf_comap, iInf_le_iSup, AlgebraicGeometry.Scheme.IdealSheafData.support_sSup, iInf_emptyset, NNReal.le_iInf_mul, upperSemicontinuousWithinAt_ciInf, csSup_lowerBounds_range, Submodule.iInf_comap_proj, iInf_le, Nat.iInf_const_zero, le_ciInf_iff, TopCat.Presheaf.submonoidPresheafOfStalk_obj, nhdsGE_eq_iInf_inf_principal, tendsto_atBot_iInf, Filter.HasBasis.limsup_eq_ciInf_ciSup, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup, UpperSet.mem_iInf₂_iff, Filter.map_iInf_le, MeasureTheory.OuterMeasure.restrict_iInf_restrict, ENNReal.tprod_eq_iInf_prod, iInf_inf_eq, WithZeroTopology.nhds_eq_update, MeasureTheory.OuterMeasure.ofFunction_apply, iInf_pos, equicontinuousAt_iInf_rng, UniformOnFun.uniformity_eq, Filter.iInf_neBot_of_directed', uniformContinuous_iInf_dom, ciInf_Ici, ProbabilityTheory.bayesRisk_const', GaloisConnection.u_sInf, LieSubmodule.coe_iInf, Order.Coframe.MinimalAxioms.sup_sInf_eq, Submodule.exists_norm_eq_iInf_of_complete_subspace, Matrix.uniformity, AddSubgroup.relIndex_iInf_le, GaloisConnection.u_ciInf_of_directed, GaloisInsertion.l_iInf_of_ul_eq_self, PrimeSpectrum.vanishingIdeal_iUnion, StarSubalgebra.iInf_toSubalgebra, sdiff_iSup_eq, ENNReal.iInf_div', ciInf_pos, iInf_le_iInf_of_subset, iInf_const, Monotone.iInf, Ideal.IsHomogeneous.iInf₂, Filter.hasBasis_iInf_principal, Filter.HasBasis.liminf_eq_ciSup_ciInf, Prod.snd_iInf, Order.Coframe.MinimalAxioms.iInf_sup_le_sup_sInf, uniformity_pseudoedist, AddGroupSeminorm.inf_apply, Directed.le_ciInf, ciInf_const, iInf_pair, LinearMap.mem_span_iff_continuous, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sSup, ENNReal.iInf_coe_eq_top, UniformSpace.Completion.uniformity_dist', iInf_split_single, Subsemigroup.coe_iInf, topologicalAddGroup_iInf, Real.iInf_nonpos, Subring.coe_iInf, Set.map_finite_biInf, Dense.ciInf, Subgroup.unop_iInf, ENNReal.coe_sInf, AddSubgroup.mem_iInf, Set.Finite.lt_ciInf_iff, Subsemiring.op_iInf, iInf_mono', Antitone.ciInf_comp_tendsto_atTop_of_linearOrder, MeasureTheory.iInf_mul_le_setLIntegral, Monotone.ciInf_comp_tendsto_atBot_of_linearOrder, GaloisConnection.u_ciInf_set_of_directedOn, LinearMap.IsSymmetric.orthogonalFamily_iInf_eigenspaces, Order.Coframe.MinimalAxioms.sInf_sup_eq, Metric.infEDist_biUnion, Real.smul_iInf_of_nonneg, le_ciInf_add, iSup_iInf_eq, NonUnitalSubring.map_iInf, Filter.iInf_eq_generate, ProbabilityTheory.IsRatStieltjesPoint.iInf_rat_gt_eq, fixingAddSubmonoid_iUnion, MeasureTheory.OuterMeasure.iSup_sInfGen_nonempty, LowerSet.mem_iInf_iff, NonUnitalAlgebra.iInf_toSubmodule, NNReal.iInf_const_zero, iInf_true, WithTop.coe_sInf, SSet.Subcomplex.preimage_iInf, Filter.hasBasis_iInf_of_directed', Multiset.iInf_mem_map_of_exists_le_sInf_empty, biInf_ge_eq_iInf, Filter.hasBasis_biInf_of_directed', UniformConvergenceCLM.nhds_zero_eq_of_basis, Subgroup.centralizer_eq_iInf, Sublattice.mem_iInf, continuousVAdd_iInf, UniformOnFun.iInf_eq, IsTopologicalBasis.iInf_induced, biInf_le, UpperSet.iInf_Ici, NonUnitalStarAlgebra.map_iInf, Seminorm.uniformity_eq_of_hasBasis, SimpleGraph.radius_eq_iInf_iSup_edist, Module.End.injOn_iInf_maxGenEigenspace, Pi.uniformity, Set.iInf_iSup_of_antitone, Submodule.spanFinrank_eq_iInf, sInf_sup_sInf, CategoryTheory.Limits.CompleteLattice.limitCone_cone_pt, Subsemigroup.comap_iInf
iInf_delab 📖	CompOp	—
iSup 📖	CompOp	1534 math math: SimpleGraph.Finsubgraph.coe_sSup, BooleanSubalgebra.map_iSup, LowerSet.iSup_Iic, CategoryTheory.IsGrothendieckAbelian.subobjectMk_of_isColimit_eq_iSup, Ordinal.iSup_eq_iSup, Finset.iSup_biUnion, iSup_insert, Ordinal.iSup_eq_bsup, LieSubmodule.map_iSup, Order.Frame.MinimalAxioms.iSup_inf_eq, Order.IsNormal.apply_of_isSuccLimit, biSup_inf_le_inf_biSup, Ordinal.lift_card_iSup_le_sum_card, Acc.rank_eq, iSup_pair, Cardinal.mk_sUnion_le, Ordinal.iSup_pow_natCast, AddSubmonoid.smul_iSup, Module.rank_def, Filter.HasBasis.liminf_eq_ite, Subring.map_iSup, Nat.iSup_lt_succ', MeasureTheory.lintegral_def, Function.csSup_div_semiconj, List.iSup_mem_map_of_exists_sSup_empty_le, Ordinal.sup_eq_lsub_iff_lt_sup, HasCompactSupport.convolution_integrand_bound_left, ciSup_mul_le, isSaddlePointOn_value, BoundedContinuousFunction.dist_eq_iSup, Language.iSup_add, Measurable.biSup, EMetric.hausdorffEdist_iUnion_le, MulAction.IwasawaStructure.is_generator, iSup_eq_of_tendsto, biSup_le_eq_sup, AlgebraicGeometry.iSup_affineOpens_eq_top, Subalgebra.coe_iSup_of_directed, dimH_sUnion, GaloisCoinsertion.u_biSup_l, lowerSemicontinuous_ciSup, LowerSet.mem_iSup_iff, CompletelyDistribLattice.MinimalAxioms.iSup_iInf_eq, setOf_isOpen_iSup, isClosed_iSup_iff, NonUnitalSubsemiring.mem_iSup_of_directed, lowerSemicontinuousOn_biSup, MeasureTheory.lintegral_iSup', Cardinal.lift_iSup_le_lift_iSup, Language.iSup_sub, AddSubsemigroup.closure_iUnion, NonarchAddGroupSeminorm.coe_iSup_apply, TopologicalSpace.Opens.coe_iSup, ciSup_unique, TopCat.Presheaf.coveringOfPresieve.iSup_eq_of_mem_grothendieck, AddSubsemigroup.op_iSup, FirstOrder.Language.Substructure.mem_iSup_of_directed, iSup₂_le, NNReal.iSup_of_not_bddAbove, Ordinal.sup_eq_lsub_iff_succ, Matrix.iSup_eigenspace_toLin'_diagonal_eq_top, ClosureOperator.closure_iSup₂_closure, lowerSemicontinuousWithinAt_iSup, Filter.biSup_pure_eq_principal, NNReal.mul_iSup_le, iSup_psigma, GroupSeminorm.coe_iSup_apply, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₁_W, ENat.smul_sSup, iSup_bool_eq, MeasureTheory.setLIntegral_le_iSup_mul, ContinuousLinearMap.iSup_rayleigh_eq_iSup_rayleigh_sphere, Ordinal.iSup_typein_succ, AffineSpace.cobounded_eq_iSup_sphere_asymptoticNhds, LieSubmodule.iSup_toSubmodule, biSup_lt_eq_iSup, nhdsWithin_biUnion, ProbabilityTheory.condIndep_iSup_of_antitone, IntermediateField.isPurelyInseparable_iSup, AlgebraicGeometry.IsAffineOpen.iSup_of_disjoint, Metric.hausdorffEDist_def, fixedPoints_subgroup_iSup, iSup_split, SSet.iSup_subcomplexOfSimplex_prod_eq_top, Antitone.le_map_iInf₂, Monotone.iSup_comp_tendsto_atTop, Subsemigroup.unop_iSup, biSup_inf_le_biSup_inf, Real.iSup_nonneg', CategoryTheory.MorphismProperty.HasCardinalLT.iSup, AddMonoidHom.noncommPiCoprod_range, iSupIndep.disjoint_biSup, MeasureTheory.isTightMeasureSet_iff_inner_tendsto, Subgroup.normalCore_eq_iSup, ciSup_partialSups_eq', AddSubgroup.iSup_eq_closure, Cardinal.iSup_of_empty, SSet.finite_iSup_iff, Submodule.map₂_iSup_right, Subgroup.op_iSup, IsOpen.measure_eq_iSup_isClosed, Cardinal.iSup_lt_of_isRegular, Seminorm.closedBall_iSup, Metric.hausdorffEDist_iUnion_le, Subgroup.mem_biSup_of_directedOn, ENat.iSup_add_iSup_of_monotone, ENNReal.iSup_pow_of_ne_zero, ENat.iSup_zero, Submonoid.unop_iSup, iSup_false, ProbabilityTheory.Kernel.indep_iSup_directed_limsup, MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top, Subgroup.mem_iSup_of_mem, Set.indicator_iUnion_apply, ProbabilityTheory.indep_iSup_of_monotone, MeasureTheory.lintegral_iSup_ae, bot_lt_iSup, Directed.disjoint_iSup_right, IntermediateField.coe_iSup_of_directed, compl_sInf, Submodule.map_iSup, Submodule.mem_iSup_iff_exists_finsupp, LieModule.iSup_genWeightSpaceOf_eq_top, Set.iSup_mulIndicator, Submonoid.coe_iSup_of_directed, Directed.Ici_ciSup, Ordinal.sup_succ_le_lsub, ClosedSubmodule.coe_sSup, Dynamics.coverEntropy_iUnion_le, Ordinal.iSup_le_lsub, Ordinal.card_iSup_Iio_le_sum_card, sSup_inf_sSup, tendsto_atBot_ciSup, Finset.ciSup_eq_max'_image, MeasureTheory.OuterMeasure.coe_iSup, Cardinal.sum_le_mk_mul_iSup, iSup_unpair, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone, cbiSup_eq_of_not_forall, Dense.ciSup, MeasureTheory.lintegral_iSup_directed, Subalgebra.centralizer_coe_iSup, ciSup_add, Ideal.sup_primeHeight_eq_ringKrullDim, ofDual_iInf, Function.sSup_div_semiconj, ciSup_sub, ENNReal.iSup_add_iSup_le, CategoryTheory.Limits.CompleteLattice.colimit_eq_iSup, sup_iSup, WellFoundedGT.iSup_eq_monotonicSequenceLimit, LieModule.genWeightSpaceChain_def', iSup₂_mono, Directed.measure_iUnion, Encodable.iSup_decode₂, DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top, TwoSidedIdeal.iSup_ringCon, iSup_image, UpperSet.mem_iSup_iff, iInf_iSup_ge_nat_add, Language.mem_iSup, SupClosed.biSup_mem_of_nonempty, ProbabilityTheory.condIndep_iSup_of_monotone, Submodule.iSup_map_single_le, MeasureTheory.ae_restrict_biUnion_eq, LinearMap.iSup_range_single, UpperSet.compl_sSup, NNReal.coe_iSup, TopologicalSpace.Opens.iSup_mk, Filter.iSup_pure_eq_top, IsLUB.iSup_eq, AddSubmonoid.iSup_map_single, LinearMap.eventually_iSup_ker_pow_eq, Subfield.coe_iSup_of_directed, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one, LieModule.iSup_genWeightSpace_eq_top', MeasureTheory.Measure.mkMetric_apply, Filter.tendsto_iSup_iSup, Real.iSup_nonpos, Function.Surjective.iSup_comp, fixedPoints_addSubmonoid_iSup, MeasureTheory.biSup_measure_Iic, iInf_iSup_of_antitone, iSup₂_inf_eq, ciSup_eq_of_forall_le_of_forall_lt_exists_gt, isLUB_iSup, Submodule.smul_iSup', NonUnitalSubring.map_iSup, Language.reverse_iSup, IsUltrametricDist.invariantExtension_apply, Filter.liminf_eq_iSup_iInf_of_nat', SubMulAction.mem_iSup, nhdsSet_iUnion, SimpleGraph.Subgraph.neighborSet_iSup, nhdsWithin_sUnion, le_ciSup_of_le, EReal.iSup_add_le_add_iSup, iSup_partialSups_eq, Submodule.biSup_comap_subtype_eq_top, Filter.HasBasis.limsInf_eq_iSup_sInf, Subgroup.FG.biSup, AddSubsemigroup.coe_iSup_of_directed, Submodule.biSup_eq_range_dfinsupp_lsum, Algebra.adjoin_attach_biUnion, LieModule.iSup_ucs_le_genWeightSpace_zero, Set.mulIndicator_iUnion_apply, Filter.bliminf_eq_iSup_biInf_of_nat, MeasureTheory.SimpleFunc.iSup_coe_eapprox, Submonoid.iSup_eq_closure, Subgroup.map_iSup, Function.Surjective.iSup_congr, WithTop.coe_sSup, IsUltrametricDist.norm_tsum_le, MeasurableSet.measure_eq_iSup_isCompact_of_ne_top, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, OrderIso.map_csSup_of_directedOn, ExpGrowth.expGrowthSup_sum, lowerSemicontinuousOn_iSup, Submodule.fg_biSup, iSup_and', Order.IsSuccLimit.iSup_Iio, generateFrom_iInter_of_generateFrom_eq_self, ENat.mul_iSup, AddSubgroup.noncommPiCoprod_range, LinearMap.iInf_ker_proj_le_iSup_range_single, UpperSet.Ici_iSup, MeasureTheory.Measure.LebesgueDecomposition.iSup_succ_eq_sup, ciSup_mul, CategoryTheory.Subfunctor.Subpresheaf.iSup_obj, NNReal.iSup_eq_zero, Matroid.cRank_eq_iSup_cardinalMk_indep, Subring.coe_iSup_of_directed, MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE, Ordinal.iSup_le, Pi.Colex.sSup_apply, IntermediateField.finiteDimensional_iSup_of_finset, Filter.limsup_top_eq_ciSup, AffineSubspace.span_iUnion, SSet.iSup_skeleton, Subsemigroup.mem_iSup_prop, iSup_iInf_le_iInf_iSup, ciSup_le_iff, PrimeSpectrum.iSup_basicOpen_eq_top_iff, IsNormalClosure.adjoin_rootSet, Submodule.annihilator_iSup, Subfield.closure_iUnion, biSup_mono, ENNReal.iSup_ne_top, biSup_le_eq_iSup, TopCat.colimit_topology, IsUltrametricDist.norm_tprod_le, Submodule.neg_iSup, Ordinal.iSup_succ, iSup_subtype, Submonoid.mem_iSup, AddSubsemigroup.unop_iSup, egauge_univ_pi, tendsto_atTop_ciSup, ProbabilityTheory.indep_biSup_limsup, LowerSet.compl_iSup₂, biSup_symmDiff_biSup_le, Monoid.CoprodI.mrange_eq_iSup, AlgebraicGeometry.Scheme.Hom.image_iSup₂, Prod.fst_iSup, OrderIso.setIsotypicComponents_apply, ExpGrowth.expGrowthSup_biSup, MeasureTheory.eLpNormEssSup_eq_iSup, biSup_le_eq_of_monotone, isNoetherian_iSup, biSup_inf_biSup, OrderHom.sSup_apply, MeasureTheory.exists_isSigmaFiniteSet_measure_ge, Filter.HasBasis.limsup_eq_ite, ENat.biSup_add', AddSubgroup.coe_iSup_of_directed, iSup_exists, Ideal.iSup_eq_span, Submonoid.iSup_map_mulSingle_le, Finset.sup_univ_eq_ciSup, ENat.sum_iSup, iSup_inf_le_inf_iSup, AddSubsemigroup.map_iSup, normalClosure_eq_iSup_adjoin', ENNReal.biSup_add, MeasureTheory.measure_sigmaFiniteSetGE_le, Subsemiring.mem_iSup_of_directed, Filter.map_iSup, Subsemiring.coe_iSup_of_directed, le_iSup₂, ENNReal.sSup_div, Set.map_finite_iSup, Measurable.iSup, CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsISup, MeasurableSpace.generateFrom_iUnion_measurableSet, iSup_iInf_of_monotone, ProbabilityTheory.Kernel.indep_iSup_limsup, Ordinal.iSup_pow, Filter.mem_iSup, EMetric.diam_insert, Cardinal.lift_iSup, Order.Frame.MinimalAxioms.sSup_inf_eq, ContinuousMap.norm_eq_iSup_norm, ProbabilityTheory.indep_iSup_of_directed_le, Ordinal.deriv_limit, OrderIso.map_iSup, Finset.iSup_coe, ENNReal.csupr_ne_top, iSup_subtype', TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types, ENNReal.coe_sSup, Measurable.iSup_Prop, sSup_image2, AlgebraicGeometry.Scheme.Hom.preimage_iSup, NonUnitalSubsemiring.coe_iSup_of_directed, biSup_sigma', Finset.iSup_singleton, NumberField.mulHeight_eq, MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le, ENNReal.biSup_add_biSup_le, spectralNorm_eq_iSup_of_finiteDimensional_normal, biSup_finsetSigma', Dynamics.coverEntropyInf_eq_iSup_netEntropyInfEntourage, SupClosed.iSup_mem, le_ciSup_iff', GaloisCoinsertion.u_iSup_of_lu_eq_self, Submodule.iSup_mul, GaloisConnection.l_ciSup_set_of_directedOn, Submodule.localized'_iSup, isLUB_ciSup, LinearMap.isCompl_iSup_ker_pow_iInf_range_pow, Subgroup.mem_iSup_prop, HomogeneousIdeal.toIdeal_iSup₂, AddSubgroup.mem_iSup_of_directed, Set.Finite.iSup_biInf_of_antitone, Prod.iSup_mk, CategoryTheory.Subfunctor.isGeneratedBy_iff, iSup_mono', GaloisCoinsertion.u_biSup_of_lu_eq_self, MeasureTheory.Content.innerContent_iSup_nat, CategoryTheory.Subfunctor.Subpresheaf.isGeneratedBy_iff, LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional, AddSubsemigroup.mem_iSup, Submodule.dualCoannihilator_iSup_eq, iSup_plift_up, MeasureTheory.Measure.ae_sum_eq, Ordinal.iSup_add_nat, Cardinal.mk_biUnion_le_lift, ENNReal.iSup_coe_lt_top, Antitone.map_iSup₂_le, Submodule.span_attach_biUnion, OrderIso.map_ciSup, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top', MeasureTheory.lintegral_le_iSup_mul, Equiv.iSup_comp, Cardinal.lift_iSup_le, UpperSet.compl_iSup₂, Language.sub_iSup, Ordinal.iSup_sum, AddSubsemigroup.mem_biSup_of_directedOn, iSup_subtype'', Submodule.comap_iSup_map_of_injective, le_ciSup_set, Submodule.map₂_iSup_left, UpperSet.Ici_sSup, ProbabilityTheory.avgRisk_le_iSup_risk, ciSup_add_le, LinearMap.iSup_range_single_eq_iInf_ker_proj, sup_eq_iSup, ENNReal.iSup_natCast, ciInf_le_ciSup, DirectedOn.sSup_inf_eq, MeasureTheory.ae_restrict_iUnion_eq, iSup_plift_down, CompleteAtomicBooleanAlgebra.iInf_iSup_eq, Antitone.iSup_comp_tendsto_atBot, Subsemigroup.mem_iSup_of_directed, Real.iSup_mul_of_nonpos, ENat.add_iSup, NNReal.iSup_mul_iSup_le, IntermediateField.normal_iSup, sup_biSup, Subsemiring.op_iSup, Function.mulSupport_iSup, LieModule.coe_genWeightSpaceOf_zero, Antitone.map_ciInf_of_continuousAt, inf_iSup₂_eq, ciSup_add_ciSup_le, IsQuantale.sSup_mul_distrib, Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub, ENat.mul_sSup, Submodule.iSup_span, LowerSet.coe_iSup, MeasurableSet.measure_eq_iSup_isCompact, Ordinal.sup_succ_eq_lsub, IsSelfAdjoint.hasEigenvector_of_isMaxOn, Filter.iSup_ultrafilter_le_eq, Concept.intent_iSup, iSup_range, Set.Finite.iSup_biInf_of_monotone, CategoryTheory.Limits.CompleteLattice.colimitCocone_cocone_pt, Language.add_iSup, Equiv.biSup_comp, AddSubmonoid.FG.iSup, TopCat.Presheaf.SheafConditionEqualizerProducts.w, DirectedOn.ciSup_set_le_iff, FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion, Module.End.iSup_genEigenspace_eq, AddSubgroup.unop_iSup, AddSubmonoid.mul_iSup, LieAlgebra.cartan_sup_iSup_rootSpace_eq_top, ENNReal.smul_iSup, NonUnitalSubring.mem_iSup_of_directed, Order.krullDim_eq_iSup_coheight_of_nonempty, Real.iSup_pow, ENNReal.iSup_add, iSup_eq_top, Submodule.iSup_dualAnnihilator_le_iInf, Set.iSup_iInf_of_monotone, Subgroup.FG.biSup_finset, ENat.coe_sSup, MeasureTheory.measure_biUnion_eq_iSup, Monotone.le_map_iSup₂, Set.iSup_eq_iUnion, iSup_sdiff_eq, Filter.principal_bind, Ordinal.iSup_mul_nat, ClosedSubmodule.toSubmodule_iSup, Submodule.sum_mem_iSup, CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq', biSup_ge_eq_sup, CategoryTheory.Limits.CompleteLattice.colimitCocone_cocone_ι_app, ENNReal.tsum_iSup_eq, SimpleGraph.EdgeLabeling.iSup_labelGraph, Submodule.mem_iSup_iff_exists_dfinsupp, Monotone.le_map_iSup, LinearMap.IsSymmetric.iSup_iInf_eq_top_of_commute, Submonoid.map_iSup, Submodule.span_range_eq_iSup, Order.krullDim_eq_iSup_length, iInf_iSup_eq, disjoint_iSup_iff, Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim, Ideal.IsHomogeneous.iSup, Finset.Nonempty.ciSup_mem_image, CompletelyDistribLattice.iInf_iSup_eq, egauge_pi, AlgebraicGeometry.iSup_basicOpen_of_span_eq_top, iSup_comm, CategoryTheory.Pairwise.cocone_pt, Submodule.iSup_eq_range_dfinsupp_lsum, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_W, Set.Nonempty.ciSup_lt_iff, iSup_range', Monoid.CoprodI.range_eq_iSup, iSup_inf_le_sSup_inf, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, iSup_split_single, NNReal.agm_eq_ciSup, DFinsupp.iSup_range_lsingle, ENNReal.toNNReal_iSup, AddSubmonoid.iSup_map_single_le, Antitone.measure_iUnion, AddSubsemigroup.mem_iSup_of_mem, Submonoid.iSup_map_mulSingle, HomogeneousIdeal.toIdeal_sSup, iSup_nhds_le_uniformity, Filter.totallyBounded_iSup, ENNReal.tsum_eq_iSup_nat', ENNReal.inv_iSup, le_iSup, iSup_eq_iSup_finset, PiLp.dist_eq_iSup, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux, OrthogonalFamily.isInternal_iff, inf_sSup_eq, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, Set.Finite.iInf_biSup_of_antitone, IsMaxOn.iSup_eq, SequentialSpace.iSup, NonUnitalSubring.closure_sUnion, AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange, LinearGrowth.linearGrowthSup_biSup, AddQuantale.add_iSup_distrib, NumberField.isTotallyReal_iSup, Ordinal.sup_le_lsub, biSup_gt_eq_iSup, Ordinal.iSup_add_natCast, ENat.add_sSup, Filter.blimsup_eq_iInf_biSup, ENNReal.tsum_eq_iSup_sum, Sublattice.le_comap_iSup, CategoryTheory.ObjectProperty.isoClosure_iSup, Ordinal.IsNormal.map_iSup, iSup_eq_iSup_subseq_of_antitone, ciSup_le_iff', Order.coheight_eq_iSup_head_eq, Ordinal.card_iSup_Iio_le_card_mul_iSup, Algebra.iSup_toSubsemiring, GaloisConnection.l_csSup_of_directedOn, TopCat.Sheaf.existsUnique_gluing, Nat.iSup_of_not_bddAbove, Submodule.isOrtho_iSup_left, ENat.coe_iSup, ENat.smul_iSup, iSup_le_iSup_of_partialSups_le_partialSups, Subsemigroup.mem_biSup_of_directedOn, Finite.le_ciSup, GaloisConnection.l_sSup, LieSubmodule.span_iUnion, SupClosed.iSup_mem_of_nonempty, LinearMap.ker_noncommProd_eq_of_supIndep_ker, ProbabilityTheory.indep_iSup_limsup, Cardinal.mul_ciSup, AddSubmonoid.mem_bsupr_iff_exists_dfinsupp, ciSup_Iic, normalClosure_def, tsum_iSup_decode₂, LocallyFinite.nhdsWithin_iUnion, NNReal.iSup_pow_of_ne_zero, compactSpace_uniformity, Order.krullDim_eq_iSup_height_of_nonempty, MeasureTheory.iSup_lintegral_measurable_le_eq_lintegral, WithSeminorms.uniformEquicontinuous_iff_bddAbove_and_continuous_iSup, AddSubmonoid.unop_iSup, Submonoid.op_iSup, MeasureTheory.tendsto_measure_norm_gt_of_isTightMeasureSet, Multiset.iSup_mem_map_of_exists_sSup_empty_le, Ordinal.sup_eq_bsup, Dynamics.coverEntropy_biUnion_finset, iSup_pos, Antitone.le_map_iInf, Cardinal.ciSup_mul, ciSup_le', MeasurableSpace.measurableSpace_iSup_eq, Ordinal.Principal.iSup, ENat.sub_iSup, Set.pairwiseDisjoint_prod_left, ConvexOn.sSup_of_nat_affine_eq, Prod.swap_iSup, IsLUB.ciSup_set_eq, PrimeSpectrum.zeroLocus_iSup, ENNReal.biSup_add', Concept.extent_iSup, iSup_dite, Ideal.homogeneousHull_eq_iSup, AddSubmonoid.mem_iSup, WithTop.iSup_coe_lt_top, UpperSet.compl_iSup, iSup_eq_iSup_finset', iSup_inf_eq, Seminorm.iSup_apply, ENNReal.iSup_add_iSup, GaloisConnection.l_iSup₂, Submodule.smul_iSup, lowerSemicontinuous_iSup, CategoryTheory.Subfunctor.iSup_min, Subsemigroup.comap_iSup_map_of_injective, ENNReal.iSup_sub, ENNReal.tsum_eq_iSup_sum', AddSubgroup.ofAddUnits_sSup, AddGroupSeminorm.coe_iSup_apply, Directed.iSup_le, ClosedSubmodule.iInf_orthogonal, MeasureTheory.measure_sigmaFiniteSetWRT', AddMonoid.exponent_eq_iSup_addOrderOf, iSup₂_add_le, LowerAdjoint.closure_iSup₂_closure, ciSup_mem_iInter_Icc_of_antitone_Icc, NonUnitalSubsemiring.map_iSup, Real.smul_iInf_of_nonpos, Ordinal.opow_limit, Digraph.iSup_adj, mul_ciSup_le, Submodule.fg_iSup, Subgroup.iSup_comap_le, SSet.skeleton_succ, Real.iSup_const_zero, Cardinal.preAleph_limit, SSet.Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top, Order.height_eq_iSup_lt_height, CategoryTheory.MorphismProperty.iSup_iff, DirectedOn.isLUB_ciSup_set, MeasureTheory.OuterMeasure.map_iSup, Submodule.inf_iSup_genEigenspace, Filter.tendsto_iSup, Ideal.iSup_mul, continuous_iSup_dom, NormedSpace.equicontinuous_TFAE, Monotone.ciSup_mem_iInter_Icc_of_antitone, iSup_sup_eq, IsOpen.measure_eq_iSup_isCompact, PiLp.nnnorm_eq_ciSup, iSup_disjoint_iff, Cardinal.lift_iSup_le_sum, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot', MeasureTheory.OuterMeasure.restrict_iSup, biSup_iInter_of_pairwise_disjoint, compl_iSup, generateFrom_iInter, generateFrom_piiUnionInter_measurableSet, Dynamics.coverEntropy_iUnion_of_finite, le_iSup_inf_iSup, compl_iInf, ENNReal.iSup_ennreal, alexandrovDiscrete_iSup, partialSups_eq_biSup, CompleteLattice.ωScottContinuous.iSup, Real.iInf_mul_of_nonpos, NonUnitalSubalgebra.coe_iSup_of_directed, CategoryTheory.Pairwise.cocone_ι_app, AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom, CompleteSublattice.coe_sSup', tprod_iSup_decode₂, iSup_ite, ProbabilityTheory.condIndep_iSup_limsup, dimH_bUnion, Submonoid.mem_iSup_prop, ciInf_eq_top_of_top_mem, TopologicalSpace.Opens.mem_iSup, biSup_prod, Filter.eventually_iSup, Cardinal.sum_le_lift_mk_mul_iSup, Subsemiring.closure_iUnion, IsQuantale.mul_sSup_distrib, ENNReal.inv_iInf, Ordinal.bsup_eq_sup, iSup_option_elim, Height.mulHeight_eq, biSup_ge_eq_of_antitone, Submonoid.map_iSup_comap_of_surjective, inf_iSup_eq, ProbabilityTheory.Kernel.indep_iSup_of_directed_le, Subfield.closure_sUnion, AddSubmonoid.coe_iSup_of_directed, Multiset.iSup_mem_map_of_ne_zero, essSup_eq_iSup, csInf_upperBounds_range, PiTensorProduct.injectiveSeminorm_apply, Subsemiring.closure_sUnion, ciSup_or', Real.iSup_of_isEmpty, trdeg_eq_iSup_cardinalMk_isTranscendenceBasis, lowerSemicontinuousWithinAt_ciSup, ProbabilityTheory.Kernel.indep_iSup_of_monotone, Submonoid.comap_iSup_map_of_injective, Ordinal.iSup_mul_natCast, Ordinal.mem_closure_iff_iSup, Filter.HasBasis.liminf_eq_iSup_iInf, AddSubsemigroup.comap_iSup_map_of_injective, PiLp.norm_eq_ciSup, ciSup_eq_univ_of_not_bddAbove, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, NNReal.iSup_div, CategoryTheory.ObjectProperty.instEssentiallySmallISupOfSmall, Antitone.map_iSup_le, iSup_prod', Ideal.iSup_iInf_eq_top_iff_pairwise, MeasureTheory.measure_iUnion_of_tendsto_zero, Submodule.closure_coe_iSup_map_single, ENat.iSup_natCast, Ordinal.iSup_lt_ord_lift, TopCat.coinduced_of_isColimit, sSup_iUnion, ciSup_of_empty, Set.Ici_iSup₂, CategoryTheory.Subfunctor.IsGeneratedBy.iSup_eq, CategoryTheory.ObjectProperty.HasCardinalLT.iSup, EMetric.pair_reduction, MeasureTheory.tendsto_ae_condExp, Seminorm.coe_sSup_eq', ProbabilityTheory.indep_iSup_directed_limsup, IsCompact.prod_nhdsSet_eq_biSup, iSup_univ, iSup_eq_of_forall_le_of_tendsto, PiLp.edist_eq_iSup, iSup_eq_dif, AddMonoidHom.noncommPiCoprod_mrange, AddSubsemigroup.iSup_eq_closure, isOpen_iSup_iff, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone', Subgroup.coe_iSup_of_directed, IsOpen.measure_eq_biSup_integral_continuous, iSup_const_mono, iSup_image2, Submonoid.inv_iSup, LowerSet.mem_iSup₂_iff, LieModule.mem_posFittingComp, Real.iSup_pow_of_ne_zero, MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup, SupClosed.biSup_mem, iSup₂_disjoint_iff, SimpleGraph.Subgraph.edgeSet_iSup, SimpleGraph.Finsubgraph.coe_iSup, ProbabilityTheory.iSup_partitionFiltration_eq_generateFrom_range, Submodule.mul_iSup, LieSubmodule.mem_iSup_of_mem, AddGroupSeminorm.coe_sSup_apply, Order.krullDim_eq_iSup_coheight, Set.map_finite_biSup, ENNReal.add_iSup, AlgebraicGeometry.Scheme.IdealSheafData.support_iSup, iSup_ulift, OrderIso.map_ciSup', TopCat.Presheaf.presieveOfCovering.indexOfHom_spec, ENNReal.iSup_coe_eq_top, Subfield.mem_iSup_of_directed, ProbabilityTheory.condIndep_biSup_limsup, ofDual_iSup, GaloisConnection.l_ciSup_of_directed, GaloisConnection.l_iSup, iSup₂_mono', Directed.ciSup_mono, Directed.iSup_inf_eq, Submodule.iSup_eq_span, ENat.iSup_mul, Filter.liminf_eq_iSup_iInf_of_nat, iSup_inf_le_inf_sSup, lowerClosure_sUnion, ClosureOperator.closure_iSup_closure, Ordinal.mem_closure_tfae, Cardinal.iSup_lt_ord_lift_of_isRegular, IsLUB.ciSup_eq, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, Order.Frame.MinimalAxioms.inf_iSup₂_eq, fixedPoints_submonoid_iSup, Set.Icc.coe_iSup, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π, Submodule.span_iUnion, BoundedContinuousFunction.nndist_eq_iSup, ciSup_partialSups_eq, biSup_congr', DirectedOn.le_ciSup_set, aeSeq.iSup, MeasureTheory.OuterMeasure.sSup_apply, NNReal.natCast_iSup, Order.pred_eq_iSup, Filter.iSup_neBot, iSup_iUnion, Ideal.map_iSup_comap_of_surjective, AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom, SimpleGraph.ediam_eq_iSup_iSup_edist, Cardinal.iSup_lt_lift_of_isRegular, Ordinal.iSup'_eq_bsup, Dynamics.coverEntropyInf_eq_iSup_basis_netEntropyInfEntourage, iSup₂_eq_bot, Order.Frame.MinimalAxioms.inf_iSup_eq, Submodule.sum_mem_biSup, Matrix.ker_diagonal_toLin', IsAtom.le_iSup, Order.krullDim_eq_iSup_height, sup_iSup_nat_succ, AddSubmonoid.FG.biSup, FirstOrder.Language.Substructure.iSup_eq_closure, UniformOnFun.edist_def', Subsemigroup.op_iSup, MeasureTheory.tendsto_measure_sigmaFiniteSetGE, CompleteSublattice.coe_iSup, MeasurableSpace.comap_iSup, ClosedSubmodule.mem_iSup, Submonoid.mem_iSup_of_directed, AddSubgroup.FG.iSup, sSup_eq_iSup, hasCardinalLT_subtype_iSup, iSup_disjointed, ENat.sSup_add, Cardinal.beth_limit, Function.support_iSup, Module.End.genEigenspace_eq_iSup_genEigenspace_nat, AlgebraicGeometry.Scheme.Hom.image_iSup, Alexandrov.lowerCone_π_app, ENNReal.biSup_add_biSup_le', Cardinal.mk_biUnion_le, MeasureTheory.lintegral_iSup_directed_of_measurable, Finset.sup_eq_iSup, MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part, Subfield.map_iSup, AddSubgroup.ofAddUnits_iSup₂, IntermediateField.map_iSup, iSup_eq_iSup_of_partialSups_eq_partialSups, MeasureTheory.ae_restrict_biUnion_finset_eq, Order.Frame.MinimalAxioms.inf_sSup_eq, UpperSet.coe_iSup, UpperSet.mem_iSup₂_iff, WithBot.coe_iSup, isSaddlePointOn_iff', Ordinal.iSup_sequence_lt_omega_one, ProbabilityTheory.Kernel.indep_biSup_limsup, LowerSet.compl_iSup, ENNReal.mul_sSup, ENNReal.iSup_add_iSup_of_monotone, Language.iSup_mul, le_ciSup, MonoidHom.noncommPiCoprod_mrange, iSup_singleton, essSup_uniformOn_eq_ciSup, MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE', ENNReal.sSup_mul, iSup_eq_iSup_subseq_of_monotone, iSup_neg, TopologicalSpace.Opens.map_iSup, ENNReal.iSup_zero, add_sSup_distrib, Finset.iSup_insert, Submonoid.FG.iSup, Cardinal.sum_le_iSup_lift, IsWellFounded.rank_eq, SSet.horn_eq_iSup, Ordinal.iSup_typein_limit, ENat.iSup_eq_zero, Measurable.iSup', Subring.mem_iSup_of_directed, GaloisInsertion.l_biSup_u, MeasureTheory.tendsto_eLpNorm_condExp, Ordinal.iSup_lt_lift, AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj, MeasureTheory.lintegral_eq_nnreal, UniformFun.edist_def, Cardinal.mk_iUnion_le_lift, Directed.ciInf_le_ciSup, AddSubmonoid.op_iSup, SSet.range_eq_iSup_sigma_ι, Subspace.dualAnnihilator_iInf_eq, IntermediateField.isSplittingField_iSup, Submodule.iSup_map_single, MeasureTheory.SimpleFunc.lintegral_restrict_iUnion_of_directed, ENat.biSup_add_biSup_le', IsCompact.nhdsSet_prod_eq_biSup, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion, ProbabilityTheory.iSup_countableFiltration, Subsemigroup.closure_iUnion, LieModule.genWeightSpaceChain_def, ClosedSubmodule.toSubmodule_sSup, ProbabilityTheory.indep_iSup_of_antitone, Subsemigroup.mem_iSup_of_mem, FirstOrder.Language.Substructure.closure_iUnion, Ordinal.derivFamily_limit, mul_ciSup, BoundedContinuousFunction.nnnorm_eq_iSup_nnnorm, coinduced_iSup, Monoid.exponent_eq_iSup_orderOf, WithBot.ciSup_empty, AddSubsemigroup.map_iSup_comap_of_surjective, ciSup_pos, Partition.iSup_eq, ZFSet.rank_range, IntermediateField.iSup_eq_adjoin, iSup₂_iInf₂_le_iInf₂_iSup₂, Subsemiring.map_iSup, ENNReal.add_biSup', LinearMap.IsSymmetric.iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute, CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq, iSup_ne_bot_subtype, NonUnitalSubsemiring.closure_sUnion, Seminorm.continuous_iSup, Submodule.map_smul', Ordinal.iSup_ord, iInf_iSup_of_monotone, inf_sSup_eq_iSup_inf_sup_finset, ENNReal.hasSum, IntermediateField.iSup_toSubfield, ENat.iSup_add_iSup, lowerClosure_iUnion, tendsto_atTop_iSup, GaloisConnection.l_csSup, ENat.iSup_add, Seminorm.coe_sSup_eq, Ordinal.sup_eq_sup, Quantale.iSup_mul_distrib, NonUnitalSubsemiring.closure_iUnion, AddSubmonoid.mem_iSup_of_directed, TopologicalSpace.Opens.leSupr_apply_mk, LinearMap.range_smul', DirectSum.IsInternal.addSubmonoid_iSup_eq_top, ENNReal.add_sSup, Submodule.small_iSup, Finsupp.disjoint_lsingle_lsingle, Ordinal.le_iSup, iSup_emptyset, Directed.ciSup_eq_of_forall_le_of_forall_lt_exists_gt, essSup_count_eq_ciSup, Ordinal.iSup_eq_zero_iff, AddSubgroup.FG.biSup_finset, Real.iSup_mul_of_nonneg, FirstOrder.Language.Substructure.comap_iSup_map_of_injective, ProbabilityTheory.condIndep_biSup_compl, SimpleGraph.Subgraph.verts_iSup, isLUB_ciSup_set, ciSup_mul_ciSup_le, Order.IsNormal.map_iSup, Set.Iic.coe_iSup, iSupIndep_def, Module.End.genEigenspace_top, ENNReal.iSup_div, Directed.ciSup_le, tendsto_atBot_iSup, Set.Nonempty.ciSup_mem_image, MonoidHom.noncommPiCoprod_range, Monoid.CoprodI.iSup_mrange_of, Submodule.iSup_torsionBy_eq_torsionBy_prod, UniformOnFun.edist_def, IntermediateField.fg_iSup, iSup_congr_Prop, NonUnitalSubring.closure_iUnion, MeasureTheory.OuterMeasure.boundedBy_apply, CategoryTheory.Subfunctor.Subpresheaf.iSup_min, ProbabilityTheory.iSup_bayesRisk_le_minimaxRisk, SSet.hasDimensionLT_iSup_iff, Real.iSup_of_not_bddAbove, biSup_const, iSup_succ, Ordinal.sup_eq_bsup', Submodule.set_smul_eq_iSup, ProbabilityTheory.condIndep_iSup_directed_limsup, IntermediateField.adjoin_iUnion, iSup₂_comm, Ordinal.succ_iSup_eq_lsub_iff, ConvexOn.real_univ_sSup_of_nat_affine_eq, LieSubmodule.sSup_toSubmodule_eq_iSup, Monotone.iSup_comp_eq, AddSubgroup.closure_iUnion, Filter.comap_sSup, SimpleGraph.diam_def, ciSup_div, iSup_inf_le_iSup_inf, Subgroup.FG.iSup, ENat.sSup_mul, Cardinal.sum_le_lift_mk_mul_iSup_lift, ENat.iSup_coe_eq_top, ClosedSubmodule.mem_sSup, Set.Finite.iInf_biSup_of_monotone, LowerAdjoint.closure_iSup_closure, IntermediateField.normalClosure_def'', Filter.comap_iSup, SSet.iSup_skeletonOfMono, DividedPowers.isSubDPIdeal_iSup, Sublattice.map_iSup, le_iSup_of_le, LieAlgebra.IsKilling.biSup_corootSubmodule_eq_cartan, BoundedContinuousFunction.edist_eq_iSup, IsCompact.inf_nhdsSet_eq_biSup, Filter.liminf_eq_iSup_iInf, iSup_true, TopologicalSpace.Opens.iSup_def, sSup_mul_distrib, Ordinal.sup_eq_lsub, LinearGrowth.linearGrowthSup_iSup, Subgroup.unop_iSup, Dynamics.coverEntropy_eq_iSup_basis, iSup_iInf_le, nhdsSet_diagonal, Subgroup.mem_iSup_of_directed, Antitone.le_map_sInf, Set.iSup_indicator, 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, iSup₂_le_iff, ENNReal.sub_iSup, SSet.iSup_range_eq_top_of_isColimit, ContinuousMap.nnnorm_eq_iSup_nnnorm, CompleteSublattice.mem_iSup, Submodule.isOrtho_iSup_right, UpperSet.coe_iSup₂, partialSups_eq_ciSup_Iic, Algebra.isIntegral_iSup, iSup_Prop_eq, MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup, Filter.frequently_iSup, Ordinal.IsNormal.map_iSup_of_bddAbove, Real.iSup_le, AlgebraicGeometry.IsAffineOpen.biSup_of_disjoint, Cardinal.preBeth_limit, Submodule.iSup_smul, Submodule.mem_iSup_finset_iff_exists_sum, Subring.op_iSup, Dynamics.coverEntropy_eq_iSup_basis_netEntropyEntourage, AddMonoid.exponent_eq_iSup_addOrderOf', Submodule.iSup_eq_span', iSup_sup, LieModule.iSup_genWeightSpace_eq_top, 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, Subsemigroup.mem_iSup, NonUnitalStarSubalgebra.coe_iSup_of_directed, Subalgebra.op_iSup, AddSubgroup.mem_iSup_of_mem, AddSubmonoid.FG.biSup_finset, MeasureTheory.lintegral_iSup, OrthonormalBasis.norm_le_card_mul_iSup_norm_inner, Ordinal.lt_iSup_iff, iSup_sigma', Dynamics.coverEntropy_biUnion_le, Monotone.le_map_sSup, OrderIso.map_ciSup_set, ENNReal.iSup_eq_zero, Antitone.iSup, Ordinal.bsup'_eq_iSup, Ordinal.IsNormal.apply_omega0, SubAddAction.mem_iSup, MeasurableSet.measure_eq_iSup_isClosed_of_ne_top, TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology, Finset.iSup_insert_update, TopologicalSpace.IsOpenCover.iSup_eq_top, MeasureTheory.eLpNormEssSup_count, iSup_iSup_eq_right, GaloisConnection.l_ciSup, Ordinal.iSup_Iio_eq_bsup, iSup_himp_eq, WithTop.iSup_coe_eq_top, TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt, MeasureTheory.OuterMeasure.iUnion_of_tendsto_zero, iSup_unique, AEMeasurable.iSup, TopCat.Presheaf.SheafConditionEqualizerProducts.w_apply, ENNReal.smul_sSup, Submodule.map_iSup_comap_of_surjective, Antitone.map_iInf_of_continuousAt, GaloisCoinsertion.u_iSup_l, Submodule.coe_iSup_of_directed, IntermediateField.finiteDimensional_iSup_of_finite, Ordinal.iSup_eq_of_range_eq, ZFSet.rank_iUnion, ciSup_of_not_bddAbove, ENNReal.sSup_add, map_iSup, BooleanSubalgebra.biSup_mem, Dynamics.coverEntropy_eq_iSup_netEntropyEntourage, MeasureTheory.iSup₂_lintegral_le, Order.krullDim_eq_iSup_height_add_coheight_of_nonempty, Ordinal.iSup_sequence_lt_omega1, Filter.HasBasis.blimsup_eq_iInf_iSup, Set.exists_seq_iSup_eq_top_iff_countable, iSup_sigma, MeasureTheory.OuterMeasure.smul_iSup, Alexandrov.projSup_obj, ENNReal.tsum_eq_iSup_nat, Ordinal.bsup_eq_iSup, Algebra.mem_iSup_of_mem, essSup_count, sSup_image, iSup_le_iSup_of_subset, SimpleGraph.ediam_def, IntermediateField.isAlgebraic_iSup, normalClosure_eq_iSup_adjoin, Ordinal.lsub_le_succ_iSup, sSup_sUnion, LowerSet.compl_sSup, Cardinal.ciSup_mul_ciSup, ciSup_eq_ite, Submodule.mem_iSup_of_mem, AddSubmonoid.map_iSup, DirectedOn.inf_sSup_eq, biSup_prod', Filter.limsup_eq_iInf_iSup, AEMeasurable.biSup, Filter.limsup_le_iSup, AddSubsemigroup.mem_iSup_prop, Field.Emb.Cardinal.iSup_adjoin_eq_top, CategoryTheory.Subfunctor.image_iSup, CliffordAlgebra.iSup_ι_range_eq_top, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup, fixedPoints.lfp_eq_sSup_iterate, NNReal.iSup_empty, iSup_le, cbiSup_eq_of_forall, Ideal.mul_iSup, Set.Ici_ciSup, IntermediateField.toSubalgebra_iSup_of_directed, mul_sSup_distrib, IsUltrametricDist.nnnorm_tprod_le, biSup_sigma, MeasureTheory.Measure.hausdorffMeasure_apply, Alexandrov.lowerCone_pt, max_norm_root_eq_spectralValue, ProbabilityTheory.indep_biSup_compl, LieModule.iSup_ucs_eq_genWeightSpace_zero, AddSubgroup.mem_iSup_prop, IntermediateField.isSeparable_iSup, AddSubmonoid.mem_iSup_iff_exists_dfinsupp', Directed.inf_iSup_eq, ENNReal.iSup_pow, Ideal.sup_height_eq_ringKrullDim, Finset.iSup_finset_image, Dynamics.coverEntropyInf_iUnion_le, isSaddlePointOn_iff, Ordinal.mem_iff_iSup_of_isClosed, NNReal.mul_iSup, EMetric.hausdorffEdist_def, ENNReal.sub_iInf, AddSubgroup.FG.biSup, Cardinal.add_ciSup, le_iInf_iSup, OrderIso.map_csSup, OrderIso.map_sSup, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces, Algebra.adjoin_iUnion, LieSubmodule.iSup_toSubmodule_eq_top, TopCat.nonempty_isColimit_iff_eq_coinduced, Set.BijOn.iSup_congr, AddSubgroup.op_iSup, ENNReal.iSup_lt_eq_self, Ideal.map_sSup, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens, ENNReal.finsetSum_iSup_of_monotone, ProjectiveSpectrum.zeroLocus_iSup_homogeneousIdeal, Finsupp.supported_iUnion, exists_eq_ciSup_of_finite, Antitone.ciSup_comp_tendsto_atBot, MeasureTheory.SimpleFunc.iSup_eapprox_apply, Language.mul_iSup, Submodule.restrictScalars_iSup, Submonoid.mem_biSup_of_directedOn, SSet.boundary_eq_iSup, ENat.toENNReal_iSup, AddSubmonoid.mem_iSup_iff_exists_dfinsupp, Ordinal.isClosed_iff_iSup, Ordinal.bsup_eq_sup', Filter.limsup_eq_iInf_iSup_of_nat', fixedPoints_addSubgroup_iSup, iSup_eq_if, Real.smul_iSup_of_nonneg, ciSup_subsingleton, Directed.le_iSup, Subsemigroup.map_iSup, HomogeneousIdeal.irrelevant_eq_iSup, Set.Iic.coe_biSup, Subsemigroup.map_iSup_comap_of_surjective, ULift.up_iSup, ciSup_mul_le_ciSup_mul_ciSup, Subsemigroup.coe_iSup_of_directed, OrderIso.map_ciSup_of_directed, Subgroup.ofUnits_iSup₂, MeasureTheory.OuterMeasure.mkMetric'.eq_iSup_nat, Real.smul_iSup_of_nonpos, WellFoundedGT.ciSup_eq_monotonicSequenceLimit, dimH_iUnion, SimpleGraph.Subgraph.iSup_adj, Monotone.measure_iUnion, AddSubmonoid.closure_iUnion, iSup_psigma', LieAlgebra.IsKilling.coe_invtSubmoduleToLieIdeal_eq_iSup, Directed.disjoint_iSup_left, DirectSum.IsInternal.submodule_iSup_eq_top, Submodule.mem_iSup_of_chain, MeasurableSpace.iSup_generateFrom, Dynamics.coverEntropyInf_biUnion_le, Submodule.mem_iSup_iff_exists_finset, MeasureTheory.tendsto_measure_compl_closedBall_of_isTightMeasureSet, Cardinal.lift_iSup_le_lift_iSup', AlgebraicGeometry.Scheme.IsLocallyDirected.exists_of_pullback_V_V, FirstOrder.Language.DirectLimit.Equiv_isup_of_apply, iSup_iInf_of_antitone, OrderIso.map_ciSup_set_of_directedOn, Submodule.localized₀_iSup, LowerSet.coe_iSup₂, Ordinal.sup_typein_limit, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, Submodule.iSup_eq_toSubmodule_range, LinearMap.iSup_range_single_le_iInf_ker_proj, Set.BijOn.iSup_comp, IsCompact.nhdsSet_inf_eq_biSup, Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf, ProbabilityTheory.condIndep_iSup_of_disjoint, Submodule.mem_sSup_iff_exists_finset, LinearMap.disjoint_single_single, List.iSup_mem_map_of_ne_nil, ENNReal.iSup_mul_le, ENat.add_biSup, ciSup_false, lt_biSup_iff, iSup_le_iff, AddSubsemigroup.mem_iSup_of_directed, LieSubalgebra.span_iUnion, ProbabilityTheory.iSup_partitionFiltration, Order.Frame.MinimalAxioms.inf_sSup_le_iSup_inf, Set.iSup_iInf_of_antitone, Subring.unop_iSup, GaloisConnection.l_ciSup_set, iSup_nat_gt_zero_eq, ciSup_set_le_iff, biInf_le_biSup, ULift.down_iSup, iSup_add_le, Subgroup.ofUnits_sSup, Cardinal.sum_le_iSup, CategoryTheory.Subfunctor.iSup_obj, IsAddQuantale.add_sSup_distrib, NonUnitalSubring.coe_iSup_of_directed, sSup_range, ENat.sum_iSup_of_monotone, Prod.snd_iSup, Module.End.iSup_maxGenEigenspace_eq_top, Nat.iSup_lt_succ, Submonoid.mem_iSup_of_mem, SSet.Subcomplex.Pairing.rank'_eq, MeasureTheory.isTightMeasureSet_iff_tendsto_measure_norm_gt, Ordinal.sup_eq_lsub_or_sup_succ_eq_lsub, Set.iInf_iSup_of_monotone, OrderIso.map_iSup₂, ClosedSubmodule.coe_iSup, iSup_option, Submodule.finite_iSup, Finsupp.lsingle_range_le_ker_lapply, MeasureTheory.measure_iUnion_eq_iSup_accumulate, OrderHom.iSup_apply, lowerSemicontinuousAt_iSup, FirstOrder.Language.DirectLimit.iSup_range_of_eq_top, MeasureTheory.SimpleFunc.iSup_approx_apply, Cardinal.lift_iSup_le_iff, AddSubgroup.iSup_comap_le, SimpleGraph.iSup_adj, Filter.blimsup_eq_iInf_biSup_of_nat, SSet.Subcomplex.preimage_iSup, iSup_const_le, lt_ciSup_iff, iSup_ge_eq_iSup_nat_add, Submonoid.closure_iUnion, sSup_iUnion_Iic, Metric.ediam_iUnion_mem_option, iSup_const, WithTop.coe_iSup, WithBot.coe_biSup, Monotone.ciSup_comp_tendsto_atTop, transfiniteIterate_limit, lp.norm_eq_ciSup, Matrix.range_diagonal, Filter.totallyBounded_biSup, Filter.limsup_eq_iInf_iSup_of_nat, sSup_image', le_iSup₂_of_le, RestrictedProduct.topologicalSpace_eq_iSup, Set.Finite.ciSup_mem_image, iSup_symmDiff_iSup_le, Quantale.mul_iSup_distrib, Order.coheight_eq, PrimitiveSpectrum.hull_iSup, Polynomial.supNorm_eq_iSup, Field.Emb.Cardinal.iSup_filtration, iSup_inf_of_monotone, Subgroup.closure_iUnion, Cardinal.aleph_limit, Finset.sup_univ_eq_iSup, bsupr_limsup_dimH, iSup_congr, isLUB_biSup, Subsemigroup.iSup_eq_closure, ciSup_const, lowerSemicontinuousOn_ciSup, MeasureTheory.iSup_lintegral_le, add_ciSup, Seminorm.coe_iSup_eq, Directed.ciSup_le_iff, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top, ProjectiveSpectrum.zeroLocus_iSup_ideal, Real.mul_iSup_of_nonpos, Finset.Nonempty.ciSup_eq_max'_image, le_iSup_iff, Ordinal.iSup_le_iff, Cardinal.iSup_lt_ord_of_isRegular, le_biSup, Ordinal.iSup_eq_lsub, iSup_of_empty, Submodule.dualAnnihilator_iSup_eq, Finset.iSup_option_toFinset, biSup_sup, toDual_iInf, Matrix.iSup_eigenspace_toLin_diagonal_eq_top, AddSubmonoid.mem_iSup_of_mem, MeasureTheory.OuterMeasure.iSup_apply, SSet.N.iSup_subcomplex_eq_top, ENNReal.iSup_mul, Ordinal.iSup_eq_lsub_iff, map_iSup₂, Topology.IsGeneratedBy.iSup, Submonoid.FG.biSup_finset, lowerSemicontinuousWithinAt_biSup, Submodule.mem_biSup_iff_exists_dfinsupp, GroupSeminorm.coe_sSup_apply, Cardinal.ciSup_add_ciSup, isSemisimpleModule_biSup_of_isSemisimpleModule_submodule, isArtinian_iSup, ENNReal.finsetSum_iSup, AddSubmonoid.map_iSup_comap_of_surjective, TopCat.Sheaf.eq_of_locally_eq_iff, Pi.Lex.sSup_apply, Ordinal.iSup_natCast, LinearMap.mapsTo_biSup_of_mapsTo, lowerSemicontinuousAt_biSup, iSup₂_le_iSup, Submodule.topologicalClosure_iSup_map_single, iSup_eq_bot, FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply, Filter.limsInf_eq_iSup_sInf, Directed.le_ciSup_of_le, CategoryTheory.Subfunctor.Subpresheaf.image_iSup, iSup_iInf_ge_nat_add, Ordinal.iSup_iterate_eq_nfp, ENat.biSup_add_biSup_le, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing, IsAddQuantale.sSup_add_distrib, ProbabilityTheory.condIndep_iSup_of_directed_le, ciSup_add_le_ciSup_add_ciSup, DirectSum.isInternal_biSup_submodule_of_iSupIndep, toDual_iSup, iSup₂_mul_le, LeftOrdContinuous.map_ciSup, Set.chainHeight_eq_iSup, AddSubmonoid.neg_iSup, AddSubmonoid.comap_iSup_map_of_injective, CategoryTheory.Limits.CompleteLattice.colimitCocone_isColimit_desc, Subgroup.ofUnits_iSup, LinearMap.IsSymmetric.iSup_eigenspace_inf_eigenspace_of_commute, ConvexOn.real_sSup_of_nat_affine_eq, biSup_congr, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux_assoc, ContinuousMap.enorm_eq_iSup_enorm, BoundedContinuousFunction.norm_eq_iSup_norm, ENNReal.inv_sInf, BooleanSubalgebra.iSup_mem, FirstOrder.Language.Substructure.map_iSup, Ordinal.apply_omega0_of_isNormal, IntermediateField.Lifts.carrier_union, PairReduction.iSup_edist_pairSet, Nat.iSup_le_succ', Filter.bliminf_eq_iSup_biInf, GaloisInsertion.l_iSup_u, IntermediateField.normalClosure_def', PrimeSpectrum.iSup_basicOpen_eq_top_iff', SimpleGraph.Subgraph.IsMatching.iSup, CompleteLattice.MulticoequalizerDiagram.iSup_eq, MeasureTheory.isTightMeasureSet_iff_tendsto_measure_compl_closedBall, iSup_apply, ENat.iSup_add_iSup_le, UniformFun.dist_def, MeasureTheory.OuterMeasure.comap_iSup, Ideal.toIdeal_homogeneousHull_eq_iSup, iSup_comp_le, Submodule.mem_iSup_iff_exists_dfinsupp', Order.height_eq_iSup_last_eq, AddSubmonoid.mem_biSup_of_directedOn, BoundedContinuousFunction.enorm_eq_iSup_enorm, Filter.HasBasis.limsup_eq_iInf_iSup, ExpGrowth.expGrowthSup_iSup, iSup_of_empty', sSup_inf_eq, Monotone.iSup, ProbabilityTheory.Kernel.indep_biSup_compl, Real.mul_iInf_of_nonpos, iInf_le_iSup, dimH_def, AddSubgroup.map_iSup, AddSubmonoid.iSup_mul, Filter.ker_iSup, ciSup_mono', Language.kstar_eq_iSup_pow, Finset.sup'_univ_eq_ciSup, Order.coheight_eq_iSup_gt_coheight, ciSup_le, NNReal.iSup_mul, AddSubgroup.ofAddUnits_iSup, MeasureTheory.OuterMeasure.trim_iSup, Filter.HasBasis.limsup_eq_ciInf_ciSup, Submodule.mem_iSup_of_directed, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup, iSup₂_eq_top, Ordinal.lsub_le_sup_succ, iSup_mul_le, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.iSup_P, Finset.exists_sup_eq_iSup, Ideal.mem_iSup_of_mem, AffineSubspace.map_iSup, Set.Ici_iSup, MeasureTheory.AECover.iSup_lintegral_eq_of_countably_generated, iSup_union, Ideal.IsHomogeneous.iSup₂, Ideal.Filtration.iSup_N, Submodule.iSup_toAddSubmonoid, biSup_inter_of_pairwise_disjoint, Order.IsSuccPrelimit.iSup_Iio, Dense.ciSup', iSup_extend_bot, NNReal.iSup_pow, Ordinal.succ_iSup_le_lsub_iff, essSup_eq_ciSup, Finset.ciSup_mem_image, OrderHom.coe_iSup, iSup_bot, Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits, LeftOrdContinuous.map_sSup, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_W, MeasureTheory.setLIntegral_iUnion_of_directed, MeasureTheory.lintegral_eq_iSup_eapprox_lintegral, Subsemiring.unop_iSup, ENNReal.coe_iSup, CategoryTheory.ObjectProperty.instSmallISupOfSmall, lt_ciSup_iff', Subgroup.iSup_eq_closure, iSup_inf_of_antitone, Equiv.iSup_congr, Ordinal.IsNormal.apply_of_isSuccLimit, sdiff_iSup_eq, CompleteDistribLattice.MinimalAxioms.inf_sSup_le_iSup_inf, ProbabilityTheory.indep_iSup_of_disjoint, Ordinal.iSup_lt_ord, AddQuantale.iSup_add_distrib, FirstOrder.Language.DirectLimit.cod_partialEquivLimit, Ideal.map_iSup, Monoid.exponent_eq_iSup_orderOf', Directed.le_ciSup, FirstOrder.Language.DirectLimit.range_lift, Dynamics.coverEntropyInf_eq_iSup_basis, Monotone.iSup_nat_add, HomogeneousIdeal.toIdeal_iSup, sSup_apply, IntermediateField.finiteDimensional_iSup_of_finset', iSup_sum, ENat.add_biSup', lowerSemicontinuousAt_ciSup, Filter.HasBasis.liminf_eq_ciSup_ciInf, CategoryTheory.Subfunctor.Subpresheaf.IsGeneratedBy.iSup_eq, ProbabilityTheory.Kernel.indep_iSup_of_disjoint, NonarchAddGroupSeminorm.coe_sSup_apply, iSup_sUnion, Filter.iSup_sets_eq, Filter.iSup_principal, HasCompactSupport.convolution_integrand_bound_right, BooleanSubalgebra.le_comap_iSup, SSet.Subcomplex.image_iSup, ENat.biSup_add, disjoint_iSup₂_iff, ENNReal.iSup₂_pow_of_ne_zero, Real.iSup_nonneg, Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin, Set.Finite.ciSup_lt_iff, nhdsWithin_iUnion, Cardinal.mk_iUnion_le, add_ciSup_le, Cardinal.iSup_le_sum, HasCompactSupport.convolution_integrand_bound_right_of_subset, Projectivization.Subspace.span_iUnion, Filter.hasBasis_iSup, measurableSet_iSup_of_mem_piiUnionInter, Subgroup.noncommPiCoprod_range, SimpleGraph.eccent_def, Cardinal.iSup_mk_le_mk_iUnion, iSup_limsup_dimH, DeltaGeneratedSpace.iSup, ZFSet.iSup_card_le_card_iUnion, Ordinal.card_iSup_le_sum_card, DirectSum.range_coeLinearMap, Alexandrov.projSup_map, biSup_ge_eq_iSup, TopCat.Presheaf.SheafConditionEqualizerProducts.res_π_apply, Cardinal.ciSup_add, iSup_or, Ordinal.iSup_lt, ConvexOn.univ_sSup_of_nat_affine_eq, Submodule.mem_iSup, Submodule.starProjection_tendsto_closure_iSup, MeasureTheory.measure_sigmaFiniteSetGE_ge, ContinuousMap.edist_eq_iSup, iSup_lt_iff, sSup_add_distrib, ENat.iSup_coe_lt_top, Submodule.span_eq_iSup_of_singleton_spans, Seminorm.sSup_apply, NNReal.iSup_mul_le, egauge_pi', iSup_iInf_eq, MeasureTheory.Filtration.stronglyMeasurable_limitProcess, AddSubgroup.mem_biSup_of_directedOn, MeasureTheory.OuterMeasure.iSup_sInfGen_nonempty, ENNReal.toReal_iSup, sSup_eq_iSup', iSup_mono, Submonoid.FG.biSup, iSup_and, lowerSemicontinuous_biSup, Monotone.ciSup_comp_tendsto_atTop_of_linearOrder, SSet.range_eq_iSup_of_isColimit, Submodule.span_iUnion₂, FirstOrder.Language.DirectLimit.rangeLiftInclusion, iSup_eq_of_forall_le_of_forall_lt_exists_gt, Filter.limsup_top_eq_iSup, Filter.iSup_join, IsUltrametricDist.nnnorm_tsum_le, Antitone.ciSup_comp_tendsto_atBot_of_linearOrder, Nat.iSup_le_succ, ENNReal.add_biSup, Metric.ediam_insert, ContinuousMap.dist_eq_iSup, SSet.skeletonOfMono_succ, Ideal.span_iUnion, AddSubmonoid.iSup_eq_closure, PiLp.nndist_eq_iSup, Submodule.coe_iSup_of_chain, Finset.iSup_union, MeasurableSpace.measurableSet_iSup, FirstOrder.Language.DirectLimit.dom_partialEquivLimit, Filter.iSup_inf_principal, iSup_iSup_eq_left, biSup_finsetSigma, Finsupp.iSup_lsingle_range, iSup_inf_iSup, Ordinal.sup_typein_succ, MeasureTheory.Measure.iSup_restrict_spanningSets_of_measurableSet, IntermediateField.biSup_adjoin_simple, MeasureTheory.lintegral_le_iSup, Real.mul_iSup_of_nonneg, AddSubmonoid.mem_iSup_prop, SimpleGraph.radius_eq_iInf_iSup_edist, ENNReal.mul_iSup, Subring.closure_sUnion, iSup_prod, LeftOrdContinuous.map_iSup, Set.iInf_iSup_of_antitone, Subalgebra.unop_iSup, CategoryTheory.MorphismProperty.toSet_iSup, Directed.isLUB_ciSup, Submodule.finiteDimensional_iSup, EMetric.diam_iUnion_mem_option, Subring.closure_iUnion, UpperSet.Ici_iSup₂, ciSup_neg, CategoryTheory.ObjectProperty.prop_iSup_iff, ciSup_mono, HilbertBasis.finite_spans_dense, lt_iSup_iff
iSup_delab 📖	CompOp	—
«term⨅_,_» 📖	CompOp	—
«term⨆_,_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infSet_to_nonempty 📖	—	—	—	—	—
supSet_to_nonempty 📖	—	—	—	—	—

---

← Back to Index