Indicator

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

Statistics

Metric	Count
Definitions `indicatorHom`, `mulIndicatorHom`	2
Theorems `map_indicator`, `map_mulIndicator`, `apply_indicator_symmDiff`, `apply_mulIndicator_symmDiff`, `indicator_add`, `indicator_add'`, `indicator_add_compl_eq_piecewise`, `indicator_add_eq_left`, `indicator_add_eq_right`, `indicator_compl`, `indicator_compl'`, `indicator_compl_add_self`, `indicator_compl_add_self_apply`, `indicator_diff`, `indicator_diff'`, `indicator_neg`, `indicator_neg'`, `indicator_self_add_compl`, `indicator_self_add_compl_apply`, `indicator_singleton`, `indicator_sub`, `indicator_sub'`, `indicator_symmDiff`, `indicator_union_add_inter`, `indicator_union_add_inter_apply`, `indicator_union_of_disjoint`, `indicator_union_of_notMem_inter`, `mulIndicator_compl`, `mulIndicator_compl'`, `mulIndicator_compl_mul_self`, `mulIndicator_compl_mul_self_apply`, `mulIndicator_diff`, `mulIndicator_diff'`, `mulIndicator_div`, `mulIndicator_div'`, `mulIndicator_inv`, `mulIndicator_inv'`, `mulIndicator_mul`, `mulIndicator_mul'`, `mulIndicator_mul_compl_eq_piecewise`, `mulIndicator_mul_eq_left`, `mulIndicator_mul_eq_right`, `mulIndicator_self_mul_compl`, `mulIndicator_self_mul_compl_apply`, `mulIndicator_singleton`, `mulIndicator_symmDiff`, `mulIndicator_union_mul_inter`, `mulIndicator_union_mul_inter_apply`, `mulIndicator_union_of_disjoint`, `mulIndicator_union_of_notMem_inter`, `map_indicator`, `map_mulIndicator`	52
Total	54

AddMonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_indicator` 📖	mathematical	—	`DFunLike.coe` `Set.indicator`	—	`map_indicator`

MonoidHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_mulIndicator` 📖	mathematical	—	`DFunLike.coe` `Set.mulIndicator`	—	`map_mulIndicator`

Set

Definitions

