AbsConvex

📁 Source: Mathlib/Analysis/LocallyConvex/AbsConvex.lean

Statistics

Metric	Count
Definitions AbsConvex, absConvexHull, closedAbsConvexHull	3
Theorems absConvexHull_eq, absConvexHull_subset_iff, closure, empty, iInter, iInter₂, inter, sInter, univ, absConvexHull, absConvexHull_add_subset, absConvexHull_empty, absConvexHull_eq_convexHull_balancedHull, absConvexHull_eq_empty, absConvexHull_eq_iInter, absConvexHull_eq_self, absConvexHull_isClosed, absConvexHull_min, absConvexHull_mono, absConvexHull_nonempty, absConvexHull_subset_closedAbsConvexHull, absConvexHull_univ, absConvex_absConvexHull, absConvex_closed_sInter, absConvex_convexClosedHull, balancedHull_convexHull_subseteq_absConvexHull, balancedHull_subset_convexHull_union_neg, balanced_absConvexHull, closedAbsConvexHull_closure_eq_closedAbsConvexHull, closedAbsConvexHull_eq_closure_absConvexHull, closedAbsConvexHull_isClosed, closedAbsConvexHull_min, closure_subset_closedAbsConvexHull, convexHull_union_neg_eq_absConvexHull, convex_absConvexHull, isClosed_closedAbsConvexHull, isCompact_closedAbsConvexHull_of_totallyBounded, mem_absConvexHull_iff, nhds_hasBasis_absConvex, nhds_hasBasis_absConvex_open, subset_absConvexHull, subset_closedAbsConvexHull, totallyBounded_absConvexHull, zero_mem_absConvexHull	44
Total	47

AbsConvex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absConvexHull_eq 📖	mathematical	AbsConvex	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull	—	absConvexHull_eq_self
absConvexHull_subset_iff 📖	mathematical	AbsConvex	Set Set.instHasSubset DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull	—	ClosureOperator.IsClosed.closure_le_iff
closure 📖	mathematical	AbsConvex SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	closure	—	Balanced.closure Convex.closure ContinuousSMul.continuousConstSMul
empty 📖	mathematical	—	AbsConvex Set Set.instEmptyCollection	—	balanced_empty convex_empty
iInter 📖	mathematical	AbsConvex	Set.iInter	—	sInter Set.sInter_range Set.forall_mem_range
iInter₂ 📖	mathematical	AbsConvex	Set.iInter	—	iInter
inter 📖	mathematical	AbsConvex	Set Set.instInter	—	Balanced.inter Convex.inter
sInter 📖	mathematical	AbsConvex	Set.sInter	—	Balanced.sInter convex_sInter
univ 📖	mathematical	—	AbsConvex Set.univ	—	balanced_univ convex_univ

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absConvexHull 📖	mathematical	Set.Nonempty	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull	—	absConvexHull_nonempty

(root)

Definitions

