Documentation Verification Report

Extreme

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

Statistics

Metric	Count
Definitions `IsExtreme`, `extremePoints`	2
Theorems `mem_extremePoints_iff_convex_diff`, `mem_extremePoints_iff_mem_diff_convexHull_diff`, `antisymm`, `convex_diff`, `extremePoints_eq`, `extremePoints_subset_extremePoints`, `inter`, `left_mem_of_mem_openSegment`, `mem_extremePoints`, `mono`, `refl`, `rfl`, `right_mem_of_mem_openSegment`, `subset`, `trans`, `extremePoints_eq_self`, `extremePoints_convexHull_subset`, `extremePoints_empty`, `extremePoints_pi`, `extremePoints_prod`, `extremePoints_singleton`, `extremePoints_subset`, `image_extremePoints`, `instIsPartialOrderSetIsExtreme`, `inter_extremePoints_subset_extremePoints_of_subset`, `isExtreme_biInter`, `isExtreme_iInter`, `isExtreme_iff`, `isExtreme_sInter`, `isExtreme_singleton`, `mem_extremePoints`, `mem_extremePoints_iff_forall_segment`, `mem_extremePoints_iff_left`	33
Total	35

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_extremePoints_iff_convex_diff` 📖	mathematical	`Convex` `Ring.toSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`Set` `Set.instMembership` `Set.extremePoints` `Ring.toSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Convex` `Set.instSDiff` `Set.instSingletonSet`	—	`IsExtreme.convex_diff` `IsStrictOrderedRing.toIsOrderedRing` `isExtreme_singleton` `mem_extremePoints_iff_forall_segment` `convex_iff_segment_subset` `Set.mem_singleton_iff`
`mem_extremePoints_iff_mem_diff_convexHull_diff` 📖	mathematical	`Convex` `Ring.toSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`Set` `Set.instMembership` `Set.extremePoints` `Ring.toSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set.instSDiff` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Set.instSingletonSet`	—	`mem_extremePoints_iff_convex_diff` `convex_remove_iff_notMem_convexHull_remove` `Set.mem_diff`