Name	Category	Theorems
`indicatorHom` 📖	CompOp	—
`mulIndicatorHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_indicator_symmDiff` 📖	mathematical	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`indicator` `NegZeroClass.toZero` `symmDiff` `Set` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `instSDiff` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`indicator_of_notMem` `mem_symmDiff` `indicator_of_mem` `sub_self` `sub_zero` `zero_sub`
`apply_mulIndicator_symmDiff` 📖	mathematical	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	`mulIndicator` `InvOneClass.toOne` `symmDiff` `Set` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `instSDiff` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`mulIndicator_of_notMem` `mulIndicator_of_mem` `div_self'` `div_one` `one_div`
`indicator_add` 📖	mathematical	—	`indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd`	—	`add_zero`
`indicator_add'` 📖	mathematical	—	`indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `Pi.instAdd` `AddZero.toAdd`	—	`indicator_add`
`indicator_add_compl_eq_piecewise` 📖	mathematical	—	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `indicator` `AddZero.toZero` `Compl.compl` `Set` `instCompl` `piecewise`	—	`piecewise_eq_of_mem` `Pi.add_apply` `indicator_of_mem` `indicator_of_notMem` `notMem_compl_iff` `add_zero` `piecewise_eq_of_notMem` `mem_compl` `zero_add`
`indicator_add_eq_left` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Function.support` `AddZero.toZero` `AddZeroClass.toAddZero`	`indicator` `Pi.instAdd` `AddZero.toAdd`	—	`indicator_congr` `Function.notMem_support` `disjoint_left` `Pi.add_apply` `add_zero` `indicator_support`
`indicator_add_eq_right` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Function.support` `AddZero.toZero` `AddZeroClass.toAddZero`	`indicator` `Pi.instAdd` `AddZero.toAdd`	—	`indicator_congr` `Function.notMem_support` `disjoint_right` `Pi.add_apply` `zero_add` `indicator_support`
`indicator_compl` 📖	mathematical	—	`indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Compl.compl` `Set` `instCompl` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`sub_eq_add_neg` `indicator_compl'`
`indicator_compl'` 📖	mathematical	—	`indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Compl.compl` `Set` `instCompl` `Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Pi.instNeg` `NegZeroClass.toNeg`	—	`eq_add_neg_of_add_eq` `indicator_compl_add_self`
`indicator_compl_add_self` 📖	mathematical	—	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `indicator` `AddZero.toZero` `Compl.compl` `Set` `instCompl`	—	`indicator_compl_add_self_apply`
`indicator_compl_add_self_apply` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `indicator` `AddZero.toZero` `Compl.compl` `Set` `instCompl`	—	`by_cases` `indicator_of_notMem` `mem_compl_iff` `indicator_of_mem` `zero_add` `add_zero`
`indicator_diff` 📖	mathematical	`Set` `instHasSubset`	`indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instSDiff` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`indicator_diff'` `sub_eq_add_neg`
`indicator_diff'` 📖	mathematical	`Set` `instHasSubset`	`indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instSDiff` `Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Pi.instNeg` `NegZeroClass.toNeg`	—	`eq_add_neg_of_add_eq` `Pi.add_def` `indicator_union_of_disjoint` `disjoint_sdiff_self_left` `diff_union_self` `union_eq_self_of_subset_right`
`indicator_neg` 📖	mathematical	—	`indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `NegZeroClass.toNeg`	—	`indicator_neg'`
`indicator_neg'` 📖	mathematical	—	`indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Pi.instNeg` `NegZeroClass.toNeg`	—	`AddMonoidHom.map_neg`
`indicator_self_add_compl` 📖	mathematical	—	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `indicator` `AddZero.toZero` `Compl.compl` `Set` `instCompl`	—	`indicator_self_add_compl_apply`
`indicator_self_add_compl_apply` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `indicator` `AddZero.toZero` `Compl.compl` `Set` `instCompl`	—	`by_cases` `indicator_of_mem` `indicator_of_notMem` `mem_compl_iff` `add_zero` `zero_add`
`indicator_singleton` 📖	mathematical	—	`indicator` `Set` `instSingletonSet` `Pi.single`	—	`indicator_apply` `mem_singleton_iff` `Pi.single_apply`
`indicator_sub` 📖	mathematical	—	`indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`AddMonoidHom.map_sub`
`indicator_sub'` 📖	mathematical	—	`indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`indicator_sub`
`indicator_symmDiff` 📖	mathematical	—	`indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `symmDiff` `Set` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `instSDiff` `Pi.instAdd` `AddZero.toAdd`	—	`indicator_union_of_disjoint` `Disjoint.mono_left` `sdiff_le` `disjoint_sdiff_self_right`
`indicator_union_add_inter` 📖	mathematical	—	`Pi.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `indicator` `AddZero.toZero` `Set` `instUnion` `instInter`	—	`indicator_union_add_inter_apply`
`indicator_union_add_inter_apply` 📖	mathematical	—	`AddZero.toAdd` `AddZeroClass.toAddZero` `indicator` `AddZero.toZero` `Set` `instUnion` `instInter`	—	`indicator_of_mem` `mem_union` `mem_inter_iff` `indicator_of_notMem` `add_zero` `zero_add`
`indicator_union_of_disjoint` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `instUnion` `AddZero.toAdd`	—	`indicator_union_of_notMem_inter` `Disjoint.le_bot`
`indicator_union_of_notMem_inter` 📖	mathematical	`Set` `instMembership` `instInter`	`indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `instUnion` `AddZero.toAdd`	—	`indicator_union_add_inter_apply` `indicator_of_notMem` `add_zero`
`mulIndicator_compl` 📖	mathematical	—	`mulIndicator` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Compl.compl` `Set` `instCompl` `Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Pi.instInv` `InvOneClass.toInv`	—	`eq_mul_inv_of_mul_eq` `mulIndicator_compl_mul_self`
`mulIndicator_compl'` 📖	mathematical	—	`mulIndicator` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Compl.compl` `Set` `instCompl` `Pi.instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`div_eq_mul_inv` `mulIndicator_compl`
`mulIndicator_compl_mul_self` 📖	mathematical	—	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `mulIndicator` `MulOne.toOne` `Compl.compl` `Set` `instCompl`	—	`mulIndicator_compl_mul_self_apply`
`mulIndicator_compl_mul_self_apply` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `mulIndicator` `MulOne.toOne` `Compl.compl` `Set` `instCompl`	—	`by_cases` `mulIndicator_of_notMem` `mulIndicator_of_mem` `one_mul` `mul_one`
`mulIndicator_diff` 📖	mathematical	`Set` `instHasSubset`	`mulIndicator` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instSDiff` `Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Pi.instInv` `InvOneClass.toInv`	—	`eq_mul_inv_of_mul_eq` `Pi.mul_def` `mulIndicator_union_of_disjoint` `disjoint_sdiff_self_left` `diff_union_self` `union_eq_self_of_subset_right`
`mulIndicator_diff'` 📖	mathematical	`Set` `instHasSubset`	`mulIndicator` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `instSDiff` `Pi.instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`mulIndicator_diff` `div_eq_mul_inv`
`mulIndicator_div` 📖	mathematical	—	`mulIndicator` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`MonoidHom.map_div`
`mulIndicator_div'` 📖	mathematical	—	`mulIndicator` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Pi.instDiv` `DivInvMonoid.toDiv` `Group.toDivInvMonoid`	—	`mulIndicator_div`
`mulIndicator_inv` 📖	mathematical	—	`mulIndicator` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `InvOneClass.toInv`	—	`mulIndicator_inv'`
`mulIndicator_inv'` 📖	mathematical	—	`mulIndicator` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Pi.instInv` `InvOneClass.toInv`	—	`MonoidHom.map_inv`
`mulIndicator_mul` 📖	mathematical	—	`mulIndicator` `MulOne.toOne` `MulOneClass.toMulOne` `MulOne.toMul`	—	`mul_one`
`mulIndicator_mul'` 📖	mathematical	—	`mulIndicator` `MulOne.toOne` `MulOneClass.toMulOne` `Pi.instMul` `MulOne.toMul`	—	`mulIndicator_mul`
`mulIndicator_mul_compl_eq_piecewise` 📖	mathematical	—	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `mulIndicator` `MulOne.toOne` `Compl.compl` `Set` `instCompl` `piecewise`	—	`piecewise_eq_of_mem` `Pi.mul_apply` `mulIndicator_of_mem` `mulIndicator_of_notMem` `notMem_compl_iff` `mul_one` `piecewise_eq_of_notMem` `mem_compl` `one_mul`
`mulIndicator_mul_eq_left` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Function.mulSupport` `MulOne.toOne` `MulOneClass.toMulOne`	`mulIndicator` `Pi.instMul` `MulOne.toMul`	—	`mulIndicator_congr` `Function.notMem_mulSupport` `disjoint_left` `Pi.mul_apply` `mul_one` `mulIndicator_mulSupport`
`mulIndicator_mul_eq_right` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Function.mulSupport` `MulOne.toOne` `MulOneClass.toMulOne`	`mulIndicator` `Pi.instMul` `MulOne.toMul`	—	`mulIndicator_congr` `Function.notMem_mulSupport` `disjoint_right` `Pi.mul_apply` `one_mul` `mulIndicator_mulSupport`
`mulIndicator_self_mul_compl` 📖	mathematical	—	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `mulIndicator` `MulOne.toOne` `Compl.compl` `Set` `instCompl`	—	`mulIndicator_self_mul_compl_apply`
`mulIndicator_self_mul_compl_apply` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `mulIndicator` `MulOne.toOne` `Compl.compl` `Set` `instCompl`	—	`by_cases` `mulIndicator_of_mem` `mulIndicator_of_notMem` `mul_one` `one_mul`
`mulIndicator_singleton` 📖	mathematical	—	`mulIndicator` `Set` `instSingletonSet` `Pi.mulSingle`	—	`mulIndicator_apply` `Pi.mulSingle_apply`
`mulIndicator_symmDiff` 📖	mathematical	—	`mulIndicator` `MulOne.toOne` `MulOneClass.toMulOne` `symmDiff` `Set` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `instSDiff` `Pi.instMul` `MulOne.toMul`	—	`mulIndicator_union_of_disjoint` `Disjoint.mono_left` `sdiff_le` `disjoint_sdiff_self_right`
`mulIndicator_union_mul_inter` 📖	mathematical	—	`Pi.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `mulIndicator` `MulOne.toOne` `Set` `instUnion` `instInter`	—	`mulIndicator_union_mul_inter_apply`
`mulIndicator_union_mul_inter_apply` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `mulIndicator` `MulOne.toOne` `Set` `instUnion` `instInter`	—	`mulIndicator_of_mem` `mulIndicator_of_notMem` `mul_one` `one_mul`
`mulIndicator_union_of_disjoint` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra`	`mulIndicator` `MulOne.toOne` `MulOneClass.toMulOne` `instUnion` `MulOne.toMul`	—	`mulIndicator_union_of_notMem_inter` `Disjoint.le_bot`
`mulIndicator_union_of_notMem_inter` 📖	mathematical	`Set` `instMembership` `instInter`	`mulIndicator` `MulOne.toOne` `MulOneClass.toMulOne` `instUnion` `MulOne.toMul`	—	`mulIndicator_union_mul_inter_apply` `mulIndicator_of_notMem` `mul_one`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_indicator` 📖	mathematical	—	`DFunLike.coe` `Set.indicator`	—	`Set.indicator_comp_of_zero` `map_zero`
`map_mulIndicator` 📖	mathematical	—	`DFunLike.coe` `Set.mulIndicator`	—	`Set.mulIndicator_comp_of_one` `map_one`

---

← Back to Index