Indicator

📁 Source: Mathlib/Algebra/Order/Group/Indicator.lean

Statistics

Metric	Count
Definitions	0
Theorems mulSupport_iInf, mulSupport_iSup, mulSupport_inf, mulSupport_max, mulSupport_min, mulSupport_sup, support_iInf, support_iSup, support_inf, support_max, support_min, support_sup, abs_indicator_symmDiff, iSup_indicator, iSup_mulIndicator, indicator_apply_le, indicator_apply_le', indicator_apply_nonneg, indicator_apply_nonpos, indicator_iInter_apply, indicator_iUnion_apply, indicator_le, indicator_le', indicator_le_indicator, indicator_le_indicator', indicator_le_indicator_apply_of_subset, indicator_le_indicator_nonneg, indicator_le_indicator_of_subset, indicator_le_self, indicator_le_self', indicator_mono, indicator_nonneg, indicator_nonpos, indicator_nonpos_le_indicator, le_indicator, le_indicator_apply, le_mulIndicator, le_mulIndicator_apply, mabs_mulIndicator_symmDiff, mulIndicator_apply_le, mulIndicator_apply_le', mulIndicator_apply_le_one, mulIndicator_iInter_apply, mulIndicator_iUnion_apply, mulIndicator_le, mulIndicator_le', mulIndicator_le_mulIndicator, mulIndicator_le_mulIndicator', mulIndicator_le_mulIndicator_apply_of_subset, mulIndicator_le_mulIndicator_of_subset, mulIndicator_le_one, mulIndicator_le_self, mulIndicator_le_self', mulIndicator_mono, one_le_mulIndicator, one_le_mulIndicator_apply	56
Total	56

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mulSupport_iInf 📖	mathematical	—	Set Set.instHasSubset mulSupport iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.iUnion	—	mulSupport_iSup
mulSupport_iSup 📖	mathematical	—	Set Set.instHasSubset mulSupport iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.iUnion	—	ciSup_const
mulSupport_inf 📖	mathematical	—	Set Set.instHasSubset mulSupport SemilatticeInf.toMin Set.instUnion	—	mulSupport_binop_subset inf_idem
mulSupport_max 📖	mathematical	—	Set Set.instHasSubset mulSupport SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instUnion	—	mulSupport_sup
mulSupport_min 📖	mathematical	—	Set Set.instHasSubset mulSupport SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instUnion	—	mulSupport_inf
mulSupport_sup 📖	mathematical	—	Set Set.instHasSubset mulSupport SemilatticeSup.toMax Set.instUnion	—	mulSupport_binop_subset sup_idem
support_iInf 📖	mathematical	—	Set Set.instHasSubset support iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.iUnion	—	support_iSup
support_iSup 📖	mathematical	—	Set Set.instHasSubset support iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.iUnion	—	support_subset_iff' Set.mem_iUnion notMem_support ciSup_const
support_inf 📖	mathematical	—	Set Set.instHasSubset support SemilatticeInf.toMin Set.instUnion	—	support_binop_subset inf_idem
support_max 📖	mathematical	—	Set Set.instHasSubset support SemilatticeSup.toMax Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instUnion	—	support_sup
support_min 📖	mathematical	—	Set Set.instHasSubset support SemilatticeInf.toMin Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set.instUnion	—	support_inf
support_sup 📖	mathematical	—	Set Set.instHasSubset support SemilatticeSup.toMax Set.instUnion	—	support_binop_subset sup_idem

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_indicator_symmDiff 📖	mathematical	—	abs AddCommGroup.toAddGroup indicator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra instSDiff SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	apply_indicator_symmDiff abs_neg
iSup_indicator 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Monotone Pi.preorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Set CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra	iSup Pi.supSet ConditionallyCompletePartialOrderSup.toSupSet indicator iUnion	—	le_antisymm_iff iSup_le_iff le_imp_le_of_le_of_le le_refl indicator_mono le_iSup indicator_le_indicator_of_subset subset_iUnion bot_le mem_iUnion indicator_of_mem iSup_apply iSup_le exists_ge_ge le_iSup_of_le LE.le.trans_eq indicator_of_notMem
iSup_mulIndicator 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Monotone Pi.preorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Set CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra	iSup Pi.supSet ConditionallyCompletePartialOrderSup.toSupSet mulIndicator iUnion	—	le_imp_le_of_le_of_le le_refl mulIndicator_mono le_iSup mulIndicator_le_mulIndicator_of_subset subset_iUnion mulIndicator_of_mem iSup_apply iSup_le exists_ge_ge le_iSup_of_le LE.le.trans_eq mulIndicator_of_notMem bot_le
indicator_apply_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	indicator_apply_le' zero_le
indicator_apply_le' 📖	mathematical	—	indicator	—	indicator_of_mem indicator_of_notMem
indicator_apply_nonneg 📖	mathematical	Preorder.toLE	indicator	—	le_indicator_apply le_rfl
indicator_apply_nonpos 📖	mathematical	Preorder.toLE	indicator	—	indicator_apply_le' le_rfl
indicator_iInter_apply 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	indicator iInter iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	—	indicator_of_mem mem_iInter ciInf_const indicator_of_notMem le_antisymm le_iInf_iff bot_le iInf_apply iInf_le
indicator_iUnion_apply 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	indicator iUnion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	—	indicator_of_mem le_antisymm mem_iUnion le_iSup_of_le ge_of_eq iSup_le indicator_le_self' bot_le indicator_of_notMem iSup_bot
indicator_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Pi.hasLe indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	indicator_le' zero_le
indicator_le' 📖	mathematical	—	Pi.hasLe indicator	—	indicator_apply_le'
indicator_le_indicator 📖	mathematical	Preorder.toLE	indicator	—	indicator_rel_indicator le_rfl
indicator_le_indicator' 📖	mathematical	Preorder.toLE	indicator	—	indicator_rel_indicator le_rfl
indicator_le_indicator_apply_of_subset 📖	mathematical	Set instHasSubset Preorder.toLE	indicator	—	indicator_apply_le' le_indicator_apply le_rfl indicator_apply_nonneg
indicator_le_indicator_nonneg 📖	mathematical	—	Pi.hasLe Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder indicator setOf	—	indicator_apply le_rfl LT.lt.le not_le
indicator_le_indicator_of_subset 📖	mathematical	Set instHasSubset Pi.hasLe Preorder.toLE Pi.instZero	indicator	—	indicator_le_indicator_apply_of_subset
indicator_le_self 📖	mathematical	—	Pi.hasLe Preorder.toLE PartialOrder.toPreorder indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	indicator_le_self' zero_le
indicator_le_self' 📖	mathematical	Preorder.toLE	Pi.hasLe indicator	—	indicator_le' le_rfl
indicator_mono 📖	mathematical	Pi.hasLe Preorder.toLE	indicator	—	indicator_le_indicator
indicator_nonneg 📖	mathematical	Preorder.toLE	indicator	—	indicator_apply_nonneg
indicator_nonpos 📖	mathematical	Preorder.toLE	indicator	—	indicator_apply_nonpos
indicator_nonpos_le_indicator 📖	mathematical	—	Pi.hasLe Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder indicator setOf	—	indicator_le_indicator_nonneg
le_indicator 📖	mathematical	—	Pi.hasLe indicator	—	le_indicator_apply
le_indicator_apply 📖	mathematical	—	indicator	—	indicator_apply_le'
le_mulIndicator 📖	mathematical	—	Pi.hasLe mulIndicator	—	le_mulIndicator_apply
le_mulIndicator_apply 📖	mathematical	—	mulIndicator	—	mulIndicator_apply_le'
mabs_mulIndicator_symmDiff 📖	mathematical	—	mabs CommGroup.toGroup mulIndicator InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid symmDiff Set SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra instSDiff DivInvMonoid.toDiv Group.toDivInvMonoid	—	apply_mulIndicator_symmDiff mabs_inv
mulIndicator_apply_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	mulIndicator MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	mulIndicator_apply_le' one_le
mulIndicator_apply_le' 📖	mathematical	—	mulIndicator	—	mulIndicator_of_mem mulIndicator_of_notMem
mulIndicator_apply_le_one 📖	mathematical	Preorder.toLE	mulIndicator	—	mulIndicator_apply_le' le_rfl
mulIndicator_iInter_apply 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	mulIndicator iInter iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	—	mulIndicator_of_mem ciInf_const mulIndicator_of_notMem le_antisymm iInf_apply iInf_le
mulIndicator_iUnion_apply 📖	mathematical	Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	mulIndicator iUnion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice	—	mulIndicator_of_mem le_antisymm mem_iUnion le_iSup_of_le ge_of_eq iSup_le mulIndicator_le_self' bot_le mulIndicator_of_notMem iSup_bot
mulIndicator_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	Pi.hasLe mulIndicator MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	mulIndicator_le' one_le
mulIndicator_le' 📖	mathematical	—	Pi.hasLe mulIndicator	—	mulIndicator_apply_le'
mulIndicator_le_mulIndicator 📖	mathematical	Preorder.toLE	mulIndicator	—	mulIndicator_rel_mulIndicator le_rfl
mulIndicator_le_mulIndicator' 📖	mathematical	Preorder.toLE	mulIndicator	—	mulIndicator_rel_mulIndicator le_rfl
mulIndicator_le_mulIndicator_apply_of_subset 📖	mathematical	Set instHasSubset Preorder.toLE	mulIndicator	—	mulIndicator_apply_le' le_mulIndicator_apply le_rfl one_le_mulIndicator_apply
mulIndicator_le_mulIndicator_of_subset 📖	mathematical	Set instHasSubset Pi.hasLe Preorder.toLE Pi.instOne	mulIndicator	—	mulIndicator_le_mulIndicator_apply_of_subset
mulIndicator_le_one 📖	mathematical	Preorder.toLE	mulIndicator	—	mulIndicator_apply_le_one
mulIndicator_le_self 📖	mathematical	—	Pi.hasLe Preorder.toLE PartialOrder.toPreorder mulIndicator MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass	—	mulIndicator_le_self' one_le
mulIndicator_le_self' 📖	mathematical	Preorder.toLE	Pi.hasLe mulIndicator	—	mulIndicator_le' le_rfl
mulIndicator_mono 📖	mathematical	Pi.hasLe Preorder.toLE	mulIndicator	—	mulIndicator_le_mulIndicator
one_le_mulIndicator 📖	mathematical	Preorder.toLE	mulIndicator	—	one_le_mulIndicator_apply
one_le_mulIndicator_apply 📖	mathematical	Preorder.toLE	mulIndicator	—	le_mulIndicator_apply le_rfl

---

← Back to Index