Basic

📁 Source: Mathlib/Algebra/FiniteSupport/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `comp`, `comp_of_injective`, `div`, `fst`, `fun_comp`, `fun_comp_of_injective`, `fun_div`, `fun_inv`, `fun_mul`, `fun_pow`, `fun_zpow`, `iInf`, `iSup`, `inf`, `inf'`, `inv`, `max`, `min`, `mul`, `of_comp`, `pi`, `pow`, `prod`, `prodMk`, `snd`, `sup`, `sup'`, `zpow`, `add`, `comp`, `comp_of_injective`, `fst`, `fun_add`, `fun_comp`, `fun_comp_of_injective`, `fun_neg`, `fun_nsmul`, `fun_sub`, `fun_zsmul`, `iInf`, `iSup`, `inf`, `inf'`, `max`, `min`, `neg`, `nsmul`, `of_comp`, `pi`, `snd`, `sub`, `sum`, `sumMk`, `sup`, `sup'`, `zsmul`, `hasFiniteMulSupport_fun_one`, `hasFiniteSupport_fun_zero`	58
Total	58

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasFiniteMulSupport_fun_one` 📖	mathematical	—	`HasFiniteMulSupport` `Pi.instOne`	—	`mulSupport_one`
`hasFiniteSupport_fun_zero` 📖	mathematical	—	`HasFiniteSupport` `Pi.instZero`	—	`support_zero` `Set.finite_empty`

Function.HasFiniteMulSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	—	`Function.HasFiniteMulSupport`	—	`Set.Finite.subset` `Function.mulSupport_comp_subset`
`comp_of_injective` 📖	mathematical	—	`Function.HasFiniteMulSupport`	—	`Set.Finite.of_injOn` `Set.injOn_of_injective`
`div` 📖	mathematical	—	`Function.HasFiniteMulSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Pi.instDiv` `DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid`	—	`Set.Finite.subset` `Set.Finite.union` `Function.mulSupport_div`
`fst` 📖	mathematical	—	`Function.HasFiniteMulSupport`	—	`comp`
`fun_comp` 📖	mathematical	—	`Function.HasFiniteMulSupport`	—	`Set.Finite.subset` `Function.mulSupport_comp_subset`
`fun_comp_of_injective` 📖	mathematical	—	`Function.HasFiniteMulSupport`	—	`comp_of_injective`
`fun_div` 📖	mathematical	—	`Function.HasFiniteMulSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivInvMonoid.toDiv` `DivisionMonoid.toDivInvMonoid`	—	`div`
`fun_inv` 📖	mathematical	—	`Function.HasFiniteMulSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `InvOneClass.toInv`	—	`inv`
`fun_mul` 📖	mathematical	—	`Function.HasFiniteMulSupport` `MulOne.toOne` `MulOneClass.toMulOne` `MulOne.toMul`	—	`mul`
`fun_pow` 📖	mathematical	—	`Function.HasFiniteMulSupport` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Monoid.toPow`	—	`pow`
`fun_zpow` 📖	mathematical	—	`Function.HasFiniteMulSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivInvMonoid.toZPow` `DivisionMonoid.toDivInvMonoid`	—	`zpow`
`iInf` 📖	mathematical	`Function.HasFiniteMulSupport`	`Function.HasFiniteMulSupport` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`Set.Finite.subset` `Set.finite_iUnion` `Function.mulSupport_iInf`
`iSup` 📖	mathematical	`Function.HasFiniteMulSupport`	`Function.HasFiniteMulSupport` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`Set.Finite.subset` `Set.finite_iUnion` `Function.mulSupport_iSup`
`inf` 📖	mathematical	—	`Function.HasFiniteMulSupport` `SemilatticeInf.toMin`	—	`Set.Finite.subset` `Set.Finite.union` `Function.mulSupport_inf`
`inf'` 📖	mathematical	`Function.HasFiniteMulSupport` `Finset.Nonempty`	`Function.HasFiniteMulSupport` `Finset.inf'`	—	`Set.Finite.subset` `Set.Finite.biUnion` `Finset.finite_toSet` `Set.iUnion_congr_Prop` `Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `Finset.inf'_eq_of_forall`
`inv` 📖	mathematical	—	`Function.HasFiniteMulSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Pi.instInv` `InvOneClass.toInv`	—	`comp` `inv_one`
`max` 📖	mathematical	—	`Function.HasFiniteMulSupport` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.Finite.subset` `Set.Finite.union` `Function.mulSupport_max`
`min` 📖	mathematical	—	`Function.HasFiniteMulSupport` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.Finite.subset` `Set.Finite.union` `Function.mulSupport_min`
`mul` 📖	mathematical	—	`Function.HasFiniteMulSupport` `MulOne.toOne` `MulOneClass.toMulOne` `Pi.instMul` `MulOne.toMul`	—	`Set.Finite.subset` `Set.Finite.union` `Function.mulSupport_mul`
`of_comp` 📖	mathematical	—	`Function.HasFiniteMulSupport`	—	`Set.Finite.subset` `Set.mem_setOf`
`pi` 📖	mathematical	`Function.HasFiniteMulSupport`	`Function.HasFiniteMulSupport` `Pi.instOne`	—	`Set.Finite.subset` `Set.finite_iUnion` `Function.ne_iff`
`pow` 📖	mathematical	—	`Function.HasFiniteMulSupport` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Pi.instPow` `Monoid.toPow`	—	`comp` `one_pow`
`prod` 📖	mathematical	`Function.HasFiniteMulSupport` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	`Function.HasFiniteMulSupport` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Finset.prod`	—	`Set.Finite.subset` `Set.Finite.biUnion` `Finset.finite_toSet` `Finset.mulSupport_prod`
`prodMk` 📖	mathematical	—	`Function.HasFiniteMulSupport` `Prod.instOne`	—	`Function.mulSupport_prodMk` `Set.Finite.union`
`snd` 📖	mathematical	—	`Function.HasFiniteMulSupport`	—	`comp`
`sup` 📖	mathematical	—	`Function.HasFiniteMulSupport` `SemilatticeSup.toMax`	—	`Set.Finite.subset` `Set.Finite.union` `Function.mulSupport_sup`
`sup'` 📖	mathematical	`Function.HasFiniteMulSupport` `Finset.Nonempty`	`Function.HasFiniteMulSupport` `Finset.sup'`	—	`Set.Finite.subset` `Set.Finite.biUnion` `Finset.finite_toSet` `Set.iUnion_congr_Prop` `Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `Finset.sup'_eq_of_forall`
`zpow` 📖	mathematical	—	`Function.HasFiniteMulSupport` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Pi.instPow` `DivInvMonoid.toZPow` `DivisionMonoid.toDivInvMonoid`	—	`comp` `one_zpow`

Function.HasFiniteSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	—	`Function.HasFiniteSupport` `AddZero.toZero` `AddZeroClass.toAddZero` `Pi.instAdd` `AddZero.toAdd`	—	`Set.Finite.subset` `Set.Finite.union` `Function.support_add`
`comp` 📖	mathematical	—	`Function.HasFiniteSupport`	—	`Set.Finite.subset` `Function.support_comp_subset`
`comp_of_injective` 📖	mathematical	—	`Function.HasFiniteSupport`	—	`Set.Finite.of_injOn` `Set.injOn_of_injective`
`fst` 📖	mathematical	—	`Function.HasFiniteSupport`	—	`comp`
`fun_add` 📖	mathematical	—	`Function.HasFiniteSupport` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd`	—	`add`
`fun_comp` 📖	mathematical	—	`Function.HasFiniteSupport`	—	`Set.Finite.subset` `Function.support_comp_subset`
`fun_comp_of_injective` 📖	mathematical	—	`Function.HasFiniteSupport`	—	`comp_of_injective`
`fun_neg` 📖	mathematical	—	`Function.HasFiniteSupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `NegZeroClass.toNeg`	—	`neg`
`fun_nsmul` 📖	mathematical	—	`Function.HasFiniteSupport` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoid.toNSMul`	—	`nsmul`
`fun_sub` 📖	mathematical	—	`Function.HasFiniteSupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid`	—	`sub`
`fun_zsmul` 📖	mathematical	—	`Function.HasFiniteSupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubNegMonoid.toZSMul` `SubtractionMonoid.toSubNegMonoid`	—	`zsmul`
`iInf` 📖	mathematical	`Function.HasFiniteSupport`	`Function.HasFiniteSupport` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`Set.Finite.subset` `Set.finite_iUnion` `Function.support_iInf`
`iSup` 📖	mathematical	`Function.HasFiniteSupport`	`Function.HasFiniteSupport` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`Set.Finite.subset` `Set.finite_iUnion` `Function.support_iSup`
`inf` 📖	mathematical	—	`Function.HasFiniteSupport` `SemilatticeInf.toMin`	—	`Set.Finite.subset` `Set.Finite.union` `Function.support_inf`
`inf'` 📖	mathematical	`Function.HasFiniteSupport` `Finset.Nonempty`	`Function.HasFiniteSupport` `Finset.inf'`	—	`Set.Finite.subset` `Set.Finite.biUnion` `Finset.finite_toSet` `Set.iUnion_congr_Prop` `SetLike.mem_coe` `Set.mem_iUnion` `Function.mem_support` `Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_exists` `Mathlib.Tactic.Push.not_and_eq` `Finset.inf'_eq_of_forall`
`max` 📖	mathematical	—	`Function.HasFiniteSupport` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.Finite.subset` `Set.Finite.union` `Function.support_max`
`min` 📖	mathematical	—	`Function.HasFiniteSupport` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Set.Finite.subset` `Set.Finite.union` `Function.support_min`
`neg` 📖	mathematical	—	`Function.HasFiniteSupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `Pi.instNeg` `NegZeroClass.toNeg`	—	`comp` `neg_zero`
`nsmul` 📖	mathematical	—	`Function.HasFiniteSupport` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Pi.instSMul` `AddMonoid.toNSMul`	—	`comp` `nsmul_zero`
`of_comp` 📖	mathematical	—	`Function.HasFiniteSupport`	—	`Set.Finite.subset` `Set.mem_setOf`
`pi` 📖	mathematical	`Function.HasFiniteSupport`	`Function.HasFiniteSupport` `Pi.instZero`	—	`Set.Finite.subset` `Set.finite_iUnion` `Set.mem_iUnion` `Function.mem_support` `Function.ne_iff`
`snd` 📖	mathematical	—	`Function.HasFiniteSupport`	—	`comp`
`sub` 📖	mathematical	—	`Function.HasFiniteSupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `Pi.instSub` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid`	—	`Set.Finite.subset` `Set.Finite.union` `Function.support_sub`
`sum` 📖	mathematical	`Function.HasFiniteSupport` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	`Function.HasFiniteSupport` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset.sum`	—	`Set.Finite.subset` `Set.Finite.biUnion` `Finset.finite_toSet` `Finset.support_sum`
`sumMk` 📖	mathematical	—	`Function.HasFiniteSupport` `Prod.instZero`	—	`Function.support_prodMk` `Set.Finite.union`
`sup` 📖	mathematical	—	`Function.HasFiniteSupport` `SemilatticeSup.toMax`	—	`Set.Finite.subset` `Set.Finite.union` `Function.support_sup`
`sup'` 📖	mathematical	`Function.HasFiniteSupport` `Finset.Nonempty`	`Function.HasFiniteSupport` `Finset.sup'`	—	`Set.Finite.subset` `Set.Finite.biUnion` `Finset.finite_toSet` `Set.iUnion_congr_Prop` `SetLike.mem_coe` `Set.mem_iUnion` `Function.mem_support` `Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_exists` `Mathlib.Tactic.Push.not_and_eq` `Finset.sup'_eq_of_forall`
`zsmul` 📖	mathematical	—	`Function.HasFiniteSupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `Pi.instSMul` `SubNegMonoid.toZSMul` `SubtractionMonoid.toSubNegMonoid`	—	`comp` `zsmul_zero`

---

← Back to Index