Subset

📁 Source: Mathlib/Data/Set/Subset.lean

Statistics

Metric	Count
Definitions Subset	1
Theorems eq_of_preimage_val_eq_of_subset, image_val_compl, image_val_diff, image_val_iInter, image_val_iUnion, image_val_inj, image_val_injective, image_val_inter, image_val_inter_self_left_eq_coe, image_val_inter_self_right_eq_coe, image_val_mono, image_val_preimage_val_subset_self, image_val_sInter, image_val_sUnion, image_val_union, image_val_union_self_left_eq, image_val_union_self_right_eq, preimage_val_eq_univ_of_subset, preimage_val_iInter, preimage_val_image_val_eq_self, preimage_val_sInter, preimage_val_sInter_eq_sInter, preimage_val_sUnion, subset_of_image_val_subset_image_val, subset_preimage_val_image_val_iff	25
Total	26

Set

Definitions

Name	Category	Theorems
Subset 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_preimage_val_eq_of_subset 📖	—	Set instHasSubset preimage Elem instMembership	—	—	—
image_val_compl 📖	mathematical	—	image Set instMembership Compl.compl Elem instCompl instSDiff	—	compl_eq_univ_diff image_val_diff image_univ Subtype.range_coe_subtype setOf_mem_eq
image_val_diff 📖	mathematical	—	image Set instMembership Elem instSDiff	—	image_diff Subtype.val_injective
image_val_iInter 📖	mathematical	—	image Set instMembership iInter Elem	—	InjOn.image_iInter_eq Function.Injective.injOn Subtype.val_injective
image_val_iUnion 📖	mathematical	—	image Set instMembership iUnion Elem	—	image_iUnion
image_val_inj 📖	mathematical	—	image Set instMembership	—	Function.Injective.image_injective Subtype.val_injective
image_val_injective 📖	mathematical	—	Set instMembership image	—	Function.Injective.image_injective Subtype.val_injective
image_val_inter 📖	mathematical	—	image Set instMembership Elem instInter	—	image_inter Subtype.val_injective
image_val_inter_self_left_eq_coe 📖	mathematical	—	Set instInter image instMembership	—	inter_eq_left image_val_subset
image_val_inter_self_right_eq_coe 📖	mathematical	—	Set instInter image instMembership	—	inter_eq_right image_val_subset
image_val_mono 📖	mathematical	Set Elem instHasSubset	image instMembership	—	image_subset_image_iff Subtype.val_injective
image_val_preimage_val_subset_self 📖	mathematical	—	Set instHasSubset image instMembership preimage Elem	—	image_preimage_subset
image_val_sInter 📖	mathematical	Nonempty Set Elem	image instMembership sInter setOf	—	image.eq_1 sInter_image sInter_eq_biInter InjOn.image_biInter_eq Function.Injective.injOn Subtype.val_injective
image_val_sUnion 📖	mathematical	—	image Set instMembership sUnion Elem setOf	—	image_sUnion image.eq_1
image_val_union 📖	mathematical	—	image Set instMembership Elem instUnion	—	image_union
image_val_union_self_left_eq 📖	mathematical	—	Set instUnion image instMembership	—	union_eq_right image_val_subset
image_val_union_self_right_eq 📖	mathematical	—	Set instUnion image instMembership	—	union_eq_left image_val_subset
preimage_val_eq_univ_of_subset 📖	mathematical	Set instHasSubset	preimage Elem instMembership univ	—	eq_univ_iff_forall
preimage_val_iInter 📖	mathematical	—	preimage Elem Set instMembership iInter	—	preimage_iInter
preimage_val_image_val_eq_self 📖	mathematical	—	preimage Elem Set instMembership image	—	Function.Injective.preimage_image Subtype.val_injective
preimage_val_sInter 📖	mathematical	—	preimage Elem Set instMembership sInter setOf	—	image.eq_1 sInter_image sInter_eq_biInter preimage_iInter
preimage_val_sInter_eq_sInter 📖	mathematical	—	preimage Elem Set instMembership sInter image	—	preimage_sInter sInter_image
preimage_val_sUnion 📖	mathematical	—	preimage Elem Set instMembership sUnion setOf	—	image.eq_1 sUnion_image sUnion_eq_biUnion preimage_iUnion
subset_of_image_val_subset_image_val 📖	mathematical	Set instHasSubset image instMembership	Elem	—	image_subset_image_iff Subtype.val_injective
subset_preimage_val_image_val_iff 📖	mathematical	—	Set Elem instHasSubset preimage instMembership image	—	preimage_image_eq Subtype.val_injective

---

← Back to Index