Preimage

📁 Source: Mathlib/Data/Finset/Preimage.lean

Statistics

Metric	Count
Definitions `restrictPreimageFinset`, `preimage`, `Preimage`	3
Theorems `restrictPreimageFinset_apply_coe`, `restrictPreimageFinset_symm_apply_coe`, `card_preimage`, `coe_preimage`, `image_preimage`, `image_preimage_of_bij`, `image_subset_iff_subset_preimage`, `map_subset_iff_subset_preimage`, `mem_preimage`, `monotone_preimage`, `preimage_compl`, `preimage_compl'`, `preimage_empty`, `preimage_inl`, `preimage_inr`, `preimage_inter`, `preimage_map`, `preimage_subset`, `preimage_subset_of_subset_image`, `preimage_union`, `preimage_univ`, `restrict_comp_piCongrLeft`, `sigma_image_fst_preimage_mk`, `sigma_preimage_mk`, `sigma_preimage_mk_of_subset`, `subset_map_iff`	26
Total	29

Equiv

Definitions

Name	Category	Theorems
`restrictPreimageFinset` 📖	CompOp	3 math math: `restrictPreimageFinset_symm_apply_coe`, `restrictPreimageFinset_apply_coe`, `Finset.restrict_comp_piCongrLeft`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrictPreimageFinset_apply_coe` 📖	mathematical	—	`Finset` `SetLike.instMembership` `Finset.instSetLike` `DFunLike.coe` `Equiv` `Finset.preimage` `EquivLike.toFunLike` `instEquivLike` `Function.Injective.injOn` `injective` `Set.preimage` `SetLike.coe` `restrictPreimageFinset`	—	`Function.Injective.injOn` `injective`
`restrictPreimageFinset_symm_apply_coe` 📖	mathematical	—	`Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.preimage` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike` `Function.Injective.injOn` `injective` `Set.preimage` `SetLike.coe` `symm` `restrictPreimageFinset`	—	`Function.Injective.injOn` `injective`

Finset

Definitions

