Map

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

Statistics

Metric	Count
Definitions comap, comapOn, map, mapEmbedding, mapEquiv, mapSetEmbedding, mapSetEquiv, restrictSubtype	8
Theorems exists_bijOn_of_map, exists_eq_image_of_mapSetEmbedding, map, mapEmbedding, map, mapEmbedding, map, mapEmbedding, comapOn_dual_eq_of_bijOn, comapOn_finitary, comapOn_ground_eq, comapOn_indep_iff, comapOn_isBase_iff, comapOn_isBase_iff_of_bijOn, comapOn_isBase_iff_of_surjOn, comapOn_preimage_eq, comapOn_rankFinite, comap_dep_iff, comap_emptyOn, comap_finitary, comap_ground_eq, comap_id, comap_indep_iff, comap_indep_iff_of_injOn, comap_isBase_iff, comap_isBasis'_iff, comap_isBasis_iff, comap_loopyOn, comap_map, comap_rankFinite, eq_of_restrictSubtype_eq, instFinitaryElemRestrictSubtype, instFinitaryMap, instFinitaryMapEmbedding, instFinitaryMapEquiv, instFiniteElemERestrictSubtype, instFiniteMap, instFiniteMapEmbedding, instFiniteMapEquiv, instNonemptyElemERestrictSubtype, instNonemptyMap, instNonemptyMapEmbedding, instNonemptyMapEquiv, instRankFiniteElemRestrictSubtype, instRankFiniteMap, instRankFiniteMapEmbedding, instRankFiniteMapEquiv, instRankPosElemERestrictSubtype, instRankPosMap, instRankPosMapEmbedding, instRankPosMapEquiv, mapEmbedding_ground_eq, mapEmbedding_indep_iff, mapEmbedding_isBase_iff, mapEmbedding_isBasis_iff, mapEquiv_dep_iff, mapEquiv_eq_map, mapEquiv_ground_eq, mapEquiv_indep_iff, mapEquiv_isBase_iff, mapEquiv_isBasis_iff, mapSetEmbedding_ground, mapSetEmbedding_indep_iff, mapSetEmbedding_indep_iff', ground, mapSetEquiv_indep_iff, map_comap, map_dep_iff, map_dual, map_emptyOn, map_freeOn, map_ground, map_id, map_image_indep_iff, map_image_isBase_iff, map_indep_iff, map_isBase_iff, map_isBasis_iff, map_isBasis_iff', map_loopyOn, map_val_restrictSubtype_eq, map_val_restrictSubtype_ground_eq, restrictSubtype_dual, restrictSubtype_dual', restrictSubtype_ground, restrictSubtype_ground_isBase_iff, restrictSubtype_ground_isBasis_iff, restrictSubtype_indep_iff, restrictSubtype_indep_iff_of_subset, restrictSubtype_inter_indep_iff, restrictSubtype_isBase_iff, restrictSubtype_isBasis_iff	92
Total	100

Matroid

Definitions

