UV

📁 Source: Mathlib/Combinatorics/SetFamily/Compression/UV.lean

Statistics

Metric	Count
Definitions term𝓒, IsCompressed, compress, compression	4
Theorems uvCompression, eq, card_compress, card_compression, card_shadow_compression_le, compress_disjoint, compress_idem, compress_injOn, compress_mem_compression, compress_mem_compression_of_mem_compression, compress_of_disjoint_of_le, compress_of_disjoint_of_le', compress_sdiff_sdiff, compress_self, compression_idem, compression_self, disjoint_of_mem_compression_of_notMem, isCompressed_self, le_of_mem_compression_of_notMem, mem_compression, mem_of_mem_compression, shadow_compression_subset_compression_shadow, sup_sdiff_mem_of_mem_compression, sup_sdiff_mem_of_mem_compression_of_notMem, sup_sdiff_injOn	25
Total	29

FinsetFamily

Definitions

Name	Category	Theorems
term𝓒 📖	CompOp	—

Set.Sized

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
uvCompression 📖	mathematical	Finset.card Set.Sized SetLike.coe Finset Finset.instSetLike	UV.compression Finset.instGeneralizedBooleanAlgebra Finset.decidableDisjoint Finset.instDecidableLE Finset.decidableEq	—	UV.card_compress

UV

Definitions

