Radon

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

Statistics

Metric	Count
Definitions	0
Theorems helly_theorem, helly_theorem', helly_theorem_compact, helly_theorem_compact', helly_theorem_set, helly_theorem_set', helly_theorem_set_compact, helly_theorem_set_compact', radon_partition	9
Total	9

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
helly_theorem 📖	—	Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Finset.card Convex SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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.Nonempty Set.iInter Finset Finset.instMembership	—	—	helly_theorem' Finset.exists_subsuperset_card_eq Set.Nonempty.mono Set.biInter_mono Set.Subset.rfl
helly_theorem' 📖	—	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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.Nonempty Set.iInter Finset Finset.instMembership	—	—	lt_or_ge le_of_lt Nat.le_induction le_of_eq Finset.mem_of_mem_erase subset_trans Finset.instIsTransSubset Finset.erase_subset Finset.card_erase_of_mem finrank_vectorSpan_le_iff_not_affineIndependent Fintype.card_coe LE.le.trans Submodule.finrank_le IsNoetherianRing.strongRankCondition EuclideanDomain.toNontrivial PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain radon_partition Set.mem_biInter convexHull_subset_iff Set.mem_of_subset_of_mem Set.biInter_subset_of_mem SetCoe.ext Set.Nonempty.some_mem compl_compl
helly_theorem_compact 📖	—	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.instNatCast Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne ENat.card Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsCompact Set.Nonempty Set.iInter Finset Finset.instMembership	—	—	helly_theorem_compact' Infinite.exists_superset_card_eq Finite.of_not_infinite Finset.exists_superset_card_eq Nat.cast_le IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass Nat.cast_add Nat.cast_one ENat.card_eq_coe_fintype_card Set.Nonempty.mono Set.biInter_mono subset_refl Set.instReflSubset
helly_theorem_compact' 📖	—	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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 IsCompact Set.Nonempty Set.iInter Finset Finset.instMembership	—	—	isEmpty_or_nonempty Set.iInter_of_empty AddTorsor.nonempty helly_theorem' IsCompact.inter_iInter_nonempty IsCompact.isClosed Set.iInter_congr_Prop Set.iInter_iInter_eq_or_left
helly_theorem_set 📖	—	Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Finset.card Set Convex SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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.Nonempty Set.sInter SetLike.coe Finset Finset.instSetLike	—	—	helly_theorem_set' Finset.exists_subsuperset_card_eq Set.sInter_mono instIsConcreteLE Set.Nonempty.mono
helly_theorem_set' 📖	—	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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.Nonempty Set.sInter SetLike.coe Finset Set Finset.instSetLike	—	—	Set.ext helly_theorem'
helly_theorem_set_compact 📖	—	ENat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.instNatCast Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set.encard Set Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsCompact Set.Nonempty Set.sInter SetLike.coe Finset Finset.instSetLike	—	—	helly_theorem_set_compact' Set.exists_superset_subset_encard_eq Set.encard_coe_eq_coe_finsetCard IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass Set.Nonempty.mono Set.sInter_mono Set.finite_of_encard_eq_coe Set.coe_toFinset ENat.coe_add ENat.coe_one Set.encard_eq_coe_toFinset_card
helly_theorem_set_compact' 📖	—	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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 IsCompact Set.Nonempty Set.sInter SetLike.coe Finset Set Finset.instSetLike	—	—	Set.ext Set.iInter_coe_set Set.iInter_congr_Prop helly_theorem_compact' Finset.coe_image Set.sInter_image Subtype.coe_preimage_self le_trans Finset.card_image_le
radon_partition 📖	mathematical	AffineIndependent DivisionRing.toRing Field.toDivisionRing addGroupIsAddTorsor AddCommGroup.toAddGroup	Set.Nonempty Set Set.instInter DFunLike.coe ClosureOperator PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid Set.image Compl.compl Set.instCompl	—	Mathlib.Tactic.Push.not_forall_eq affineIndependent_iff Finset.sum_congr Finset.filter.congr_simp Finset.sum_filter_add_sum_filter_not Finset.exists_pos_of_sum_zero_of_exists_nonzero IsStrictOrderedRing.toIsOrderedCancelAddMonoid Finset.sum_pos' Finset.mem_filter LT.lt.le Finset.centerMass_of_sum_add_sum_eq_zero Finset.centerMass_mem_convexHull Set.mem_image_of_mem Finset.centerMass_mem_convexHull_of_nonpos lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt sub_eq_zero_of_eq LE.le.not_gt

---

← Back to Index