Set

📁 Source: Mathlib/Logic/Equiv/Set.lean

Statistics

Metric	Count
Definitions compl, empty, image, imageOfInjOn, insert, pempty, powerset, prod, rangeInl, rangeInr, rangeSplittingImageEquiv, sep, singleton, sumCompl, sumDiffSubset, union, union', unionSumInter, univ, univPi, image, ofInjective, ofLeftInverse, ofLeftInverse', ofPreimageEquiv, setCongr, setProdEquivSigma, sigmaPreimageEquiv, equiv	29
Theorems strictMono_setCongr, congr_apply, congr_symm_apply, image_apply, image_symm_apply, image_symm_preimage, insert_apply_left, insert_apply_right, insert_symm_apply_inl, insert_symm_apply_inr, rangeInl_apply_inl, rangeInl_symm_apply_coe, rangeInr_apply_inr, rangeInr_symm_apply_coe, rangeSplittingImageEquiv_apply_coe_coe, rangeSplittingImageEquiv_symm_apply_coe, sumCompl_apply_inl, sumCompl_apply_inr, sumCompl_symm_apply, sumCompl_symm_apply_compl, sumCompl_symm_apply_of_mem, sumCompl_symm_apply_of_notMem, sumDiffSubset_apply_inl, sumDiffSubset_apply_inr, sumDiffSubset_symm_apply_of_mem, sumDiffSubset_symm_apply_of_notMem, union_apply_left, union_apply_right, union_symm_apply_left, union_symm_apply_right, univPi_apply_coe, univPi_symm_apply_coe, univ_apply, univ_symm_apply, apply_ofInjective_symm, coe_ofInjective_symm, eq_image_iff_symm_image_eq, eq_preimage_iff_image_eq, image_antitone, image_apply_coe, image_compl, image_eq_iff_eq, image_eq_preimage, image_eq_preimage_symm, image_monotone, image_preimage, image_strictAnti, image_strictMono, image_subset, image_symm_apply_coe, image_symm_eq_preimage, image_symm_image, ofInjective_apply, ofInjective_symm_apply, ofLeftInverse'_eq_ofInjective, ofLeftInverse_apply_coe, ofLeftInverse_eq_ofInjective, ofLeftInverse_symm_apply, ofPreimageEquiv_apply, ofPreimageEquiv_map, ofPreimageEquiv_symm_apply, preimage_eq_iff_eq_image, preimage_image, preimage_piEquivPiSubtypeProd_symm_pi, preimage_subset, preimage_symm_preimage, prod_assoc_image, prod_assoc_preimage, prod_assoc_symm_image, prod_assoc_symm_preimage, range_eq_univ, self_comp_ofInjective_symm, setCongr_apply, setCongr_symm_apply, setOf_apply_symm_eq_image_setOf, set_forall_iff, sigmaPreimageEquiv_apply, sigmaPreimageEquiv_symm_apply_fst, sigmaPreimageEquiv_symm_apply_snd_coe, subset_symm_image, swap_bijOn_exchange, swap_bijOn_self, symm_image_image, symm_image_subset, symm_preimage_preimage, range_eq_univ, image_equiv_eq_preimage_symm, mem_image_equiv, preimage_equiv_eq_image_symm, dite_comp_equiv_update	90
Total	119

Equiv

Definitions