Name	Category	Theorems
IsCompressed 📖	MathDef	1 math math: isCompressed_self
compress 📖	CompOp	12 math math: compress_injOn, compress_of_disjoint_of_le', compress_self, compress_sdiff_sdiff, card_compress, compress_mem_compression, Finset.UV.toColex_compress_lt_toColex, compress_of_disjoint_of_le, compress_idem, compress_disjoint, mem_compression, compress_mem_compression_of_mem_compression
compression 📖	CompOp	9 math math: shadow_compression_subset_compression_shadow, IsCompressed.eq, card_shadow_compression_le, compression_self, Set.Sized.uvCompression, compress_mem_compression, compression_idem, mem_compression, card_compression

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_compress 📖	mathematical	Finset.card	compress Finset Finset.instGeneralizedBooleanAlgebra Finset.decidableDisjoint Finset.instDecidableLE	—	Finset.card_sdiff_of_subset LE.le.trans le_sup_left Finset.sup_eq_union Finset.card_union_of_disjoint Disjoint.symm add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
card_compression 📖	mathematical	—	Finset.card compression	—	compression.eq_1 Finset.card_union_of_disjoint compress_disjoint Finset.filter_image Finset.card_image_of_injOn compress_injOn Finset.disjoint_filter_filter_not Finset.filter_union_filter_not_eq
card_shadow_compression_le 📖	mathematical	Finset Finset.instMembership IsCompressed Finset.instGeneralizedBooleanAlgebra Finset.decidableDisjoint Finset.instDecidableLE Finset.decidableEq Finset.erase	Finset.card Finset.shadow compression	—	LE.le.trans Finset.card_le_card shadow_compression_subset_compression_shadow Eq.le card_compression
compress_disjoint 📖	mathematical	—	Disjoint Finset Finset.partialOrder Finset.instOrderBot Finset.filter Finset.instMembership compress Finset.decidableMem Finset.image	—	Finset.disjoint_left Finset.mem_filter
compress_idem 📖	mathematical	—	compress	—	le_sdiff_right sdiff_bot sup_assoc sup_idem
compress_injOn 📖	mathematical	—	Set.InjOn compress SetLike.coe Finset Finset.instSetLike Finset.filter Finset.instMembership Finset.decidableMem	—	sup_sdiff_injOn compress.eq_1 Finset.mem_filter Finset.mem_coe
compress_mem_compression 📖	mathematical	Finset Finset.instMembership	compression compress	—	mem_compression compress_idem
compress_mem_compression_of_mem_compression 📖	mathematical	Finset Finset.instMembership compression	compress	—	mem_compression compress_idem
compress_of_disjoint_of_le 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra GeneralizedBooleanAlgebra.toOrderBot Preorder.toLE PartialOrder.toPreorder	compress GeneralizedBooleanAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup	—	—
compress_of_disjoint_of_le' 📖	mathematical	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra GeneralizedBooleanAlgebra.toOrderBot Preorder.toLE PartialOrder.toPreorder	compress GeneralizedBooleanAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup	—	compress_of_disjoint_of_le disjoint_sdiff_self_right le_sdiff le_sup_right Disjoint.mono_right sdiff_sup_cancel le_sup_of_le_left Disjoint.sup_sdiff_cancel_right Disjoint.symm
compress_sdiff_sdiff 📖	mathematical	—	compress GeneralizedBooleanAlgebra.toSDiff	—	compress_of_disjoint_of_le disjoint_sdiff_self_left sdiff_le sup_sdiff_self_right sup_sdiff Disjoint.sdiff_eq_left disjoint_sdiff_self_right sup_eq_right sdiff_sdiff_le
compress_self 📖	mathematical	—	compress	—	Disjoint.sup_sdiff_cancel_right Disjoint.symm
compression_idem 📖	mathematical	—	compression	—	Finset.filter_false_of_mem compress_mem_compression_of_mem_compression compression.eq_1 Finset.filter_image Finset.image_empty Finset.filter_union_filter_not_eq
compression_self 📖	mathematical	—	compression	—	Finset.ext Finset.mem_filter compress_self Finset.eq_empty_of_forall_notMem Finset.union_empty
disjoint_of_mem_compression_of_notMem 📖	mathematical	Finset Finset.instMembership compression	Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra GeneralizedBooleanAlgebra.toOrderBot	—	mem_compression disjoint_sdiff_self_right
isCompressed_self 📖	mathematical	—	IsCompressed	—	compression_self
le_of_mem_compression_of_notMem 📖	mathematical	Finset Finset.instMembership compression	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra	—	mem_compression le_sdiff le_sup_right Disjoint.mono_right
mem_compression 📖	mathematical	—	Finset Finset.instMembership compression compress	—	—
mem_of_mem_compression 📖	—	Finset Finset.instMembership compression Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra Bot.bot GeneralizedBooleanAlgebra.toBot	—	—	mem_compression le_sdiff_right sup_bot_eq sdiff_bot
shadow_compression_subset_compression_shadow 📖	mathematical	Finset Finset.instMembership IsCompressed Finset.instGeneralizedBooleanAlgebra Finset.decidableDisjoint Finset.instDecidableLE Finset.decidableEq Finset.erase	Finset.instHasSubset Finset.shadow compression	—	Finset.mem_shadow_iff_insert_mem le_of_mem_compression_of_notMem disjoint_of_mem_compression_of_notMem sup_sdiff_mem_of_mem_compression_of_notMem Disjoint.mono_left Finset.subset_insert Disjoint.symm Finset.disjoint_of_subset_right Finset.disjoint_right Finset.mem_insert_self Disjoint.sdiff_eq_left sup_sdiff_mem_of_mem_compression IsCompressed.eq Finset.union_sdiff_distrib HasSubset.Subset.trans Finset.instIsTransSubset Finset.erase_subset Finset.subset_union_right Finset.disjoint_of_subset_left Finset.disjoint_sdiff Finset.sdiff_union_erase_cancel Finset.subset_union_left Finset.erase_union_distrib Finset.erase_insert Finset.erase_eq_of_notMem Finset.sdiff_erase Finset.mem_union_right Finset.union_sdiff_cancel_right Finset.subset_insert_iff Finset.notMem_sdiff_of_notMem_left Finset.notMem_union Finset.insert_sdiff_of_notMem Finset.insert_union Finset.subset_sdiff mem_of_mem_compression Finset.mem_union_left Finset.insert_union_comm Finset.insert_erase Finset.sdiff_union_of_subset Finset.mem_sdiff Finset.disjoint_insert_right mem_compression compress.eq_1 Finset.mem_shadow_iff Finset.notMem_mono Finset.notMem_erase LE.le.trans Finset.notMem_sdiff_of_mem_right Finset.disjoint_erase_comm Finset.erase_union_of_mem Finset.union_erase_of_mem Finset.sup_eq_union Finset.disjoint_of_erase_right Finset.mem_union compress_of_disjoint_of_le'
sup_sdiff_mem_of_mem_compression 📖	mathematical	Finset Finset.instMembership compression Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra Disjoint GeneralizedBooleanAlgebra.toOrderBot	GeneralizedBooleanAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup	—	compress_of_disjoint_of_le mem_compression Disjoint.mono_right compress_idem sdiff_le_sdiff_right le_sup_right disjoint_self Disjoint.sdiff_eq_left disjoint_sdiff_self_right compress_self sup_bot_eq sdiff_bot
sup_sdiff_mem_of_mem_compression_of_notMem 📖	mathematical	Finset Finset.instMembership compression	GeneralizedBooleanAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra	—	mem_compression sdiff_sup_cancel le_sup_of_le_left sup_sdiff_right_self Disjoint.sdiff_eq_left Disjoint.symm

UV.IsCompressed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	mathematical	UV.IsCompressed	UV.compression	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sup_sdiff_injOn 📖	mathematical	—	Set.InjOn GeneralizedBooleanAlgebra.toSDiff SemilatticeSup.toMax Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra setOf Disjoint SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf GeneralizedBooleanAlgebra.toOrderBot Preorder.toLE PartialOrder.toPreorder	—	sdiff_sup_cancel Disjoint.sup_sdiff_cancel_right Disjoint.symm sdiff_sdiff_comm

---

← Back to Index