IsExtreme

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antisymm` 📖	mathematical	—	`Set` `IsExtreme`	—	`Set.Subset.antisymm` `subset`
`convex_diff` 📖	mathematical	`Convex` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `IsExtreme`	`Convex` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set` `Set.instSDiff`	—	`convex_iff_openSegment_subset` `IsOrderedRing.toZeroLEOneClass` `Convex.openSegment_subset` `left_mem_of_mem_openSegment`
`extremePoints_eq` 📖	mathematical	`IsExtreme`	`Set.extremePoints` `Set` `Set.instInter`	—	`Set.Subset.antisymm` `extremePoints_subset_extremePoints` `inter_extremePoints_subset_extremePoints_of_subset` `subset`
`extremePoints_subset_extremePoints` 📖	mathematical	`IsExtreme`	`Set` `Set.instHasSubset` `Set.extremePoints`	—	`trans`
`inter` 📖	mathematical	`IsExtreme`	`IsExtreme` `Set` `Set.instInter`	—	`Set.Subset.trans` `Set.inter_subset_left` `subset` `left_mem_of_mem_openSegment`
`left_mem_of_mem_openSegment` 📖	mathematical	`IsExtreme` `Set` `Set.instMembership` `openSegment`	`Set` `Set.instMembership`	—	—
`mem_extremePoints` 📖	mathematical	`IsExtreme` `Set` `Set.instSingletonSet`	`Set` `Set.instMembership` `Set.extremePoints`	—	`isExtreme_singleton`
`mono` 📖	mathematical	`IsExtreme` `Set` `Set.instHasSubset`	`IsExtreme`	—	`left_mem_of_mem_openSegment`
`refl` 📖	mathematical	—	`IsExtreme`	—	`Set.Subset.rfl`
`rfl` 📖	mathematical	—	`IsExtreme`	—	`refl`
`right_mem_of_mem_openSegment` 📖	mathematical	`IsExtreme` `Set` `Set.instMembership` `openSegment`	`Set` `Set.instMembership`	—	`left_mem_of_mem_openSegment` `openSegment_symm`
`subset` 📖	mathematical	`IsExtreme`	`Set` `Set.instHasSubset`	—	—
`trans` 📖	mathematical	`IsExtreme`	`IsExtreme`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset` `left_mem_of_mem_openSegment` `right_mem_of_mem_openSegment`

Set

Definitions

Name	Category	Theorems
`extremePoints` 📖	CompOp	35 math math: `mem_extremePoints_iff_left`, `extremePoints_Icc`, `StrictConvex.diff_interior_subset_extremePoints`, `extremePoints_prod`, `isExtreme_singleton`, `extremePoints_pi`, `StrictConvex.extremePoints_eq_diff_interior`, `IsExtreme.mem_extremePoints`, `mem_extremePoints`, `Ergodic.iff_mem_extremePoints_measure_univ_eq`, `IsExtreme.extremePoints_subset_extremePoints`, `Convex.mem_extremePoints_iff_mem_diff_convexHull_diff`, `mem_extremePoints_iff_forall_segment`, `closure_convexHull_extremePoints`, `IsCompact.extremePoints_nonempty`, `extremePoints_closedBall_subset_sphere`, `StrictConvexSpace.extremePoints_closedBall_eq_sphere`, `Ergodic.iff_mem_extremePoints`, `extremePoints_doublyStochastic`, `StrictConvexSpace.sphere_subset_extremePoints_closedBall`, `extremePoints_singleton`, `extremePoints_convexHull_subset`, `exposedPoints_subset_extremePoints`, `surjOn_extremePoints_image`, `image_extremePoints`, `Ergodic.mem_extremePoints_measure_univ_eq`, `extremePoints_eq_self`, `extremePoints_subset`, `extremePoints_empty`, `disjoint_interior_extremePoints`, `IsExtreme.extremePoints_eq`, `Ergodic.mem_extremePoints`, `inter_extremePoints_subset_extremePoints_of_subset`, `Convex.convexIndependent_extremePoints`, `Convex.mem_extremePoints_iff_convex_diff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extremePoints_eq_self` 📖	mathematical	—	`extremePoints`	—	`subset_antisymm` `instAntisymmSubset` `extremePoints_subset`

(root)

Definitions

Name	Category	Theorems
`IsExtreme` 📖	CompData	13 math math: `IsExposed.isExtreme`, `isExtreme_singleton`, `IsExtreme.mono`, `IsExtreme.rfl`, `instIsPartialOrderSetIsExtreme`, `isExtreme_biInter`, `IsExtreme.trans`, `isExtreme_sInter`, `isExtreme_iInter`, `isExtreme_iff`, `IsExtreme.inter`, `IsExtreme.refl`, `IsExtreme.antisymm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`extremePoints_convexHull_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.extremePoints` `Ring.toSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull`	—	`convexHull_min` `Set.subset_diff` `subset_convexHull` `Set.disjoint_singleton_right` `Convex.mem_extremePoints_iff_convex_diff` `convex_convexHull`
`extremePoints_empty` 📖	mathematical	—	`Set.extremePoints` `Set` `Set.instEmptyCollection`	—	`Set.subset_empty_iff` `extremePoints_subset`
`extremePoints_pi` 📖	mathematical	—	`Set.extremePoints` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Pi.instSMul` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set.pi` `Set.univ` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`Set.ext` `Function.update_self` `eq_or_ne` `Function.update_of_ne` `Pi.image_update_openSegment` `Function.update_eq_self`
`extremePoints_prod` 📖	mathematical	—	`Set.extremePoints` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `SProd.sprod` `Set` `Set.instSProd`	—	`Set.ext` `Set.mk_mem_prod` `Prod.image_mk_openSegment_left` `Set.mem_image_of_mem` `Prod.image_mk_openSegment_right`
`extremePoints_singleton` 📖	mathematical	—	`Set.extremePoints` `Set` `Set.instSingletonSet`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `extremePoints_subset` `Set.singleton_subset_iff` `Set.mem_singleton`
`extremePoints_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.extremePoints`	—	—
`image_extremePoints` 📖	mathematical	—	`Set.image` `DFunLike.coe` `EquivLike.toFunLike` `Set.extremePoints` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`Set.ext` `EquivLike.surjective` `image_openSegment` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `SemilinearEquivClass.instSemilinearMapClass` `RingHomInvPair.ids` `Function.Injective.mem_set_image` `EquivLike.injective` `Function.Surjective.forall`
`instIsPartialOrderSetIsExtreme` 📖	mathematical	—	`IsPartialOrder` `Set` `IsExtreme`	—	`IsExtreme.antisymm` `IsExtreme.refl` `IsExtreme.trans`
`inter_extremePoints_subset_extremePoints_of_subset` 📖	mathematical	`Set` `Set.instHasSubset`	`Set` `Set.instHasSubset` `Set.instInter` `Set.extremePoints`	—	—
`isExtreme_biInter` 📖	mathematical	`Set.Nonempty` `Set` `IsExtreme`	`IsExtreme` `Set.iInter` `Set` `Set.instMembership`	—	`Set.iInter_subtype` `Set.iInter_congr_Prop` `isExtreme_iInter` `Set.Nonempty.to_subtype`
`isExtreme_iInter` 📖	mathematical	`IsExtreme`	`IsExtreme` `Set.iInter`	—	`Set.iInter_subset_of_subset` `IsExtreme.subset` `Set.mem_iInter` `IsExtreme.left_mem_of_mem_openSegment`
`isExtreme_iff` 📖	mathematical	—	`IsExtreme` `Set` `Set.instHasSubset` `Set.instMembership`	—	—
`isExtreme_sInter` 📖	mathematical	`Set.Nonempty` `Set` `IsExtreme`	`IsExtreme` `Set.sInter`	—	`Set.sInter_eq_biInter` `isExtreme_biInter`
`isExtreme_singleton` 📖	mathematical	—	`IsExtreme` `Set` `Set.instSingletonSet` `Set.instMembership` `Set.extremePoints`	—	—
`mem_extremePoints` 📖	mathematical	—	`Set` `Set.instMembership` `Set.extremePoints`	—	`openSegment_symm`
`mem_extremePoints_iff_forall_segment` 📖	mathematical	—	`Set` `Set.instMembership` `Set.extremePoints` `Ring.toSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`mem_extremePoints` `insert_endpoints_openSegment` `IsStrictOrderedRing.toZeroLEOneClass` `openSegment_subset_segment` `left_mem_openSegment_iff` `right_mem_openSegment_iff`
`mem_extremePoints_iff_left` 📖	mathematical	—	`Set` `Set.instMembership` `Set.extremePoints`	—	—

---

← Back to Index