Name	Category	Theorems
comap 📖	CompOp	23 math math: comap_finitary, comap_isBasis'_iff, comap_loopyOn, cRk_comap_lift, comap_emptyOn, comap_map, comap_indep_iff, comap_rankFinite, comap_closure_eq, comap_indep_iff_of_injOn, comap_isNonloop_iff, comap_isBasis_iff, comap_dep_iff, comap_isLoop_iff, invariantCardinalRank_comap, comap_id, map_comap, eRk_comap, comap_ground_eq, cRk_comap, comap_isBase_iff, comap_loops, comapOn_preimage_eq
comapOn 📖	CompOp	9 math math: comapOn_isBase_iff_of_surjOn, comapOn_indep_iff, comapOn_ground_eq, comapOn_isBase_iff, comapOn_isBase_iff_of_bijOn, comapOn_rankFinite, comapOn_dual_eq_of_bijOn, comapOn_finitary, comapOn_preimage_eq
map 📖	CompOp	35 math math: IsBase.map, eRank_map, map_isLoop_iff, map_ground, Indep.map, map_dep_iff, eRk_map, invariantCardinalRank_map, comap_map, map_image_isBase_iff, map_loopyOn, cRk_map_eq, instRankPosMap, map_freeOn, instNonemptyMap, map_dual, cRk_map_image, map_id, map_val_restrictSubtype_eq, map_closure_eq, map_indep_iff, map_comap, map_isBasis_iff, IsBasis.map, map_loops, cRk_map_image_lift, instFinitaryMap, map_image_indep_iff, instFiniteMap, map_val_restrictSubtype_ground_eq, map_isBase_iff, map_isBasis_iff', mapEquiv_eq_map, instRankFiniteMap, map_emptyOn
mapEmbedding 📖	CompOp	13 math math: instNonemptyMapEmbedding, instFinitaryMapEmbedding, mapEmbedding_isBase_iff, Indep.mapEmbedding, mapEmbedding_ground_eq, mapEmbedding_indep_iff, IsBasis.mapEmbedding, instFiniteMapEmbedding, mapEmbedding_isBasis_iff, instRankPosMapEmbedding, IsBase.mapEmbedding, instRankFiniteMapEmbedding, mapEmbedding_isLoop_iff
mapEquiv 📖	CompOp	11 math math: instRankPosMapEquiv, mapEquiv_dep_iff, instNonemptyMapEquiv, mapEquiv_ground_eq, instRankFiniteMapEquiv, instFinitaryMapEquiv, mapEquiv_indep_iff, mapEquiv_isBasis_iff, mapEquiv_eq_map, mapEquiv_isBase_iff, instFiniteMapEquiv
mapSetEmbedding 📖	CompOp	3 math math: mapSetEmbedding_indep_iff', mapSetEmbedding_indep_iff, mapSetEmbedding_ground
mapSetEquiv 📖	CompOp	2 math math: mapSetEquiv.ground, mapSetEquiv_indep_iff
restrictSubtype 📖	CompOp	17 math math: restrictSubtype_indep_iff, restrictSubtype_isBasis_iff, instRankFiniteElemRestrictSubtype, restrictSubtype_ground, restrictSubtype_dual', instFinitaryElemRestrictSubtype, instFiniteElemERestrictSubtype, restrictSubtype_inter_indep_iff, map_val_restrictSubtype_eq, instRankPosElemERestrictSubtype, restrictSubtype_indep_iff_of_subset, restrictSubtype_ground_isBasis_iff, restrictSubtype_ground_isBase_iff, restrictSubtype_dual, map_val_restrictSubtype_ground_eq, restrictSubtype_isBase_iff, instNonemptyElemERestrictSubtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comapOn_dual_eq_of_bijOn 📖	mathematical	Set.BijOn E	dual comapOn	—	ext_isBase comapOn_isBase_iff_of_bijOn dual_isBase_iff Set.MapsTo.image_subset Set.MapsTo.mono_left Set.BijOn.mapsTo comapOn_ground_eq Set.diff_subset Set.InjOn.image_diff_subset Set.BijOn.injOn Set.BijOn.image_eq
comapOn_finitary 📖	mathematical	—	Finitary comapOn	—	comapOn.eq_1 restrict_finitary comap_finitary
comapOn_ground_eq 📖	mathematical	—	E comapOn	—	—
comapOn_indep_iff 📖	mathematical	—	Indep comapOn Set.image Set.InjOn Set Set.instHasSubset	—	—
comapOn_isBase_iff 📖	mathematical	—	IsBase comapOn IsBasis' Set.image Set.InjOn Set Set.instHasSubset	—	comapOn.eq_1 isBase_restrict_iff' comap_isBasis'_iff
comapOn_isBase_iff_of_bijOn 📖	mathematical	Set.BijOn E	IsBase comapOn Set.image Set Set.instHasSubset	—	IsBase.subset_ground comapOn_ground_eq Set.InjOn.mono Set.BijOn.injOn comapOn_isBase_iff_of_surjOn Set.BijOn.surjOn
comapOn_isBase_iff_of_surjOn 📖	mathematical	Set.SurjOn E	IsBase comapOn Set.image Set.InjOn Set Set.instHasSubset	—	Set.inter_eq_self_of_subset_right
comapOn_preimage_eq 📖	mathematical	—	comapOn Set.preimage E comap	—	comapOn.eq_1 restrict_eq_self_iff
comapOn_rankFinite 📖	mathematical	—	RankFinite comapOn	—	comapOn.eq_1 restrict_rankFinite comap_rankFinite
comap_dep_iff 📖	mathematical	—	Dep comap Set.image Indep Set.InjOn	—	Dep.eq_1 comap_indep_iff comap_ground_eq Set.image_subset_iff Indep.subset_ground
comap_emptyOn 📖	mathematical	—	comap emptyOn	—	—
comap_finitary 📖	mathematical	—	Finitary comap	—	comap_indep_iff indep_iff_forall_finite_subset_indep Set.SurjOn.exists_bijOn_subset Set.surjOn_image Set.BijOn.image_eq HasSubset.Subset.trans Set.instIsTransSubset Set.Finite.of_finite_image Set.BijOn.injOn Set.pair_subset
comap_ground_eq 📖	mathematical	—	E comap Set.preimage	—	—
comap_id 📖	mathematical	—	comap	—	ext_indep Set.image_congr Set.image_id' Function.Injective.injOn
comap_indep_iff 📖	mathematical	—	Indep comap Set.image Set.InjOn	—	—
comap_indep_iff_of_injOn 📖	mathematical	Set.InjOn Set.preimage E	Indep comap Set.image	—	comap_indep_iff Set.InjOn.mono subset_trans Set.instIsTransSubset Set.subset_preimage_image Set.preimage_mono Indep.subset_ground
comap_isBase_iff 📖	mathematical	—	IsBase comap IsBasis Set.image Set.preimage E Set.InjOn Set Set.instHasSubset	—	isBasis_ground_iff comap_isBasis_iff
comap_isBasis'_iff 📖	mathematical	—	IsBasis' comap Set.image Set.InjOn Set Set.instHasSubset	—	Set.image_inter_preimage Set.image_subset_iff Indep.subset_ground IsBasis.indep
comap_isBasis_iff 📖	mathematical	—	IsBasis comap Set.image Set.InjOn Set Set.instHasSubset	—	comap_indep_iff IsBasis.indep Indep.isBasis_of_forall_insert Set.image_mono IsBasis.subset IsBasis.insert_dep Set.image_insert_eq Set.injOn_insert HasSubset.Subset.trans Set.instIsTransSubset Set.insert_subset IsBasis.subset_ground IsBasis.mem_of_insert_indep Set.mem_image_of_mem not_indep_iff
comap_loopyOn 📖	mathematical	—	comap loopyOn Set.preimage	—	eq_loopyOn_iff
comap_map 📖	mathematical	—	comap map Function.Injective.injOn E	—	Function.Injective.injOn Set.preimage_image_eq Set.image_eq_image
comap_rankFinite 📖	mathematical	—	RankFinite comap	—	exists_isBase IsBase.rankFinite_of_finite Set.Finite.of_finite_image Indep.finite IsBasis.indep
eq_of_restrictSubtype_eq 📖	—	E restrictSubtype	—	—	ext_indep restrictSubtype_indep_iff_of_subset
instFinitaryElemRestrictSubtype 📖	mathematical	—	Finitary Set.Elem restrictSubtype	—	restrictSubtype.eq_1 comap_finitary restrict_finitary
instFinitaryMap 📖	mathematical	Set.InjOn E	Finitary map	—	Set.image_mono Indep.subset_ground Eq.subset Set.instReflSubset Set.subset_image_iff indep_of_forall_finite_subset_indep map_image_indep_iff HasSubset.Subset.trans Set.instIsTransSubset Set.Finite.image
instFinitaryMapEmbedding 📖	mathematical	—	Finitary mapEmbedding	—	Function.Injective.injOn Function.Embedding.injective instFinitaryMap
instFinitaryMapEquiv 📖	mathematical	—	Finitary mapEquiv	—	Function.Injective.injOn Equiv.injective instFinitaryMap
instFiniteElemERestrictSubtype 📖	mathematical	—	Finite Set.Elem E restrictSubtype	—	Set.Finite.to_subtype ground_finite Finite.ground_finite finite_of_finite
instFiniteMap 📖	mathematical	Set.InjOn E	Finite map	—	Set.Finite.image ground_finite
instFiniteMapEmbedding 📖	mathematical	—	Finite mapEmbedding	—	Function.Injective.injOn Function.Embedding.injective instFiniteMap
instFiniteMapEquiv 📖	mathematical	—	Finite mapEquiv	—	Function.Injective.injOn Equiv.injective instFiniteMap
instNonemptyElemERestrictSubtype 📖	mathematical	—	Nonempty Set.Elem E restrictSubtype	—	Set.Nonempty.coe_sort ground_nonempty restrictSubtype_ground
instNonemptyMap 📖	mathematical	Set.InjOn E	Nonempty map	—	ground_nonempty
instNonemptyMapEmbedding 📖	mathematical	—	Nonempty mapEmbedding	—	Function.Injective.injOn Function.Embedding.injective instNonemptyMap
instNonemptyMapEquiv 📖	mathematical	—	Nonempty mapEquiv	—	Function.Injective.injOn Equiv.injective instNonemptyMap
instRankFiniteElemRestrictSubtype 📖	mathematical	—	RankFinite Set.Elem restrictSubtype	—	restrictSubtype.eq_1 comap_rankFinite restrict_rankFinite
instRankFiniteMap 📖	mathematical	Set.InjOn E	RankFinite map	—	exists_isBase IsBase.rankFinite_of_finite IsBase.map Set.Finite.image IsBase.finite
instRankFiniteMapEmbedding 📖	mathematical	—	RankFinite mapEmbedding	—	Function.Injective.injOn Function.Embedding.injective instRankFiniteMap
instRankFiniteMapEquiv 📖	mathematical	—	RankFinite mapEquiv	—	Function.Injective.injOn Equiv.injective instRankFiniteMap
instRankPosElemERestrictSubtype 📖	mathematical	—	RankPos Set.Elem E restrictSubtype	—	exists_isBase Function.Injective.injOn Subtype.val_injective map_val_restrictSubtype_eq restrict_ground_eq_self IsBase.map IsBase.rankPos_of_nonempty IsBase.nonempty
instRankPosMap 📖	mathematical	Set.InjOn E	RankPos map	—	exists_isBase IsBase.rankPos_of_nonempty IsBase.map Set.Nonempty.image IsBase.nonempty
instRankPosMapEmbedding 📖	mathematical	—	RankPos mapEmbedding	—	Function.Injective.injOn Function.Embedding.injective instRankPosMap
instRankPosMapEquiv 📖	mathematical	—	RankPos mapEquiv	—	Function.Injective.injOn Equiv.injective instRankPosMap
mapEmbedding_ground_eq 📖	mathematical	—	E mapEmbedding Set.image DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	—	—
mapEmbedding_indep_iff 📖	mathematical	—	Indep mapEmbedding Set.preimage DFunLike.coe Function.Embedding Function.instFunLikeEmbedding Set Set.instHasSubset Set.range	—	mapEmbedding.eq_1 map_indep_iff Set.preimage_image_eq Function.Embedding.injective Set.image_subset_range Set.image_preimage_eq_iff
mapEmbedding_isBase_iff 📖	mathematical	—	IsBase mapEmbedding Set.preimage DFunLike.coe Function.Embedding Function.instFunLikeEmbedding Set Set.instHasSubset Set.range	—	mapEmbedding.eq_1 map_isBase_iff Set.preimage_image_eq Function.Embedding.injective Set.image_subset_range Set.image_preimage_eq_iff
mapEmbedding_isBasis_iff 📖	mathematical	—	IsBasis mapEmbedding Set.preimage DFunLike.coe Function.Embedding Function.instFunLikeEmbedding Set Set.instHasSubset Set.range	—	mapEmbedding.eq_1 map_isBasis_iff' Set.preimage_image_eq Function.Embedding.injective Set.image_mono IsBasis.subset Set.preimage_range Set.subset_range_iff_exists_image_eq Set.subset_image_iff
mapEquiv_dep_iff 📖	mathematical	—	Dep mapEquiv Set.image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	Function.Injective.injOn Equiv.injective mapEquiv_eq_map map_dep_iff Equiv.symm_image_image Equiv.image_symm_image
mapEquiv_eq_map 📖	mathematical	—	mapEquiv map DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Function.Injective.injOn Equiv.injective E	—	—
mapEquiv_ground_eq 📖	mathematical	—	E mapEquiv Set.image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	—
mapEquiv_indep_iff 📖	mathematical	—	Indep mapEquiv Set.image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	Function.Injective.injOn Equiv.injective mapEquiv_eq_map map_indep_iff Equiv.symm_image_image Equiv.image_symm_image
mapEquiv_isBase_iff 📖	mathematical	—	IsBase mapEquiv Set.image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	Function.Injective.injOn Equiv.injective mapEquiv_eq_map map_isBase_iff Equiv.symm_image_image Equiv.image_symm_image
mapEquiv_isBasis_iff 📖	mathematical	—	IsBasis mapEquiv Set.image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	Function.Injective.injOn Equiv.injective mapEquiv_eq_map map_isBasis_iff' Equiv.symm_image_image Equiv.image_symm_image
mapSetEmbedding_ground 📖	mathematical	—	E mapSetEmbedding Set.range Set.Elem DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	—	—
mapSetEmbedding_indep_iff 📖	mathematical	—	Indep mapSetEmbedding Set.image Set Set.instMembership E Set.preimage Set.Elem DFunLike.coe Function.Embedding Function.instFunLikeEmbedding Set.instHasSubset Set.range	—	—
mapSetEmbedding_indep_iff' 📖	mathematical	—	Indep mapSetEmbedding Set.image Set Set.instMembership E Set.Elem DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	—	Set.preimage_image_eq Function.Embedding.injective
mapSetEquiv_indep_iff 📖	mathematical	—	Indep mapSetEquiv Set.image Set Set.instMembership E Set.Elem DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Set.preimage Set.instHasSubset	—	—
map_comap 📖	mathematical	Set Set.instHasSubset E Set.range Set.InjOn Set.preimage	map comap	—	ext_indep Set.InjOn.mono
map_dep_iff 📖	mathematical	Set.InjOn E	Dep map Set.image	—	Set.InjOn.image_eq_image_iff Indep.subset_ground
map_dual 📖	mathematical	Set.InjOn E	dual map	—	ext_isBase Set.InjOn.image_diff_subset map_image_isBase_iff Set.diff_subset dual_isBase_iff
map_emptyOn 📖	mathematical	—	map emptyOn	—	Set.image_empty
map_freeOn 📖	mathematical	Set.InjOn E freeOn	map Set.image	—	map_dual freeOn_dual_eq map.congr_simp map_loopyOn
map_ground 📖	mathematical	Set.InjOn E	map Set.image	—	—
map_id 📖	mathematical	—	map Set.injOn_id E	—	Set.injOn_id Set.image_congr Set.image_id'
map_image_indep_iff 📖	mathematical	Set.InjOn E Set Set.instHasSubset	Indep map Set.image	—	map_indep_iff Set.InjOn.image_eq_image_iff Indep.subset_ground
map_image_isBase_iff 📖	mathematical	Set.InjOn E Set Set.instHasSubset	IsBase map Set.image	—	map_isBase_iff Set.InjOn.image_eq_image_iff IsBase.subset_ground
map_indep_iff 📖	mathematical	Set.InjOn E	Indep map Set.image	—	—
map_isBase_iff 📖	mathematical	Set.InjOn E	IsBase map Set.image	—	isBase_iff_maximal_indep Indep.exists_bijOn_of_map Maximal.prop Indep.isBase_of_maximal Set.InjOn.image_eq_image_iff Indep.subset_ground Set.BijOn.image_eq Maximal.eq_of_subset Indep.map Set.image_mono maximal_subset_iff IsBase.indep IsBase.eq_of_subset_indep Set.InjOn.image_subset_image_iff IsBase.subset_ground
map_isBasis_iff 📖	mathematical	Set.InjOn E Set Set.instHasSubset	IsBasis map Set.image	—	map_indep_iff IsBasis.indep Set.InjOn.image_subset_image_iff IsBasis.subset Indep.isBasis_of_maximal_subset IsBasis.eq_of_subset_indep Indep.map Set.image_mono Eq.subset Set.instReflSubset Set.InjOn.image_eq_image_iff Indep.subset_ground IsBasis.map
map_isBasis_iff' 📖	mathematical	Set.InjOn E	IsBasis map Set.image	—	Set.subset_image_iff Indep.subset_ground IsBasis.indep IsBasis.subset_ground map_isBasis_iff IsBasis.map
map_loopyOn 📖	mathematical	Set.InjOn E loopyOn	map Set.image	—	Set.image_empty
map_val_restrictSubtype_eq 📖	mathematical	—	map Set.Elem restrictSubtype Set Set.instMembership Function.Injective.injOn Subtype.val_injective E restrict	—	Function.Injective.injOn Subtype.val_injective map_comap Subtype.range_coe_subtype Set.instReflSubset
map_val_restrictSubtype_ground_eq 📖	mathematical	—	map Set.Elem E restrictSubtype Set Set.instMembership Function.Injective.injOn Subtype.val_injective	—	Function.Injective.injOn Subtype.val_injective map_val_restrictSubtype_eq restrict_ground_eq_self
restrictSubtype_dual 📖	mathematical	—	dual Set.Elem E restrictSubtype	—	restrictSubtype.eq_1 comapOn_preimage_eq comapOn_dual_eq_of_bijOn restrict_ground_eq_self Subtype.coe_preimage_self Function.Injective.injOn Subtype.val_injective Set.image_univ Subtype.range_coe_subtype Set.instReflSubset dual_ground
restrictSubtype_dual' 📖	mathematical	E	dual Set.Elem restrictSubtype	—	restrictSubtype_dual
restrictSubtype_ground 📖	mathematical	—	E Set.Elem restrictSubtype Set.univ	—	Subtype.coe_preimage_self
restrictSubtype_ground_isBase_iff 📖	mathematical	—	IsBase Set.Elem E restrictSubtype Set.image Set Set.instMembership	—	restrictSubtype_isBase_iff isBasis'_iff_isBasis Set.instReflSubset isBasis_ground_iff
restrictSubtype_ground_isBasis_iff 📖	mathematical	—	IsBasis Set.Elem E restrictSubtype Set.image Set Set.instMembership	—	restrictSubtype_isBasis_iff isBasis'_iff_isBasis Subtype.coe_preimage_self
restrictSubtype_indep_iff 📖	mathematical	—	Indep Set.Elem restrictSubtype Set.image Set Set.instMembership	—	Subtype.coe_preimage_self Function.Injective.injOn Subtype.val_injective
restrictSubtype_indep_iff_of_subset 📖	mathematical	Set Set.instHasSubset	Indep Set.Elem restrictSubtype Set.preimage Set.instMembership	—	restrictSubtype_indep_iff Set.image_preimage_eq_iff Subtype.range_coe_subtype
restrictSubtype_inter_indep_iff 📖	mathematical	—	Indep Set.Elem restrictSubtype Set.preimage Set Set.instMembership Set.instInter	—	Subtype.image_preimage_coe Function.Injective.injOn Subtype.val_injective
restrictSubtype_isBase_iff 📖	mathematical	—	IsBase Set.Elem restrictSubtype IsBasis' Set.image Set Set.instMembership	—	restrictSubtype.eq_1 comap_isBase_iff Subtype.coe_preimage_self Set.image_univ Subtype.range_coe_subtype Set.instReflSubset Function.Injective.injOn Subtype.val_injective
restrictSubtype_isBasis_iff 📖	mathematical	—	IsBasis Set.Elem restrictSubtype IsBasis' Set.image Set Set.instMembership	—	restrictSubtype.eq_1 comap_isBasis_iff Function.Injective.injOn Subtype.val_injective Set.image_subset_image_iff IsBasis.subset isBasis_restrict_iff' isBasis'_iff_isBasis_inter_ground Subtype.coe_preimage_self

