Supported

📁 Source: Mathlib/LinearAlgebra/Finsupp/Supported.lean

Statistics

Metric	Count
Definitions restrictDom, supported, supportedEquivFinsupp	3
Theorems codisjoint_supported_supported, codisjoint_supported_supported_iff, disjoint_supported_supported, disjoint_supported_supported_iff, lmapDomain_disjoint_ker, lmapDomain_supported, mem_supported, mem_supported', mem_supported_support, range_restrictDom, restrictDom_apply, restrictDom_comp_subtype, single_mem_span_single, single_mem_supported, span_le_supported_biUnion_support, supportedEquivFinsupp_apply_apply, supportedEquivFinsupp_apply_support_val, supportedEquivFinsupp_symm_apply_coe, supportedEquivFinsupp_symm_apply_coe_apply, supportedEquivFinsupp_symm_apply_coe_support_val, supportedEquivFinsupp_symm_single, supported_comap_lmapDomain, supported_empty, supported_eq_span_single, supported_iInter, supported_iUnion, supported_inter, supported_mono, supported_union, supported_univ	30
Total	33

Finsupp

Definitions

Name	Category	Theorems
restrictDom 📖	CompOp	3 math math: restrictDom_apply, restrictDom_comp_subtype, range_restrictDom
supported 📖	CompOp	44 math math: mem_supported_support, restrictDom_apply, supportedEquivFinsupp_symm_single, mem_supported, supported_inter, span_le_supported_biUnion_support, span_image_eq_map_linearCombination, supported_eq_span_single, supported_univ, supported_comap_lmapDomain, Module.Basis.repr_range, MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported, codisjoint_supported_supported, supported_union, supported_iInter, linearDepOn_iff, linearIndepOn_iff_disjoint, Submodule.set_smul_eq_map, linearCombinationOn_range, restrictDom_comp_subtype, disjoint_supported_supported, supportedEquivFinsupp_symm_apply_coe_support_val, linearCombination_restrict, supported_empty, codisjoint_supported_supported_iff, supported_mono, MvPolynomial.homogeneousSubmodule_eq_finsupp_supported, supportedEquivFinsupp_symm_apply_coe, supportedEquivFinsupp_apply_support_val, supported_iUnion, linearDepOn_iffₛ, mem_span_image_iff_linearCombination, disjoint_supported_supported_iff, linearDepOn_iff', supportedEquivFinsupp_symm_apply_coe_apply, lmapDomain_disjoint_ker, supportedEquivFinsupp_apply_apply, single_mem_supported, linearDepOn_iff'ₛ, range_restrictDom, linearIndepOn_iff_linearCombinationOnₛ, linearIndepOn_iff_linearCombinationOn, mem_supported', lmapDomain_supported
supportedEquivFinsupp 📖	CompOp	7 math math: supportedEquivFinsupp_symm_single, supportedEquivFinsupp_symm_apply_coe_support_val, linearCombination_restrict, supportedEquivFinsupp_symm_apply_coe, supportedEquivFinsupp_apply_support_val, supportedEquivFinsupp_symm_apply_coe_apply, supportedEquivFinsupp_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
codisjoint_supported_supported 📖	mathematical	Codisjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instOrderTop	Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Submodule.instPartialOrder Submodule.instOrderTop supported	—	codisjoint_iff eq_top_iff supported_union supported_univ le_refl
codisjoint_supported_supported_iff 📖	mathematical	—	Codisjoint Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Submodule.instPartialOrder Submodule.instOrderTop supported Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instOrderTop	—	codisjoint_iff eq_top_iff exists_ne support_single_ne_zero Finset.coe_singleton Submodule.eq_top_iff' supported_union codisjoint_supported_supported
disjoint_supported_supported 📖	mathematical	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Submodule.instPartialOrder Submodule.instOrderBot supported	—	disjoint_iff supported_inter Set.disjoint_iff_inter_eq_empty supported_empty
disjoint_supported_supported_iff 📖	mathematical	—	Disjoint Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Submodule.instPartialOrder Submodule.instOrderBot supported Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	Set.disjoint_left exists_ne Disjoint.le_bot single_mem_supported single_eq_zero Submodule.mem_bot disjoint_supported_supported
lmapDomain_disjoint_ker 📖	mathematical	—	Disjoint Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Submodule.instPartialOrder Submodule.instOrderBot supported LinearMap.ker RingHom.id Semiring.toNonAssocSemiring lmapDomain	—	disjoint_iff_inf_le ext mapDomain.eq_1 lmapDomain_apply LinearMap.mem_ker SetLike.mem_coe single_eq_same sum_eq_single single_eq_of_ne' single_zero sum_apply mem_support_iff
lmapDomain_supported 📖	mathematical	—	Submodule.map Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids lmapDomain supported Set.image	—	isEmpty_or_nonempty RingHomSurjective.ids Submodule.map.congr_simp Set.eq_empty_of_isEmpty instIsEmptySubtype supported_empty Submodule.map_bot Set.image_empty le_antisymm Submodule.map_le_iff_le_comap le_trans supported_mono Set.subset_preimage_image supported_comap_lmapDomain Finset.mem_image mapDomain_support Function.invFunOn_mem RingHomCompTriple.ids LinearMap.comp_apply lmapDomain_comp mapDomain_congr Function.invFunOn_eq mapDomain_id
mem_supported 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule instAddCommMonoid module SetLike.instMembership Submodule.setLike supported Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike support	—	—
mem_supported' 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule instAddCommMonoid module SetLike.instMembership Submodule.setLike supported DFunLike.coe instFunLike	—	—
mem_supported_support 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule instAddCommMonoid module SetLike.instMembership Submodule.setLike supported SetLike.coe Finset Finset.instSetLike support	—	mem_supported subset_refl Set.instReflSubset
range_restrictDom 📖	mathematical	—	LinearMap.range Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule instAddCommMonoid module SetLike.instMembership Submodule.setLike supported Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids restrictDom Top.top Submodule.instTop	—	RingHomSurjective.ids LinearMap.range_eq_top LinearMap.congr_fun RingHomCompTriple.ids restrictDom_comp_subtype
restrictDom_apply 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule instAddCommMonoid module SetLike.instMembership Submodule.setLike supported DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Submodule.addCommMonoid Submodule.module LinearMap.instFunLike restrictDom filter Set Set.instMembership	—	—
restrictDom_comp_subtype 📖	mathematical	—	LinearMap.comp Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule instAddCommMonoid module SetLike.instMembership Submodule.setLike supported Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids restrictDom Submodule.subtype LinearMap.id	—	LinearMap.ext RingHomCompTriple.ids ext filter_apply_pos filter_apply_neg mem_supported'
single_mem_span_single 📖	mathematical	—	Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid module Semiring.toModule SetLike.instMembership Submodule.setLike Submodule.span Set.image single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Set Set.instMembership	—	Finset.coe_singleton support_single_ne_zero one_ne_zero' NeZero.one mem_supported supported_eq_span_single Submodule.subset_span Set.mem_image_of_mem
single_mem_supported 📖	mathematical	Set Set.instMembership	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule instAddCommMonoid module SetLike.instMembership Submodule.setLike supported single	—	Set.Subset.trans support_single_subset Finset.singleton_subset_set_iff
span_le_supported_biUnion_support 📖	mathematical	—	Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.span supported Set.iUnion Set Set.instMembership SetLike.coe Finset Finset.instSetLike support	—	Submodule.span_le Set.subset_biUnion_of_mem
supportedEquivFinsupp_apply_apply 📖	mathematical	—	DFunLike.coe Finsupp Set.Elem AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Submodule instAddCommMonoid module SetLike.instMembership Submodule.setLike supported Submodule.addCommMonoid Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike supportedEquivFinsupp Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike support Set.instMembership	—	RingHomInvPair.ids
supportedEquivFinsupp_apply_support_val 📖	mathematical	—	Finset.val Set Set.instMembership support Set.Elem AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp Submodule instAddCommMonoid module SetLike.instMembership Submodule.setLike supported Submodule.addCommMonoid Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike supportedEquivFinsupp Multiset.map Finset Finset.instMembership Finset.filter Classical.decPred Set.instHasSubset SetLike.coe Finset.instSetLike Multiset.attach Multiset.filter	—	RingHomInvPair.ids
supportedEquivFinsupp_symm_apply_coe 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule instAddCommMonoid module SetLike.instMembership Submodule.setLike supported DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Set.Elem Submodule.addCommMonoid Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm supportedEquivFinsupp extendDomain Set Set.instMembership	—	RingHomInvPair.ids restrictSupportEquiv_symm_apply_coe
supportedEquivFinsupp_symm_apply_coe_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike Submodule instAddCommMonoid module SetLike.instMembership Submodule.setLike supported LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Set.Elem Submodule.addCommMonoid Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm supportedEquivFinsupp Set Set.instMembership Classical.decPred	—	RingHomInvPair.ids
supportedEquivFinsupp_symm_apply_coe_support_val 📖	mathematical	—	Finset.val support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp Submodule instAddCommMonoid module SetLike.instMembership Submodule.setLike supported DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Set.Elem Submodule.addCommMonoid Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm supportedEquivFinsupp Multiset.map Set Set.instMembership	—	Multiset.add_zero
supportedEquivFinsupp_symm_single 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule instAddCommMonoid module SetLike.instMembership Submodule.setLike supported DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Set.Elem Submodule.addCommMonoid Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm supportedEquivFinsupp single Set Set.instMembership	—	RingHomInvPair.ids supportedEquivFinsupp_symm_apply_coe extendDomain_single
supported_comap_lmapDomain 📖	mathematical	—	Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder supported Set.preimage Submodule.comap RingHom.id Semiring.toNonAssocSemiring lmapDomain	—	Set.Subset.trans mapDomain_support Finset.coe_image Set.image_subset_iff
supported_empty 📖	mathematical	—	supported Set Set.instEmptyCollection Bot.bot Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Submodule.instBot	—	eq_bot_iff Submodule.mem_bot ext
supported_eq_span_single 📖	mathematical	—	supported NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.span Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Set.image single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Submodule.span_eq_of_le single_mem_supported SetLike.le_def instIsConcreteLE sum_single sum_mem Submodule.addSubmonoidClass smul_single mul_one Submodule.smul_mem Submodule.subset_span Set.mem_image_of_mem
supported_iInter 📖	mathematical	—	supported Set.iInter iInf Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Submodule.instInfSet	—	Submodule.ext
supported_iUnion 📖	mathematical	—	supported Set.iUnion iSup Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	—	le_antisymm RingHomSurjective.ids RingHomCompTriple.ids LinearMap.range_le_iff_comap eq_top_iff induction ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass filter_single_of_pos le_iSup single_mem_supported filter_single_of_neg Submodule.range_subtype Submodule.map_top range_restrictDom LinearMap.range_comp iSup_le supported_mono Set.subset_iUnion
supported_inter 📖	mathematical	—	supported Set Set.instInter Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Submodule.instMin	—	Set.inter_eq_iInter supported_iInter iInf_bool_eq
supported_mono 📖	mathematical	Set Set.instHasSubset	Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder supported	—	Set.Subset.trans
supported_union 📖	mathematical	—	supported Set Set.instUnion Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	—	Set.union_eq_iUnion supported_iUnion iSup_bool_eq
supported_univ 📖	mathematical	—	supported Set.univ Top.top Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Submodule.instTop	—	eq_top_iff Set.subset_univ

---

← Back to Index