Sum

📁 Source: Mathlib/Combinatorics/Matroid/Sum.lean

Statistics

Metric	Count
Definitions `disjointSigma`, `disjointSum`, `sigma`, `sum`, `sum'`	5
Theorems `sigma`, `sum'`, `eq_union_image_of_disjointSum`, `eq_union_image_of_disjointSum`, `disjointSigma_ground_eq`, `disjointSigma_indep_iff`, `disjointSigma_isBase_iff`, `disjointSigma_isBasis_iff`, `disjointSum_comm`, `disjointSum_ground_eq`, `disjointSum_indep_iff`, `disjointSum_isBase_iff`, `disjointSum_isBasis_iff`, `sigma_ground_eq`, `sigma_indep_iff`, `sigma_isBase_iff`, `sigma_isBasis_iff`, `sum'_ground_eq`, `sum'_indep_iff`, `sum'_isBase_iff`, `sum'_isBasis_iff`, `sum_ground`, `sum_indep_iff`, `sum_isBase_iff`, `sum_isBasis_iff`	25
Total	30

Matroid

Definitions

Name	Category	Theorems
`disjointSigma` 📖	CompOp	4 math math: `disjointSigma_indep_iff`, `disjointSigma_isBasis_iff`, `disjointSigma_isBase_iff`, `disjointSigma_ground_eq`
`disjointSum` 📖	CompOp	5 math math: `disjointSum_comm`, `disjointSum_isBase_iff`, `disjointSum_isBasis_iff`, `disjointSum_ground_eq`, `disjointSum_indep_iff`
`sigma` 📖	CompOp	5 math math: `sigma_isBasis_iff`, `sigma_ground_eq`, `sigma_isBase_iff`, `sigma_indep_iff`, `Finitary.sigma`
`sum` 📖	CompOp	4 math math: `sum_isBase_iff`, `sum_indep_iff`, `sum_isBasis_iff`, `sum_ground`
`sum'` 📖	CompOp	5 math math: `sum'_indep_iff`, `sum'_ground_eq`, `Finitary.sum'`, `sum'_isBasis_iff`, `sum'_isBase_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjointSigma_ground_eq` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `E`	`disjointSigma` `Set.iUnion`	—	`Set.ext` `restrict_ground_eq_self` `map.congr_simp` `Set.image_congr` `Subtype.coe_preimage_self` `Set.sigma_univ` `Set.image_univ`
`disjointSigma_indep_iff` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `E`	`Indep` `disjointSigma` `Set.instInter` `Set.instHasSubset` `Set.iUnion`	—	`Function.Embedding.sigmaSet_preimage` `Function.Embedding.sigmaSet_range`
`disjointSigma_isBase_iff` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `E`	`IsBase` `disjointSigma` `Set.instInter` `Set.instHasSubset` `Set.iUnion`	—	`Function.Embedding.sigmaSet_preimage` `Function.Embedding.sigmaSet_range`
`disjointSigma_isBasis_iff` 📖	mathematical	`Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `E`	`IsBasis` `disjointSigma` `Set.instInter` `Set.instHasSubset` `Set.iUnion`	—	`Function.Embedding.sigmaSet_preimage` `Function.Embedding.sigmaSet_range`
`disjointSum_comm` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `E`	`disjointSum` `Disjoint.symm`	—	`ext_indep` `Disjoint.symm` `Set.ext` `disjointSum_ground_eq` `Set.union_comm`
`disjointSum_ground_eq` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `E`	`disjointSum` `Set.instUnion`	—	`restrict_ground_eq_self` `map.congr_simp` `Set.image_congr` `sum_ground` `Subtype.coe_preimage_self` `Set.image_univ` `Set.range_inl_union_range_inr` `Set.Sum.elim_range` `Subtype.range_coe_subtype`
`disjointSum_indep_iff` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `E`	`Indep` `disjointSum` `Set.instInter` `Set.instHasSubset` `Set.instUnion`	—	`Function.Embedding.sumSet_preimage_inl` `Function.Embedding.sumSet_preimage_inr` `Function.Embedding.sumSet_range`
`disjointSum_isBase_iff` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `E`	`IsBase` `disjointSum` `Set.instInter` `Set.instHasSubset` `Set.instUnion`	—	`Function.Embedding.sumSet_preimage_inl` `Function.Embedding.sumSet_preimage_inr` `Function.Embedding.sumSet_range`
`disjointSum_isBasis_iff` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `E`	`IsBasis` `disjointSum` `Set.instInter` `Set.instHasSubset` `Set.instUnion`	—	`Function.Embedding.sumSet_preimage_inl` `Function.Embedding.sumSet_preimage_inr` `Function.Embedding.sumSet_range`
`sigma_ground_eq` 📖	mathematical	—	`E` `sigma` `Set.sigma` `Set.univ`	—	—
`sigma_indep_iff` 📖	mathematical	—	`Indep` `sigma` `Set.preimage`	—	—
`sigma_isBase_iff` 📖	mathematical	—	`IsBase` `sigma` `Set.preimage`	—	—
`sigma_isBasis_iff` 📖	mathematical	—	`IsBasis` `sigma` `Set.preimage`	—	`Set.preimage_mono` `HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `eq_or_ne` `sigma_mk_preimage_image_eq_self` `Set.union_eq_self_of_subset_left` `sigma_mk_preimage_image'` `Set.union_empty` `Set.preimage_union` `Set.subset_union_right` `Set.mk_preimage_sigma` `Eq.subset` `Set.instReflSubset`
`sum'_ground_eq` 📖	mathematical	—	`E` `sum'` `Set.iUnion` `Set.image`	—	`Set.ext` `Set.image_congr`
`sum'_indep_iff` 📖	mathematical	—	`Indep` `sum'` `Set.preimage`	—	`Set.image_congr` `Set.ext`
`sum'_isBase_iff` 📖	mathematical	—	`IsBase` `sum'` `Set.preimage`	—	`Set.image_congr` `Set.ext`
`sum'_isBasis_iff` 📖	mathematical	—	`IsBasis` `sum'` `Set.preimage`	—	`Set.image_congr` `Set.ext`
`sum_ground` 📖	mathematical	—	`E` `sum` `Set` `Set.instUnion` `Set.image`	—	`Set.image_congr` `Bool.univ_eq`
`sum_indep_iff` 📖	mathematical	—	`Indep` `sum` `Set.preimage`	—	`Set.image_congr`
`sum_isBase_iff` 📖	mathematical	—	`IsBase` `sum` `Set.preimage`	—	`Set.image_congr`
`sum_isBasis_iff` 📖	mathematical	—	`IsBasis` `sum` `Set.preimage`	—	`Set.image_congr` `Set.ext`

Matroid.Finitary

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sigma` 📖	mathematical	`Matroid.Finitary`	`Matroid.sigma`	—	`Matroid.indep_of_forall_finite_subset_indep` `sigma_mk_preimage_image_eq_self` `Set.Finite.image`
`sum'` 📖	mathematical	`Matroid.Finitary`	`Matroid.sum'`	—	`sigma` `Matroid.sum'.eq_1` `Matroid.instFinitaryMapEquiv`

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_union_image_of_disjointSum` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Matroid.E` `Matroid.Indep` `Matroid.disjointSum`	`Set.instUnion`	—	`Matroid.disjointSum_indep_iff` `Disjoint.mono` `Set.inter_subset_right` `Set.inter_union_distrib_left` `Set.inter_eq_self_of_subset_left`

Matroid.IsBase

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_union_image_of_disjointSum` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Matroid.E` `Matroid.IsBase` `Matroid.disjointSum`	`Set.instUnion`	—	`Matroid.disjointSum_isBase_iff` `Disjoint.mono` `Set.inter_subset_right` `Set.inter_union_distrib_left` `Set.inter_eq_self_of_subset_left`

---

← Back to Index