Name	Category	Theorems
AbsConvex 📖	MathDef	17 math math: nhds_hasBasis_absConvex_open, AbsConvex.empty, AbsConvexOpenSets.coe_nhds, AbsConvexOpenSets.coe_isOpen, absConvexHull_eq_self, nhds_hasBasis_absConvex, absConvex_convexClosedHull, absConvexHull_eq_iInter, absConvex_absConvexHull, LinearMap.polar_AbsConvex, absConvexHull_isClosed, AbsConvexOpenSets.coe_zero_mem, AbsConvexOpenSets.coe_convex, closedAbsConvexHull_isClosed, gaugeSeminormFamily_ball, AbsConvex.univ, AbsConvexOpenSets.coe_balanced
absConvexHull 📖	CompOp	25 math math: convexHull_union_neg_eq_absConvexHull, mem_absConvexHull_iff, subset_absConvexHull, totallyBounded_absConvexHull, absConvexHull_nonempty, absConvexHull_empty, absConvexHull_eq_self, absConvexHull_add_subset, convex_absConvexHull, absConvexHull_mono, Set.Nonempty.absConvexHull, absConvexHull_subset_closedAbsConvexHull, absConvexHull_eq_iInter, AbsConvex.absConvexHull_subset_iff, absConvex_absConvexHull, absConvexHull_min, zero_mem_absConvexHull, absConvexHull_univ, absConvexHull_isClosed, closedAbsConvexHull_eq_closure_absConvexHull, absConvexHull_eq_convexHull_balancedHull, absConvexHull_eq_empty, balanced_absConvexHull, balancedHull_convexHull_subseteq_absConvexHull, AbsConvex.absConvexHull_eq
closedAbsConvexHull 📖	CompOp	10 math math: subset_closedAbsConvexHull, closedAbsConvexHull_min, absConvex_convexClosedHull, isCompact_closedAbsConvexHull_of_totallyBounded, absConvexHull_subset_closedAbsConvexHull, closedAbsConvexHull_eq_closure_absConvexHull, closedAbsConvexHull_isClosed, isClosed_closedAbsConvexHull, closure_subset_closedAbsConvexHull, closedAbsConvexHull_closure_eq_closedAbsConvexHull

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absConvexHull_add_subset 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	absConvexHull_min Set.add_subset_add subset_absConvexHull Balanced.add balanced_absConvexHull Convex.add convex_absConvexHull
absConvexHull_empty 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull Set.instEmptyCollection	—	AbsConvex.absConvexHull_eq AbsConvex.empty
absConvexHull_eq_convexHull_balancedHull 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid convexHull balancedHull	—	le_antisymm absConvexHull_min HasSubset.Subset.trans Set.instIsTransSubset subset_convexHull convexHull_mono subset_balancedHull NormedDivisionRing.to_normOneClass Balanced.convexHull balancedHull.balanced convex_convexHull convexHull_min Balanced.balancedHull_subset_of_subset balanced_absConvexHull subset_absConvexHull convex_absConvexHull
absConvexHull_eq_empty 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull Set.instEmptyCollection	—	Set.subset_empty_iff subset_absConvexHull absConvexHull_empty
absConvexHull_eq_iInter 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull Set.iInter Set.instHasSubset AbsConvex	—	Set.iInter_subtype Set.iInter_congr_Prop Set.iInter_and
absConvexHull_eq_self 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull AbsConvex	—	ClosureOperator.isClosed_iff
absConvexHull_isClosed 📖	mathematical	—	ClosureOperator.IsClosed Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra absConvexHull AbsConvex	—	—
absConvexHull_min 📖	mathematical	Set Set.instHasSubset AbsConvex	DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull	—	ClosureOperator.closure_min
absConvexHull_mono 📖	mathematical	Set Set.instHasSubset	DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull	—	ClosureOperator.monotone
absConvexHull_nonempty 📖	mathematical	—	Set.Nonempty DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull	—	Set.nonempty_iff_ne_empty absConvexHull_eq_empty
absConvexHull_subset_closedAbsConvexHull 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull closedAbsConvexHull	—	absConvexHull_min subset_closedAbsConvexHull absConvex_convexClosedHull
absConvexHull_univ 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull Set.univ	—	ClosureOperator.closure_top
absConvex_absConvexHull 📖	mathematical	—	AbsConvex DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull	—	ClosureOperator.isClosed_closure
absConvex_closed_sInter 📖	mathematical	AbsConvex IsClosed	Set.sInter	—	AbsConvex.sInter isClosed_sInter
absConvex_convexClosedHull 📖	mathematical	—	AbsConvex DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedAbsConvexHull	—	ClosureOperator.isClosed_closure
balancedHull_convexHull_subseteq_absConvexHull 📖	mathematical	—	Set Set.instHasSubset balancedHull SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull absConvexHull	—	Balanced.balancedHull_subset_of_subset balanced_absConvexHull convexHull_min subset_absConvexHull convex_absConvexHull
balancedHull_subset_convexHull_union_neg 📖	mathematical	—	Set Set.instHasSubset balancedHull Real SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Real.partialOrder Set.instUnion Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	mem_balancedHull_iff segment_subset_convexHull Set.mem_union_left Set.mem_union_right Set.neg_mem_neg neg_le_iff_add_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_le_of_abs_le sub_nonneg covariant_swap_add_of_covariant_add le_of_abs_le Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz smul_neg sub_eq_add_neg sub_smul Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero
balanced_absConvexHull 📖	mathematical	—	Balanced DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull	—	absConvex_absConvexHull
closedAbsConvexHull_closure_eq_closedAbsConvexHull 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedAbsConvexHull closure	—	subset_antisymm Set.instAntisymmSubset ClosureOperator.idempotent ClosureOperator.monotone closure_subset_closedAbsConvexHull subset_closure
closedAbsConvexHull_eq_closure_absConvexHull 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedAbsConvexHull SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid closure absConvexHull	—	subset_antisymm Set.instAntisymmSubset closedAbsConvexHull_min subset_trans Set.instIsTransSubset subset_absConvexHull subset_closure AbsConvex.closure absConvex_absConvexHull isClosed_closure closure_minimal absConvexHull_subset_closedAbsConvexHull isClosed_closedAbsConvexHull
closedAbsConvexHull_isClosed 📖	mathematical	—	ClosureOperator.IsClosed Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra closedAbsConvexHull AbsConvex IsClosed	—	—
closedAbsConvexHull_min 📖	mathematical	Set Set.instHasSubset AbsConvex	DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedAbsConvexHull	—	ClosureOperator.closure_min
closure_subset_closedAbsConvexHull 📖	mathematical	—	Set Set.instHasSubset closure DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedAbsConvexHull	—	closure_minimal subset_closedAbsConvexHull isClosed_closedAbsConvexHull
convexHull_union_neg_eq_absConvexHull 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid Set.instUnion Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid absConvexHull SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction	—	absConvexHull_eq_convexHull_balancedHull le_antisymm convexHull_mono Set.union_subset subset_balancedHull NormedDivisionRing.to_normOneClass mem_balancedHull_iff norm_neg NormOneClass.norm_one Set.neg_smul_set one_smul Convex.convexHull_eq convex_convexHull balancedHull_subset_convexHull_union_neg
convex_absConvexHull 📖	mathematical	—	Convex Ring.toSemiring SeminormedRing.toRing DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull	—	absConvex_absConvexHull
isClosed_closedAbsConvexHull 📖	mathematical	—	IsClosed DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedAbsConvexHull	—	ClosureOperator.isClosed_closure
isCompact_closedAbsConvexHull_of_totallyBounded 📖	mathematical	TotallyBounded	IsCompact UniformSpace.toTopologicalSpace DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedAbsConvexHull Real SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid Real.partialOrder	—	closedAbsConvexHull_eq_closure_absConvexHull IsUniformAddGroup.to_topologicalAddGroup isCompact_closure_of_totallyBounded_quasiComplete totallyBounded_absConvexHull
mem_absConvexHull_iff 📖	mathematical	—	Set Set.instMembership DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull	—	absConvexHull_eq_iInter
nhds_hasBasis_absConvex 📖	mathematical	—	Filter.HasBasis Set nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Filter Filter.instMembership AbsConvex SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	Filter.HasBasis.to_hasBasis LocallyConvexSpace.convex_basis_zero Filter.mem_of_superset balancedCore_mem_nhds_zero NormedField.nhdsNE_neBot subset_convexHull Balanced.convexHull balancedCore_balanced convex_convexHull convexHull_min balancedCore_subset Eq.subset Set.instReflSubset
nhds_hasBasis_absConvex_open 📖	mathematical	—	Filter.HasBasis Set nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.instMembership IsOpen AbsConvex SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	Filter.HasBasis.to_hasBasis nhds_hasBasis_absConvex mem_interior_iff_mem_nhds isOpen_interior Balanced.interior Convex.interior ContinuousSMul.continuousConstSMul interior_subset IsOpen.mem_nhds Eq.subset Set.instReflSubset
subset_absConvexHull 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull	—	ClosureOperator.le_closure
subset_closedAbsConvexHull 📖	mathematical	—	Set Set.instHasSubset DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedAbsConvexHull	—	ClosureOperator.le_closure
totallyBounded_absConvexHull 📖	mathematical	TotallyBounded	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull Real SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid Real.partialOrder	—	convexHull_union_neg_eq_absConvexHull totallyBounded_convexHull totallyBounded_union totallyBounded_neg
zero_mem_absConvexHull 📖	mathematical	—	Set Set.instMembership DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike absConvexHull SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SeminormedRing.toRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Balanced.zero_mem balanced_absConvexHull Set.Nonempty.mono subset_absConvexHull Set.Nonempty.of_subtype

---

← Back to Index