instFunLike 📖 | CompOp | 245 mathmath: upperBounds_supClosure, setOf_isClosed_eq_range_closure, convexIndependent_set_iff_inter_convexHull_subset, IsLinearMap.image_convexHull, convexHull_insert, subset_closedConvexHull, Geometry.SimplicialComplex.vertex_mem_convexHull_iff, closedConvexHull_min, convexHull_multiset_sum, Geometry.SimplicialComplex.convexHull_subset_space, ofCompletePred_apply, closure_iSup₂_closure, supClosure_eq_self, Geometry.SimplicialComplex.mem_space_iff, isSublattice_latticeClosure, Convex.convex_remove_iff_notMem_convexHull_remove, inf_mem_infClosure, convexHull_eq_iInter, latticeClosure_univ, Complex.convexHull_reProdIm, isGLB_infClosure, convexJoin_segments, IsSublattice.latticeClosure_eq, convexHull_union_neg_eq_absConvexHull, interior_convexHull_nonempty_iff_affineSpan_eq_top, mem_absConvexHull_iff, conjBy_apply, Geometry.SimplicialComplex.convexHull_inter_convexHull, AffineBasis.convexHull_eq_nonneg_coord, segment_subset_convexHull, convexHull_toCone_eq_sInf, Balanced.convexHull, subset_absConvexHull, balancedHull_subset_convexHull_union_neg, Convex.convexHull_union, closedConvexHull_eq_closure_convexHull, Finset.mem_convexHull', subset_convexHull, Convex.convexHull_subset_iff, AffineBasis.interior_convexHull, Set.Finite.infClosure, ofDual_preimage_latticeClosure, Geometry.SimplicialComplex.inter_subset_convexHull, convexJoin_segment_singleton, le_closure_iff, convexJoin_singleton_segment, convexHull_diam, subset_closedAbsConvexHull, Finset.centerMass_id_mem_convexHull, latticeClosure_mono, Set.Finite.isCompact_convexHull, image_latticeClosure', Finset.centerMass_id_mem_convexHull_of_nonpos, convexHull_add, affineSpan_convexHull, MeasureTheory.IsSetSemiring.isSetRing_supClosure, convexHull_basis_eq_stdSimplex, MeasureTheory.AddContent.supClosure_apply_finpartition, Convex.radon_partition, ConvexOn.bddAbove_convexHull, MeasureTheory.IsSetSemiring.mem_supClosure_iff, SupClosed.infClosure, Matroid.closure_eq_subtypeClosure, infClosed_infClosure, ConvexIndependent.mem_convexHull_iff, not_disjoint_segment_convexHull_triple, convexHull_vadd, MeasureTheory.dense_of_generateFrom_isSetSemiring, exists_mem_interior_convexHull_affineBasis, supClosure_empty, compl_image_latticeClosure, closedAbsConvexHull_min, ofPred_apply, PrimitiveSpectrum.gc_closureOperator, totallyBounded_absConvexHull, ext_iff, infClosure_singleton, absConvexHull_nonempty, absConvexHull_empty, absConvexHull_eq_self, Convex.mem_extremePoints_iff_mem_diff_convexHull_diff, latticeClosure_prod, InfClosed.infClosure_eq, le_closure, convexHull_add_subset, MeasureTheory.IsSetSemiring.diff_mem_supClosure, infClosure_eq_self, closedConvexHull_closure_eq_closedConvexHull, compl_image_latticeClosure_eq_of_compl_image_eq_self, Polynomial.rootSet_derivative_subset_convexHull_rootSet, latticeClosure_singleton, closure_convexHull_extremePoints, closure_sup_closure_right, Set.Finite.isClosed_convexHull, convexHull_empty, absConvexHull_add_subset, Finset.centerMass_mem_convexHull, convexHull_pair, infClosure_univ, subset_latticeClosure, convexJoin_subset_convexHull, Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull, subset_infClosure, convexHull_eq_empty, convexHull_singleton, BooleanSubalgebra.latticeClosure_subset_closure, convex_convexHull, convexHull_sum, isBounded_convexHull, Finset.mem_convexHull, BooleanSubalgebra.closure_latticeClosure, convexHull_neg, convexIndependent_set_iff_notMem_convexHull_diff, convexHull_sphere_eq_closedBall, Set.Finite.supClosure, Convex.exists_subset_interior_convexHull_finset_of_isCompact, IntermediateField.normalClosureOperator_apply, convexHull_mono, convex_absConvexHull, convexHullAddMonoidHom_apply, absConvexHull_mono, Finset.convexHull_eq, totallyBounded_convexHull, Set.Nonempty.absConvexHull, sup_mem_supClosure, closure_sup_closure_left, lowerBounds_infClosure, absConvex_convexClosedHull, closure_sup_closure, convexHull_eq_singleton, convexHull_eq_zero, closure_iSup_closure, isCompact_closedAbsConvexHull_of_totallyBounded, absConvexHull_subset_closedAbsConvexHull, toWeakSpace_closedConvexHull_eq, convexHull_pi, closure_min, supClosure_singleton, image_latticeClosure, doublyStochastic_eq_convexHull_permMatrix, latticeClosure_eq_self, absConvexHull_eq_iInter, latticeClosure_empty, Finset.centroid_mem_convexHull, supClosure_mono, LowerAdjoint.closureOperator_apply, AbsConvex.absConvexHull_subset_iff, SupClosed.supClosure_eq, PrimitiveSpectrum.closedsGC_closureOperator, absConvex_absConvexHull, LinearMap.image_convexHull, IsClosed.closure_le_iff, convexHull_univ, convexHull_ediam, infClosure_min, absConvexHull_min, AffineIndependent.convexHull_inter', mk'_apply, latticeClosure_idem, closure_top, convexHull_zero, isClosed_iff_closure_le, convexHull_eq_union_convexHull_finite_subsets, zero_mem_absConvexHull, infClosure_prod, affineCombination_mem_convexHull, mem_convexHull_iff_exists_fintype, absConvexHull_univ, convexHull_toCone_isLeast, Set.Finite.latticeClosure, extremePoints_convexHull_subset, Geometry.SimplicialComplex.face_subset_face_iff, Convex.convexHull_eq, convexHull_convexHull_union_right, mk₂_apply, supClosure_infClosure, closure_inf_le, infClosure_mono, convexHull_convexHull_union_left, convexHull_min, MeasureTheory.AddContent.supClosure_apply_of_mem, InfClosed.supClosure, closedAbsConvexHull_eq_closure_absConvexHull, convexHull_prod, infClosure_supClosure, convexHull_eq_union, convexHull_eq, monotone, supClosure_idem, convexHull_smul, Set.Nonempty.convexHull, absConvexHull_eq_convexHull_balancedHull, Set.Finite.convexHull_eq_image, infClosure_idem, GaloisConnection.closureOperator_apply, mem_convexHull_of_exists_fintype, MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring, convexHull_rangle_single_eq_stdSimplex, AffineBasis.centroid_mem_interior_convexHull, AffineMap.image_convexHull, convexHull_union, convexHull_sub, closure_subset_closedConvexHull, ConcaveOn.bddBelow_convexHull, convexHull_list_sum, convexHull_nonempty_iff, subset_supClosure, finsetInf'_mem_infClosure, mem_convexHull_iff, parallelepiped_eq_convexHull, instOrderHomClass, eq_ofPred_closed, absConvexHull_eq_empty, isLUB_supClosure, isClosed_closedAbsConvexHull, supClosure_prod, AffineIndependent.convexHull_inter, finsetSup'_mem_supClosure, infClosure_empty, convex_closedConvexHull, closure_subset_closedAbsConvexHull, MeasureTheory.AddContent.supClosure_apply, IsClosed.closure_eq, closure_sup_closure_le, Set.Finite.convexHull_eq, supClosed_supClosure, isClosed_closedConvexHull, balanced_absConvexHull, convexHull_subset_affineSpan, idempotent, convexHull_eq_self, isClosed_closure, supClosure_univ, id_apply, balancedHull_convexHull_subseteq_absConvexHull, latticeClosure_min, convexHull_range_eq_exists_affineCombination, convexIndependent_iff_notMem_convexHull_diff, closure_isGLB, AbsConvex.absConvexHull_eq, supClosure_min, closedAbsConvexHull_closure_eq_closedAbsConvexHull, Complex.rectangle_eq_convexHull, convexHull_subset_closedConvexHull, Finset.centerMass_mem_convexHull_of_nonpos
|