DualFinite

📁 Source: Mathlib/Geometry/Convex/Cone/DualFinite.lean

Statistics

Metric	Count
Definitions DualFG	1
Theorems dual_dual_flip, dual_flip_dual, dual_of_fg, dual_of_finite, dual_of_finset, exists_fg_dual, id, iff_exists_fg_dual, inf, top, dual_dualfg	11
Total	12

PointedCone

Definitions

Name	Category	Theorems
DualFG 📖	MathDef	8 math math: DualFG.top, FG.dual_dualfg, DualFG.dual_of_finset, DualFG.id, DualFG.inf, DualFG.dual_of_fg, DualFG.dual_of_finite, DualFG.iff_exists_fg_dual

PointedCone.DualFG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dual_dual_flip 📖	mathematical	PointedCone.DualFG	PointedCone.dual CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.coe PointedCone CommSemiring.toSemiring Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule LinearMap.flip NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono exists_fg_dual PointedCone.dual_dual_flip_dual
dual_flip_dual 📖	mathematical	PointedCone.DualFG LinearMap.flip CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id Semiring.toNonAssocSemiring	PointedCone.dual CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.flip CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id Semiring.toNonAssocSemiring SetLike.coe PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Algebra.to_smulCommClass dual_dual_flip
dual_of_fg 📖	mathematical	Submodule.FG Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono AddCommGroup.toAddCommMonoid Nonneg.instModule	PointedCone.DualFG PointedCone.dual CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.coe PointedCone CommSemiring.toSemiring Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono PointedCone.dual_hull
dual_of_finite 📖	mathematical	—	PointedCone.DualFG PointedCone.dual CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	Algebra.to_smulCommClass Set.Finite.coe_toFinset
dual_of_finset 📖	mathematical	—	PointedCone.DualFG PointedCone.dual CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.coe Finset Finset.instSetLike	—	Algebra.to_smulCommClass
exists_fg_dual 📖	mathematical	PointedCone.DualFG	PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.FG Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule PointedCone.dual SetLike.coe Submodule.setLike	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Submodule.fg_span Finset.finite_toSet PointedCone.dual_hull
id 📖	mathematical	PointedCone.DualFG	PointedCone.DualFG LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.addCommGroup Ring.toAddCommGroup CommRing.toRing LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.id	—	Algebra.to_smulCommClass RingHomCompTriple.ids Finset.coe_image PointedCone.dual_image
iff_exists_fg_dual 📖	mathematical	—	PointedCone.DualFG PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.FG Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule PointedCone.dual SetLike.coe Submodule.setLike	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono exists_fg_dual PointedCone.dual_hull
inf 📖	mathematical	PointedCone.DualFG	PointedCone.DualFG PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instMin Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Finset.coe_union PointedCone.dual_union
top 📖	mathematical	—	PointedCone.DualFG Top.top PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instTop Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Finset.coe_empty PointedCone.dual_empty

PointedCone.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dual_dualfg 📖	mathematical	Submodule.FG Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono AddCommGroup.toAddCommMonoid Nonneg.instModule	PointedCone.DualFG PointedCone.dual CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.coe PointedCone CommSemiring.toSemiring Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	PointedCone.DualFG.dual_of_fg

---

← Back to Index