Name	Category	Theorems
image 📖	CompOp	6 math math: image_strictAnti, image_strictMono, image_antitone, image_symm_apply_coe, image_apply_coe, image_monotone
ofInjective 📖	CompOp	13 math math: coe_ofInjective_symm, Fin.coe_of_injective_castSucc_symm, Isometry.isometryEquivOnRange_toEquiv, Fin.coe_of_injective_castLE_symm, LinearIndependent.span_repr_eq, ofInjective_symm_apply, ofLeftInverse'_eq_ofInjective, ofInjective_apply, Function.Embedding.toEquivRange_eq_ofInjective, ofLeftInverse_eq_ofInjective, Types.monoOverEquivalenceSet_unitIso, self_comp_ofInjective_symm, apply_ofInjective_symm
ofLeftInverse 📖	CompOp	3 math math: ofLeftInverse_apply_coe, ofLeftInverse_symm_apply, ofLeftInverse_eq_ofInjective
ofLeftInverse' 📖	CompOp	1 math math: ofLeftInverse'_eq_ofInjective
ofPreimageEquiv 📖	CompOp	3 math math: ofPreimageEquiv_map, ofPreimageEquiv_apply, ofPreimageEquiv_symm_apply
setCongr 📖	CompOp	4 math math: PrincipalSeg.subrelIso_symm_apply, Set.Equiv.strictMono_setCongr, setCongr_apply, setCongr_symm_apply
setProdEquivSigma 📖	CompOp	—
sigmaPreimageEquiv 📖	CompOp	3 math math: sigmaPreimageEquiv_symm_apply_snd_coe, sigmaPreimageEquiv_symm_apply_fst, sigmaPreimageEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_ofInjective_symm 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Set.range EquivLike.toFunLike instEquivLike symm ofInjective Set Set.instMembership	—	apply_symm_apply
coe_ofInjective_symm 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Set.range EquivLike.toFunLike instEquivLike symm ofInjective Set.rangeSplitting	—	ofInjective_symm_apply Set.apply_rangeSplitting
eq_image_iff_symm_image_eq 📖	mathematical	—	Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm	—	Function.Injective.image_injective injective symm_image_image
eq_preimage_iff_image_eq 📖	mathematical	—	Set.preimage DFunLike.coe Equiv EquivLike.toFunLike instEquivLike Set.image	—	Set.eq_preimage_iff_image_eq bijective
image_antitone 📖	mathematical	Antitone DFunLike.coe Equiv EquivLike.toFunLike instEquivLike	Set.Elem Set.image Subtype.preorder Set Set.instMembership image	—	Antitone.comp_monotone Subtype.mono_coe
image_apply_coe 📖	mathematical	—	Set Set.instMembership Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike Set.Elem image	—	—
image_compl 📖	mathematical	—	Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike Compl.compl Set Set.instCompl	—	Set.image_compl_eq bijective
image_eq_iff_eq 📖	mathematical	—	Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike	—	Set.image_eq_image injective
image_eq_preimage 📖	mathematical	—	Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike Set.preimage symm	—	image_eq_preimage_symm
image_eq_preimage_symm 📖	mathematical	—	Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike Set.preimage symm	—	image_symm_eq_preimage
image_monotone 📖	mathematical	Monotone DFunLike.coe Equiv EquivLike.toFunLike instEquivLike	Set.Elem Set.image Subtype.preorder Set Set.instMembership image	—	Monotone.comp Subtype.mono_coe
image_preimage 📖	mathematical	—	Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike Set.preimage	—	Function.Surjective.image_preimage surjective
image_strictAnti 📖	mathematical	StrictAnti DFunLike.coe Equiv EquivLike.toFunLike instEquivLike	Set.Elem Set.image Subtype.preorder Set Set.instMembership image	—	StrictAnti.comp_strictMono Subtype.strictMono_coe
image_strictMono 📖	mathematical	StrictMono DFunLike.coe Equiv EquivLike.toFunLike instEquivLike	Set.Elem Set.image Subtype.preorder Set Set.instMembership image	—	StrictMono.comp Subtype.strictMono_coe
image_subset 📖	mathematical	—	Set Set.instHasSubset Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike	—	Set.image_subset_image_iff injective
image_symm_apply_coe 📖	mathematical	—	Set Set.instMembership DFunLike.coe Equiv Set.Elem Set.image EquivLike.toFunLike instEquivLike symm image	—	—
image_symm_eq_preimage 📖	mathematical	—	Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm Set.preimage	—	Set.ext Set.mem_image_iff_of_inverse right_inv left_inv
image_symm_image 📖	mathematical	—	Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm	—	symm_image_image
ofInjective_apply 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Set.range EquivLike.toFunLike instEquivLike ofInjective Set Set.instMembership	—	—
ofInjective_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Set.range EquivLike.toFunLike instEquivLike symm ofInjective Set Set.instMembership	—	injective apply_symm_apply
ofLeftInverse'_eq_ofInjective 📖	mathematical	—	ofLeftInverse' ofInjective	—	ext
ofLeftInverse_apply_coe 📖	mathematical	—	Set Set.instMembership Set.range DFunLike.coe Equiv Set.Elem EquivLike.toFunLike instEquivLike ofLeftInverse	—	—
ofLeftInverse_eq_ofInjective 📖	mathematical	—	ofLeftInverse ofInjective IsEmpty isEmpty_or_nonempty IsEmpty.instSubsingleton	—	ext isEmpty_or_nonempty IsEmpty.instSubsingleton
ofLeftInverse_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Set.range EquivLike.toFunLike instEquivLike symm ofLeftInverse Set Set.instMembership	—	—
ofPreimageEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike instEquivLike ofPreimageEquiv symm sigmaFiberEquiv	—	—
ofPreimageEquiv_map 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike instEquivLike ofPreimageEquiv	—	ofFiberEquiv_map
ofPreimageEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm ofPreimageEquiv sigmaCongrRight sigmaFiberEquiv	—	—
preimage_eq_iff_eq_image 📖	mathematical	—	Set.preimage DFunLike.coe Equiv EquivLike.toFunLike instEquivLike Set.image	—	Set.preimage_eq_iff_eq_image bijective
preimage_image 📖	mathematical	—	Set.preimage DFunLike.coe Equiv EquivLike.toFunLike instEquivLike Set.image	—	Function.Injective.preimage_image injective
preimage_piEquivPiSubtypeProd_symm_pi 📖	mathematical	—	Set.preimage DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm piEquivPiSubtypeProd Set.pi Set.univ SProd.sprod Set Set.instSProd	—	Set.ext instIsEmptyFalse
preimage_subset 📖	mathematical	—	Set Set.instHasSubset Set.preimage DFunLike.coe Equiv EquivLike.toFunLike instEquivLike	—	Function.Surjective.preimage_subset_preimage_iff surjective
preimage_symm_preimage 📖	mathematical	—	Set.preimage DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm	—	Function.LeftInverse.preimage_preimage leftInverse_symm
prod_assoc_image 📖	mathematical	—	Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike prodAssoc SProd.sprod Set Set.instSProd	—	image_eq_preimage_symm prod_assoc_symm_preimage
prod_assoc_preimage 📖	mathematical	—	Set.preimage DFunLike.coe Equiv EquivLike.toFunLike instEquivLike prodAssoc SProd.sprod Set Set.instSProd	—	Set.ext
prod_assoc_symm_image 📖	mathematical	—	Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm prodAssoc SProd.sprod Set Set.instSProd	—	image_eq_preimage_symm prod_assoc_preimage
prod_assoc_symm_preimage 📖	mathematical	—	Set.preimage DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm prodAssoc SProd.sprod Set Set.instSProd	—	Set.ext
range_eq_univ 📖	mathematical	—	Set.range DFunLike.coe Equiv EquivLike.toFunLike instEquivLike Set.univ	—	EquivLike.range_eq_univ
self_comp_ofInjective_symm 📖	mathematical	—	Set.Elem Set.range DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm ofInjective Set Set.instMembership	—	apply_ofInjective_symm
setCongr_apply 📖	mathematical	—	DFunLike.coe Equiv Set.Elem EquivLike.toFunLike instEquivLike setCongr Set Set.instMembership refl	—	—
setCongr_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Set.Elem EquivLike.toFunLike instEquivLike symm setCongr Set Set.instMembership refl	—	—
setOf_apply_symm_eq_image_setOf 📖	mathematical	—	setOf DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm Set.image	—	image_eq_preimage_symm Set.preimage_setOf_eq
set_forall_iff 📖	mathematical	—	Set.preimage DFunLike.coe Equiv EquivLike.toFunLike instEquivLike	—	Function.Surjective.forall Function.Injective.preimage_surjective injective
sigmaPreimageEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Set.preimage Set Set.instSingletonSet EquivLike.toFunLike instEquivLike sigmaPreimageEquiv	—	—
sigmaPreimageEquiv_symm_apply_fst 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Set.preimage Set Set.instSingletonSet EquivLike.toFunLike instEquivLike symm sigmaPreimageEquiv	—	—
sigmaPreimageEquiv_symm_apply_snd_coe 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Set.preimage Set Set.instSingletonSet EquivLike.toFunLike instEquivLike symm sigmaPreimageEquiv	—	—
subset_symm_image 📖	mathematical	—	Set Set.instHasSubset Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm	—	symm_image_subset symm_symm
swap_bijOn_exchange 📖	mathematical	Set Set.instMembership	Set.BijOn DFunLike.coe Perm EquivLike.toFunLike instEquivLike swap Set.instInsert Set.instSDiff Set.instSingletonSet	—	—
swap_bijOn_self 📖	mathematical	Set Set.instMembership	Set.BijOn DFunLike.coe Perm EquivLike.toFunLike instEquivLike swap	—	—
symm_image_image 📖	mathematical	—	Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm	—	Function.LeftInverse.image_image leftInverse_symm
symm_image_subset 📖	mathematical	—	Set Set.instHasSubset Set.image DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm	—	Set.image_subset_iff image_eq_preimage_symm
symm_preimage_preimage 📖	mathematical	—	Set.preimage DFunLike.coe Equiv EquivLike.toFunLike instEquivLike symm	—	Function.LeftInverse.preimage_preimage rightInverse_symm

