Span

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

Statistics

Metric	Count
Definitions	0
Theorems disjoint_lsingle_lsingle, iInf_ker_lapply_le_bot, iSup_lsingle_range, ker_lsingle, lsingle_range_le_ker_lapply, range_lmapDomain, span_single_image, exists_finset_of_mem_iSup, mem_iSup_iff_exists_finset, mem_sSup_iff_exists_finset	10
Total	10

Finsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_lsingle_lsingle 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder 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 iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set.instMembership LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids lsingle	—	Disjoint.mono RingHomSurjective.ids lsingle_range_le_ker_lapply disjoint_compl_right disjoint_iff_inf_le le_trans le_iInf Disjoint.le_bot inf_le_of_right_le iInf_le_of_le iInf_le inf_le_of_left_le iInf_ker_lapply_le_bot
iInf_ker_lapply_le_bot 📖	mathematical	—	Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder iInf Submodule.instInfSet LinearMap.ker RingHom.id Semiring.toNonAssocSemiring lapply Bot.bot Submodule.instBot	—	instIsConcreteLE ext
iSup_lsingle_range 📖	mathematical	—	iSup Submodule Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids lsingle Top.top Submodule.instTop	—	RingHomSurjective.ids eq_top_iff SetLike.le_def instIsConcreteLE sum_single sum_mem Submodule.addSubmonoidClass Submodule.mem_iSup_of_mem
ker_lsingle 📖	mathematical	—	LinearMap.ker Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module RingHom.id Semiring.toNonAssocSemiring lsingle Bot.bot Submodule Submodule.instBot	—	LinearMap.ker_eq_bot_of_injective single_injective
lsingle_range_le_ker_lapply 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder 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 Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set.instMembership LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids lsingle iInf Submodule.instInfSet LinearMap.ker lapply	—	iSup_le RingHomSurjective.ids LinearMap.range_le_iff_comap RingHomCompTriple.ids Submodule.comap_iInf iInf_congr_Prop LinearMap.ker_comp instIsConcreteLE Disjoint.le_bot single_eq_of_ne
range_lmapDomain 📖	mathematical	—	LinearMap.range Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instAddCommMonoid module Semiring.toModule RingHom.id RingHomSurjective.ids lmapDomain Submodule.span Set.range single AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	le_antisymm RingHomSurjective.ids induction_linear mapDomain_zero AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass Submodule.add_mem lmapDomain_apply mapDomain_single smul_single_one Submodule.smul_mem Submodule.subset_span Submodule.span_le Set.range_subset_iff
span_single_image 📖	mathematical	—	Submodule.span Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module Set.image single Submodule.map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids lsingle	—	RingHomSurjective.ids Submodule.span_image

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finset_of_mem_iSup 📖	mathematical	Submodule SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	Finset Finset.instMembership	—	CompleteLattice.IsCompactElement.exists_finset_of_le_iSup singleton_span_isCompactElement
mem_iSup_iff_exists_finset 📖	mathematical	—	Submodule SetLike.instMembership setLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice Finset Finset.instMembership	—	exists_finset_of_mem_iSup iSup_mono iSup_const_le
mem_sSup_iff_exists_finset 📖	mathematical	—	Submodule SetLike.instMembership setLike SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike iSup Finset.instMembership	—	sSup_eq_iSup iSup_subtype' mem_iSup_iff_exists_finset Finset.coe_map Set.image_congr iSup_congr_Prop iSup_exists Function.Injective.injOn Subtype.coe_injective iSup_subtype iSup_and'

---

← Back to Index