AddTorsorBases

📁 Source: Mathlib/Analysis/Normed/Affine/AddTorsorBases.lean

Statistics

Metric	Count
Definitions	0
Theorems centroid_mem_interior_convexHull, interior_convexHull, interior_nonempty_iff_affineSpan_eq_top, affineSpan_eq_top, exists_between_affineIndependent_span_eq_top, exists_subset_affineIndependent_span_eq_top, affineSpan_eq_top_of_nonempty_interior, continuous_barycentric_coord, interior_convexHull_nonempty_iff_affineSpan_eq_top, isOpenMap_barycentric_coord	10
Total	10

AffineBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
centroid_mem_interior_convexHull 📖	mathematical	—	Set Set.instMembership interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Set.range AffineBasis NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor Real.instRing instFunLike Finset.centroid Real.instDivisionRing Finset.univ	—	interior_convexHull Finite.of_fintype coord_apply_centroid RCLike.charZero_rclike Finset.mem_univ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instIsOrderedRing Real.instNontrivial nonempty
interior_convexHull 📖	mathematical	—	interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Set.range AffineBasis NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor Real.instRing instFunLike setOf	—	subsingleton_or_nontrivial AffineSubspace.eq_univ_of_subsingleton_span_eq_top Set.subsingleton_range tot convexHull_univ interior_univ coe_coord_of_subsingleton_eq_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike convexHull_eq_nonneg_coord Real.instIsStrictOrderedRing Set.setOf_forall Set.ext interior_iInter_of_finite IsOpenMap.preimage_interior_eq_interior_preimage isOpenMap_barycentric_coord Real.instCompleteSpace continuous_barycentric_coord finiteDimensional interior_Ici instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
interior_nonempty_iff_affineSpan_eq_top 📖	mathematical	Convex Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField	Set.Nonempty interior affineSpan Real.instRing NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	interior_convexHull_nonempty_iff_affineSpan_eq_top convexHull_eq

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineSpan_eq_top 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.Nonempty	affineSpan Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	exists_subset_affineIndependent_span_eq_top top_unique affineSpan_mono
exists_between_affineIndependent_span_eq_top 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set Set.instHasSubset Set.Nonempty AffineIndependent Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor Set.instMembership	affineSpan Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Filter.HasBasis.mem_iff Metric.nhds_basis_closedBall mem_nhds exists_subset_affineIndependent_affineSpan_eq_top Metric.mem_closedBall AffineMap.lineMap_apply dist_vadd_left norm_smul NormedSpace.toNormSMulClass Real.norm_eq_abs dist_eq_norm_vsub abs_div Real.instIsStrictOrderedRing abs_of_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid abs_of_nonneg norm_nonneg div_mul_comm mul_le_of_le_one_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing LT.lt.le div_self_le_one Real.instZeroLEOneClass div_ne_zero LT.lt.ne' dist_ne_zero AffineMap.lineMap_apply_one AffineIndependent.range AffineIndependent.units_lineMap affineSpan_eq_affineSpan_lineMap_units Real.instNontrivial
exists_subset_affineIndependent_span_eq_top 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.Nonempty	Set Set.instHasSubset AffineIndependent Real Real.instRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor Set.instMembership affineSpan Top.top AffineSubspace OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	exists_between_affineIndependent_span_eq_top Set.singleton_subset_iff Set.singleton_nonempty affineIndependent_of_subsingleton Unique.instSubsingleton

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
affineSpan_eq_top_of_nonempty_interior 📖	mathematical	Set.Nonempty interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField	affineSpan Real.instRing NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor Top.top AffineSubspace OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique LE.le.trans_eq affineSpan_mono interior_subset affineSpan_convexHull IsOpen.affineSpan_eq_top isOpen_interior
continuous_barycentric_coord 📖	mathematical	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField DFunLike.coe AffineMap NormedRing.toRing NormedCommRing.toNormedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AffineMap.instFunLike AffineBasis.coord	—	AffineMap.continuous_of_finiteDimensional
interior_convexHull_nonempty_iff_affineSpan_eq_top 📖	mathematical	—	Set.Nonempty interior UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Real Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField affineSpan Real.instRing NormedAddCommGroup.toAddCommGroup NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toNormedAddTorsor Top.top AffineSubspace OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice AffineSubspace.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	affineSpan_eq_top_of_nonempty_interior AffineBasis.exists_affine_subbasis CanLift.prf Set.instCanLiftFinsetCoeFinite AffineBasis.finite_set AffineBasis.centroid_mem_interior_convexHull Set.Nonempty.mono interior_mono convexHull_mono Set.setOf_mem_eq Subtype.range_coe_subtype
isOpenMap_barycentric_coord 📖	mathematical	—	IsOpenMap UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField DFunLike.coe AffineMap NormedRing.toRing NormedCommRing.toNormedRing NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AffineMap.instFunLike AffineBasis.coord	—	AffineMap.isOpenMap_linear_iff instIsTopologicalAddTorsor_1 LinearMap.isOpenMap_of_finiteDimensional SeminormedAddCommGroup.toIsTopologicalAddGroup IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self AffineMap.linear_surjective_iff AffineBasis.surjective_coord

---

← Back to Index