Equiv.Set

Definitions

Name	Category	Theorems
compl 📖	CompOp	—
empty 📖	CompOp	—
image 📖	CompOp	3 math math: image_apply, image_symm_preimage, image_symm_apply
imageOfInjOn 📖	CompOp	—
insert 📖	CompOp	4 math math: insert_symm_apply_inr, insert_apply_left, insert_symm_apply_inl, insert_apply_right
pempty 📖	CompOp	—
powerset 📖	CompOp	—
prod 📖	CompOp	1 math math: Sublattice.prodEquiv_toEquiv
rangeInl 📖	CompOp	2 math math: rangeInl_symm_apply_coe, rangeInl_apply_inl
rangeInr 📖	CompOp	2 math math: rangeInr_apply_inr, rangeInr_symm_apply_coe
rangeSplittingImageEquiv 📖	CompOp	2 math math: rangeSplittingImageEquiv_symm_apply_coe, rangeSplittingImageEquiv_apply_coe_coe
sep 📖	CompOp	—
singleton 📖	CompOp	—
sumCompl 📖	CompOp	6 math math: sumCompl_symm_apply_of_mem, sumCompl_symm_apply, sumCompl_apply_inr, sumCompl_apply_inl, sumCompl_symm_apply_compl, sumCompl_symm_apply_of_notMem
sumDiffSubset 📖	CompOp	4 math math: sumDiffSubset_symm_apply_of_notMem, sumDiffSubset_apply_inr, sumDiffSubset_symm_apply_of_mem, sumDiffSubset_apply_inl
union 📖	CompOp	4 math math: union_symm_apply_left, union_apply_left, union_apply_right, union_symm_apply_right
union' 📖	CompOp	—
unionSumInter 📖	CompOp	—
univ 📖	CompOp	2 math math: univ_symm_apply, univ_apply
univPi 📖	CompOp	2 math math: univPi_symm_apply_coe, univPi_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_apply 📖	mathematical	—	DFunLike.coe Equiv Set EquivLike.toFunLike Equiv.instEquivLike congr Set.image	—	—
congr_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Set EquivLike.toFunLike Equiv.instEquivLike Equiv.symm congr Set.image	—	—
image_apply 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Set.image EquivLike.toFunLike Equiv.instEquivLike image Set Set.instMembership	—	—
image_symm_apply 📖	mathematical	Set Set.instMembership Set.image	DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm image Function.Injective.mem_set_image	—	Function.Injective.mem_set_image Equiv.symm_apply_eq
image_symm_preimage 📖	mathematical	—	Set.preimage Set.Elem Set.image Set Set.instMembership DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm image	—	Set.ext Function.Injective.mem_set_image image_symm_apply
insert_apply_left 📖	mathematical	Set Set.instMembership	DFunLike.coe Equiv Set.Elem Set.instInsert EquivLike.toFunLike Equiv.instEquivLike insert	—	Equiv.apply_eq_iff_eq_symm_apply
insert_apply_right 📖	mathematical	Set Set.instMembership	DFunLike.coe Equiv Set.Elem Set.instInsert EquivLike.toFunLike Equiv.instEquivLike insert	—	Equiv.apply_eq_iff_eq_symm_apply
insert_symm_apply_inl 📖	mathematical	Set Set.instMembership	DFunLike.coe Equiv Set.Elem Set.instInsert EquivLike.toFunLike Equiv.instEquivLike Equiv.symm insert	—	—
insert_symm_apply_inr 📖	mathematical	Set Set.instMembership	DFunLike.coe Equiv Set.Elem Set.instInsert EquivLike.toFunLike Equiv.instEquivLike Equiv.symm insert	—	—
rangeInl_apply_inl 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Set.range EquivLike.toFunLike Equiv.instEquivLike rangeInl Set Set.instMembership Set.mem_range_self	—	Set.mem_range_self
rangeInl_symm_apply_coe 📖	mathematical	—	Set Set.instMembership Set.range DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm rangeInl	—	—
rangeInr_apply_inr 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Set.range EquivLike.toFunLike Equiv.instEquivLike rangeInr Set Set.instMembership Set.mem_range_self	—	Set.mem_range_self
rangeInr_symm_apply_coe 📖	mathematical	—	Set Set.instMembership Set.range DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm rangeInr	—	—
rangeSplittingImageEquiv_apply_coe_coe 📖	mathematical	—	Set Set.instMembership Set.range Set.Elem DFunLike.coe Equiv Set.image Set.rangeSplitting EquivLike.toFunLike Equiv.instEquivLike rangeSplittingImageEquiv	—	—
rangeSplittingImageEquiv_symm_apply_coe 📖	mathematical	—	Set Set.instMembership Set.image Set.Elem Set.range Set.rangeSplitting DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm rangeSplittingImageEquiv	—	—
sumCompl_apply_inl 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Compl.compl Set Set.instCompl EquivLike.toFunLike Equiv.instEquivLike sumCompl Set.instMembership	—	—
sumCompl_apply_inr 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Compl.compl Set Set.instCompl EquivLike.toFunLike Equiv.instEquivLike sumCompl Set.instMembership	—	—
sumCompl_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Compl.compl Set Set.instCompl EquivLike.toFunLike Equiv.instEquivLike Equiv.symm sumCompl Set.instMembership	—	Equiv.sumCompl_symm_apply_pos
sumCompl_symm_apply_compl 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Compl.compl Set Set.instCompl EquivLike.toFunLike Equiv.instEquivLike Equiv.symm sumCompl Set.instMembership	—	Equiv.sumCompl_symm_apply_neg
sumCompl_symm_apply_of_mem 📖	mathematical	Set Set.instMembership	DFunLike.coe Equiv Set.Elem Compl.compl Set.instCompl EquivLike.toFunLike Equiv.instEquivLike Equiv.symm sumCompl	—	Equiv.sumCompl_symm_apply_of_pos
sumCompl_symm_apply_of_notMem 📖	mathematical	Set Set.instMembership	DFunLike.coe Equiv Set.Elem Compl.compl Set.instCompl EquivLike.toFunLike Equiv.instEquivLike Equiv.symm sumCompl	—	Equiv.sumCompl_symm_apply_of_neg
sumDiffSubset_apply_inl 📖	mathematical	Set Set.instHasSubset	DFunLike.coe Equiv Set.Elem Set.instSDiff EquivLike.toFunLike Equiv.instEquivLike sumDiffSubset Set.inclusion	—	—
sumDiffSubset_apply_inr 📖	mathematical	Set Set.instHasSubset	DFunLike.coe Equiv Set.Elem Set.instSDiff EquivLike.toFunLike Equiv.instEquivLike sumDiffSubset Set.inclusion Set.diff_subset	—	—
sumDiffSubset_symm_apply_of_mem 📖	mathematical	Set Set.instHasSubset Set.instMembership	DFunLike.coe Equiv Set.Elem Set.instSDiff EquivLike.toFunLike Equiv.instEquivLike Equiv.symm sumDiffSubset	—	Equiv.injective Equiv.apply_symm_apply
sumDiffSubset_symm_apply_of_notMem 📖	mathematical	Set Set.instHasSubset Set.instMembership	DFunLike.coe Equiv Set.Elem Set.instSDiff EquivLike.toFunLike Equiv.instEquivLike Equiv.symm sumDiffSubset	—	Equiv.injective Set.diff_subset Equiv.apply_symm_apply
union_apply_left 📖	mathematical	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Set.instMembership Set.instUnion	DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike union	—	—
union_apply_right 📖	mathematical	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra Set.instMembership Set.instUnion	DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike union	—	Set.disjoint_left
union_symm_apply_left 📖	mathematical	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra	DFunLike.coe Equiv Set.Elem Set.instUnion EquivLike.toFunLike Equiv.instEquivLike Equiv.symm union Set.instMembership	—	—
union_symm_apply_right 📖	mathematical	Disjoint Set SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra Set.instBooleanAlgebra HeytingAlgebra.toOrderBot BiheytingAlgebra.toHeytingAlgebra	DFunLike.coe Equiv Set.Elem Set.instUnion EquivLike.toFunLike Equiv.instEquivLike Equiv.symm union Set.instMembership	—	—
univPi_apply_coe 📖	mathematical	—	Set Set.instMembership DFunLike.coe Equiv Set.Elem Set.pi Set.univ EquivLike.toFunLike Equiv.instEquivLike univPi	—	—
univPi_symm_apply_coe 📖	mathematical	—	Set Set.instMembership Set.pi Set.univ DFunLike.coe Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike Equiv.symm univPi	—	—
univ_apply 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Set.univ EquivLike.toFunLike Equiv.instEquivLike univ Set Set.instMembership	—	—
univ_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Set.Elem Set.univ EquivLike.toFunLike Equiv.instEquivLike Equiv.symm univ Set Set.instMembership	—	—

Equiv.Set.Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictMono_setCongr 📖	mathematical	—	StrictMono Set.Elem Subtype.preorder Set Set.instMembership DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.setCongr	—	—

EquivLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_eq_univ 📖	mathematical	—	Set.range DFunLike.coe toFunLike Set.univ	—	Set.eq_univ_of_forall Equiv.surjective

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_equiv_eq_preimage_symm 📖	mathematical	—	image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike preimage Equiv.symm	—	Equiv.image_eq_preimage_symm
mem_image_equiv 📖	mathematical	—	Set instMembership image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm	—	ext_iff Equiv.image_eq_preimage_symm
preimage_equiv_eq_image_symm 📖	mathematical	—	preimage DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike image Equiv.symm	—	Equiv.image_symm_eq_preimage

Set.BijOn

Definitions

Name	Category	Theorems
equiv 📖	CompOp	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dite_comp_equiv_update 📖	mathematical	—	Function.update DFunLike.coe EquivLike.toFunLike EquivLike.inv	—	Function.update_apply Subtype.coe_eta EquivLike.apply_inv_apply EquivLike.inv_apply_apply

---

← Back to Index