Matroid.Indep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_bijOn_of_map 📖	mathematical	Set.InjOn Matroid.E Matroid.Indep Matroid.map	Set.BijOn	—	Set.InjOn.bijOn_image Set.InjOn.mono subset_ground
exists_eq_image_of_mapSetEmbedding 📖	mathematical	Matroid.Indep Matroid.mapSetEmbedding	Set.image Set Set.instMembership Matroid.E Set.Elem DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	—	Set.image_preimage_eq_of_subset
map 📖	mathematical	Matroid.Indep Set.InjOn Matroid.E	Matroid.map Set.image	—	Matroid.map_indep_iff
mapEmbedding 📖	mathematical	Matroid.Indep	Matroid.mapEmbedding Set.image DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	—	Set.preimage_image_eq Function.Embedding.injective Set.preimage_range

Matroid.IsBase

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	Matroid.IsBase Set.InjOn Matroid.E	Matroid.map Set.image	—	Matroid.map_isBase_iff
mapEmbedding 📖	mathematical	Matroid.IsBase	Matroid.mapEmbedding Set.image DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	—	Matroid.mapEmbedding.eq_1 Matroid.map_isBase_iff

Matroid.IsBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	Matroid.IsBasis Set.InjOn Matroid.E	Matroid.map Set.image	—	Matroid.Indep.isBasis_of_forall_insert Matroid.Indep.map indep Set.image_mono subset Set.insert_subset subset_ground Matroid.Indep.subset_ground Matroid.not_indep_iff Set.mem_image_of_mem mem_of_insert_indep Set.InjOn.image_eq_image_iff Set.image_insert_eq
mapEmbedding 📖	mathematical	Matroid.IsBasis	Matroid.mapEmbedding Set.image DFunLike.coe Function.Embedding Function.instFunLikeEmbedding	—	map

Matroid.mapSetEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ground 📖	mathematical	—	Matroid.E Matroid.mapSetEquiv	—	—

---

← Back to Index