Name	Category	Theorems
`preimage` 📖	CompOp	61 math math: `preimage_add_left_singleton`, `preimage_mul_left_one`, `sigma_image_fst_preimage_mk`, `Equiv.restrictPreimageFinset_symm_apply_coe`, `preimage_inr`, `prod_preimage_of_bij`, `preimage_mul_left_singleton`, `image_mul_left'`, `preimage_add_left_zero`, `image_add_right`, `preimage_mul_right_one'`, `sum_preimage_of_bij`, `prod_preimage`, `preimage_empty`, `card_preimage`, `UniqueAdd.addHom_preimage`, `image_add_right'`, `sum_preimage'`, `SummationFilter.comap_filter`, `preimage_compl`, `sum_preimage`, `preimage_mul_right_one`, `UniqueMul.mulHom_preimage`, `image_subset_iff_subset_preimage`, `coe_preimage`, `Filter.tendsto_finset_preimage_atTop_atTop`, `mem_preimage`, `preimage_neg`, `image_preimage`, `preimage_add_right_singleton`, `preimage_union`, `preimage_subset`, `image_preimage_of_bij`, `AddMonoidAlgebra.support_divOf`, `preimage_inv`, `sigma_preimage_mk`, `preimage_mul_left_one'`, `Equiv.restrictPreimageFinset_apply_coe`, `image_add_left'`, `MvPolynomial.support_divMonomial`, `sigma_preimage_mk_of_subset`, `preimage_subset_of_subset_image`, `map_subset_iff_subset_preimage`, `preimage_compl'`, `preimage_map`, `preimage_univ`, `preimage_add_left_zero'`, `restrict_comp_piCongrLeft`, `preimage_add_right_zero`, `Finsupp.comapDomain_support`, `Finsupp.linearCombination_comapDomain`, `preimage_mul_right_singleton`, `image_mul_right'`, `monotone_preimage`, `image_add_left`, `preimage_add_right_zero'`, `preimage_inl`, `image_mul_left`, `preimage_inter`, `image_mul_right`, `prod_preimage'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_preimage` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike`	`card` `preimage` `filter` `Set` `Set.instMembership` `Set.range`	—	`card_nbij` `coe_preimage` `coe_filter`
`coe_preimage` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike`	`preimage`	—	`Set.Finite.coe_toFinset`
`image_preimage` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike`	`image` `preimage` `filter` `Set` `Set.instMembership` `Set.range`	—	`coe_image` `coe_preimage` `Set.image_preimage_eq_inter_range` `coe_filter`
`image_preimage_of_bij` 📖	mathematical	`Set.BijOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike`	`image` `preimage` `Set.BijOn.injOn`	—	`Set.BijOn.injOn` `coe_image` `coe_preimage` `Set.BijOn.image_eq`
`image_subset_iff_subset_preimage` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike`	`instHasSubset` `image` `preimage`	—	`image_subset_iff`
`map_subset_iff_subset_preimage` 📖	mathematical	—	`Finset` `instHasSubset` `map` `preimage` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Function.Injective.injOn` `Function.Embedding.injective` `Set.preimage` `SetLike.coe` `instSetLike`	—	`Function.Injective.injOn` `Function.Embedding.injective` `map_eq_image` `image_subset_iff_subset_preimage`
`mem_preimage` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike`	`instMembership` `preimage`	—	`Set.Finite.mem_toFinset`
`monotone_preimage` 📖	mathematical	—	`Monotone` `Finset` `PartialOrder.toPreorder` `partialOrder` `preimage` `Function.Injective.injOn` `Set.preimage` `SetLike.coe` `instSetLike`	—	`Function.Injective.injOn` `mem_preimage`
`preimage_compl` 📖	mathematical	—	`preimage` `Compl.compl` `Finset` `BooleanAlgebra.toCompl` `booleanAlgebra` `Function.Injective.injOn` `Set.preimage` `SetLike.coe` `instSetLike`	—	`preimage_compl'` `Function.Injective.injOn`
`preimage_compl'` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike` `Compl.compl` `BooleanAlgebra.toCompl` `booleanAlgebra`	`preimage`	—	`coe_injective` `coe_preimage` `coe_compl`
`preimage_empty` 📖	mathematical	—	`preimage` `Finset` `instEmptyCollection`	—	`coe_injective` `coe_preimage` `coe_empty`
`preimage_inl` 📖	mathematical	—	`preimage` `Function.Injective.injOn` `Sum.inl_injective` `Set.preimage` `SetLike.coe` `Finset` `instSetLike` `toLeft`	—	`ext` `Function.Injective.injOn` `Sum.inl_injective`
`preimage_inr` 📖	mathematical	—	`preimage` `Function.Injective.injOn` `Sum.inr_injective` `Set.preimage` `SetLike.coe` `Finset` `instSetLike` `toRight`	—	`ext` `Function.Injective.injOn` `Sum.inr_injective`
`preimage_inter` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike`	`preimage` `instInter` `mem_of_mem_inter_left`	—	`coe_injective` `mem_of_mem_inter_left` `coe_preimage` `coe_inter`
`preimage_map` 📖	mathematical	—	`preimage` `map` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Function.Injective.injOn` `Function.Embedding.injective` `Set.preimage` `SetLike.coe` `Finset` `instSetLike`	—	`coe_injective` `Function.Injective.injOn` `Function.Embedding.injective` `coe_preimage` `coe_map` `Set.preimage_image_eq`
`preimage_subset` 📖	mathematical	`Finset` `instHasSubset` `map`	`preimage` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Function.Injective.injOn` `Function.Embedding.injective` `Set.preimage` `SetLike.coe` `instSetLike`	—	`Function.Injective.injOn` `Function.Embedding.injective` `mem_map'` `mem_preimage`
`preimage_subset_of_subset_image` 📖	mathematical	`Finset` `instHasSubset` `image` `Set.InjOn` `Set.preimage` `SetLike.coe` `instSetLike`	`preimage`	—	`coe_subset` `coe_preimage` `Set.preimage_subset` `instIsConcreteLE`
`preimage_union` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike` `instUnion`	`preimage` `mem_union_left` `mem_union_right`	—	`coe_injective` `mem_union_left` `mem_union_right` `coe_preimage` `coe_union`
`preimage_univ` 📖	mathematical	`Set.InjOn` `Set.preimage` `SetLike.coe` `Finset` `instSetLike` `univ`	`preimage`	—	`coe_injective` `coe_preimage` `coe_univ`
`restrict_comp_piCongrLeft` 📖	mathematical	—	`restrict` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.piCongrLeft` `Finset` `SetLike.instMembership` `instSetLike` `preimage` `Function.Injective.injOn` `Equiv.injective` `Set.preimage` `SetLike.coe` `Equiv.restrictPreimageFinset`	—	`Function.Injective.injOn` `Equiv.injective` `Equiv.apply_symm_apply` `Equiv.piCongrLeft_apply_eq_cast`
`sigma_image_fst_preimage_mk` 📖	mathematical	—	`sigma` `image` `preimage` `Function.Injective.injOn` `sigma_mk_injective` `Set.preimage` `SetLike.coe` `Finset` `instSetLike`	—	`sigma_preimage_mk_of_subset` `Subset.refl`
`sigma_preimage_mk` 📖	mathematical	—	`sigma` `preimage` `Function.Injective.injOn` `sigma_mk_injective` `Set.preimage` `SetLike.coe` `Finset` `instSetLike` `filter` `instMembership` `decidableMem`	—	`ext` `Function.Injective.injOn` `sigma_mk_injective` `Sigma.eta`
`sigma_preimage_mk_of_subset` 📖	mathematical	`Finset` `instHasSubset` `image`	`sigma` `preimage` `Function.Injective.injOn` `sigma_mk_injective` `Set.preimage` `SetLike.coe` `instSetLike`	—	`Function.Injective.injOn` `sigma_mk_injective` `filter_true_of_mem` `image_subset_iff`
`subset_map_iff` 📖	mathematical	—	`Finset` `instHasSubset` `map`	—	`map_eq_image`

Order

Definitions

Name	Category	Theorems
`Preimage` 📖	MathDef	29 math math: `Ordinal.type_uLift`, `RelEmbedding.preimage_apply`, `Preimage.instAsymm`, `Preimage.instIsEquiv`, `directedOn_image`, `Preimage.instIsStrictOrder`, `Preimage.instIsStrictWeakOrder`, `Preimage.instRefl`, `RelIso.IsWellOrder.preimage`, `Preimage.instIsSymm`, `RelEmbedding.eq_preimage`, `RelHom.preimage_apply`, `Ordinal.type_lift_preimage`, `Preimage.isAntisymm`, `Encodable.instTotalPreimageNatCoeEmbeddingEncode'Le`, `directed_comp`, `Preimage.instIsPreorder`, `Preimage.instIrrefl`, `RelIso.preimage_apply`, `Preimage.antisymm`, `Encodable.instAntisymmPreimageNatCoeEmbeddingEncode'Le`, `RelIso.IsWellOrder.ulift`, `RelIso.preimage_symm_apply`, `Subtype.relEmbedding_apply`, `Preimage.instTotal`, `UniformOnFun.hasBasis_uniformity_of_basis_aux₂`, `Preimage.instIsTrans`, `preimage_equivalence`, `Ordinal.type_preimage`

---

← Back to Index