Documentation Verification Report

Exposed

📁 Source: Mathlib/Analysis/Convex/Exposed.lean

Statistics

Metric	Count
Definitions `toExposed`, `IsExposed`, `exposedPoints`	3
Theorems `isExposed`, `antisymm`, `convex`, `eq_inter_halfSpace`, `eq_inter_halfSpace'`, `inter`, `inter_left`, `inter_right`, `isClosed`, `isCompact`, `isExtreme`, `mono`, `refl`, `sInter`, `subset`, `exposedPoints_empty`, `exposedPoints_subset`, `exposedPoints_subset_extremePoints`, `exposed_point_def`, `isExposed_empty`, `mem_exposedPoints_iff_exposed_singleton`	21
Total	24

ContinuousLinearMap

Definitions

Name	Category	Theorems
`toExposed` 📖	CompOp	1 math math: `toExposed.isExposed`

ContinuousLinearMap.toExposed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isExposed` 📖	mathematical	—	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder` `ContinuousLinearMap.toExposed`	—	—

IsExposed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antisymm` 📖	—	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder`	—	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `subset`
`convex` 📖	—	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Convex` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—	`Set.eq_empty_or_nonempty` `convex_empty` `ConcaveOn.convex_ge` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `LinearMap.concaveOn` `convex_univ` `Set.mem_univ`
`eq_inter_halfSpace` 📖	mathematical	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder`	`setOf` `Set` `Set.instMembership` `Preorder.toLE` `DFunLike.coe` `StrongDual` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`Set.eq_empty_or_nonempty` `Set.eq_empty_iff_forall_notMem` `not_le_of_gt` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `NeZero.one` `ContinuousLinearMap.zero_apply` `eq_inter_halfSpace'`
`eq_inter_halfSpace'` 📖	mathematical	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder` `Set.Nonempty`	`setOf` `Set` `Set.instMembership` `Preorder.toLE` `DFunLike.coe` `StrongDual` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`Set.Subset.antisymm` `LE.le.trans`
`inter` 📖	mathematical	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder`	`Set` `Set.instInter`	—	`Set.Subset.antisymm` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `add_le_add_iff_right` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `IsOrderedCancelAddMonoid.toAddLeftReflectLT` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `LE.le.trans` `add_le_add_iff_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `le_trans`
`inter_left` 📖	mathematical	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder` `Set` `Set.instHasSubset`	`Set.instInter`	—	`Set.Subset.antisymm` `LE.le.trans` `subset`
`inter_right` 📖	mathematical	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder` `Set` `Set.instHasSubset`	`Set.instInter`	—	`Set.inter_comm` `inter_left`
`isClosed` 📖	mathematical	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder`	`IsClosed`	—	`Set.eq_empty_or_nonempty` `eq_inter_halfSpace'` `IsClosed.isClosed_le` `continuousOn_const` `Continuous.continuousOn` `ContinuousLinearMap.continuous`
`isCompact` 📖	—	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder` `IsCompact`	—	—	`IsCompact.of_isClosed_subset` `isClosed` `IsCompact.isClosed` `subset`
`isExtreme` 📖	mathematical	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`IsExtreme` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`subset` `LinearMap.convexOn` `convex_univ` `LE.le.antisymm` `ConvexOn.le_left_of_right_le` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsStrictOrderedModule.toPosSMulStrictMono` `IsStrictOrderedRing.toIsStrictOrderedModule` `Set.mem_univ`
`mono` 📖	—	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder` `Set` `Set.instHasSubset`	—	—	`Set.Subset.antisymm` `LE.le.trans`
`refl` 📖	mathematical	—	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder`	—	`Set.Subset.antisymm` `le_refl`
`sInter` 📖	mathematical	`Finset.Nonempty` `Set` `IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder`	`Set.sInter` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Finset.induction` `Finset.not_nonempty_empty` `Finset.coe_insert` `Set.sInter_insert` `Finset.eq_empty_or_nonempty` `Finset.coe_empty` `Set.sInter_empty` `Set.inter_univ` `Finset.mem_singleton_self` `inter` `Finset.mem_insert_self` `Finset.mem_insert_of_mem`
`subset` 📖	mathematical	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder`	`Set` `Set.instHasSubset`	—	—

Set

Definitions

Name	Category	Theorems
`exposedPoints` 📖	CompOp	5 math math: `exposedPoints_subset`, `exposed_point_def`, `exposedPoints_subset_extremePoints`, `exposedPoints_empty`, `mem_exposedPoints_iff_exposed_singleton`

(root)

Definitions

Name	Category	Theorems
`IsExposed` 📖	MathDef	4 math math: `IsExposed.refl`, `ContinuousLinearMap.toExposed.isExposed`, `isExposed_empty`, `mem_exposedPoints_iff_exposed_singleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exposedPoints_empty` 📖	mathematical	—	`Set.exposedPoints` `Set` `Set.instEmptyCollection`	—	`Set.subset_empty_iff` `exposedPoints_subset`
`exposedPoints_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.exposedPoints`	—	—
`exposedPoints_subset_extremePoints` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.exposedPoints` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.extremePoints` `Ring.toSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`IsExtreme.mem_extremePoints` `IsExposed.isExtreme` `mem_exposedPoints_iff_exposed_singleton`
`exposed_point_def` 📖	mathematical	—	`Set` `Set.instMembership` `Set.exposedPoints` `Preorder.toLE` `PartialOrder.toPreorder` `DFunLike.coe` `StrongDual` `Ring.toSemiring` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	—
`isExposed_empty` 📖	mathematical	—	`IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder` `Set` `Set.instEmptyCollection`	—	—
`mem_exposedPoints_iff_exposed_singleton` 📖	mathematical	—	`Set` `Set.instMembership` `Set.exposedPoints` `IsExposed` `Ring.toSemiring` `PartialOrder.toPreorder` `Set.instSingletonSet`	—	`Set.eq_singleton_iff_unique_mem` `Set.mem_singleton` `LE.le.trans`

---

← Back to Index