Dissipate

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

Statistics

Metric	Count
Definitions dissipate	1
Theorems antitone_dissipate, biInter_dissipate, directed_dissipate, dissipate_bot, dissipate_def, dissipate_eq_biInter_lt, dissipate_subset, dissipate_subset_dissipate, dissipate_succ, dissipate_zero_nat, exists_dissipate_eq_empty_iff_of_directed, exists_subset_dissipate_of_directed, iInter_dissipate, iInter_subset_dissipate, mem_dissipate	15
Total	16

Set

Definitions

Name	Category	Theorems
dissipate 📖	CompOp	16 math math: iInter_dissipate, mem_dissipate, dissipate_eq_biInter_lt, dissipate_def, dissipate_subset_dissipate, exists_subset_dissipate_of_directed, dissipate_bot, directed_dissipate, antitone_dissipate, dissipate_subset, biInter_dissipate, dissipate_succ, exists_dissipate_eq_empty_iff_of_directed, IsPiSystem.dissipate_mem, dissipate_zero_nat, iInter_subset_dissipate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitone_dissipate 📖	mathematical	—	Antitone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra dissipate Preorder.toLE	—	biInter_subset_biInter_left le_trans
biInter_dissipate 📖	mathematical	—	iInter Preorder.toLE dissipate	—	Subset.antisymm iInter_mono le_rfl dissipate_subset_dissipate
directed_dissipate 📖	mathematical	—	Directed Set instHasSubset dissipate	—	Antitone.directed_ge SemilatticeSup.instIsDirectedOrder antitone_dissipate
dissipate_bot 📖	mathematical	—	dissipate Preorder.toLE PartialOrder.toPreorder Bot.bot OrderBot.toBot	—	iInter_congr_Prop iInter_iInter_eq_left
dissipate_def 📖	mathematical	—	dissipate iInter	—	—
dissipate_eq_biInter_lt 📖	mathematical	—	dissipate iInter	—	iInter_congr_Prop
dissipate_subset 📖	mathematical	—	Set instHasSubset dissipate	—	biInter_subset_of_mem
dissipate_subset_dissipate 📖	mathematical	Preorder.toLE	Set instHasSubset dissipate Preorder.toLE	—	antitone_dissipate
dissipate_succ 📖	mathematical	—	dissipate Set instInter	—	ext
dissipate_zero_nat 📖	mathematical	—	dissipate	—	iInter_congr_Prop iInter_iInter_eq_left
exists_dissipate_eq_empty_iff_of_directed 📖	mathematical	Directed Set instHasSubset	dissipate Set instEmptyCollection	—	Mathlib.Tactic.Contrapose.contrapose₁ exists_subset_dissipate_of_directed Nonempty.mono subset_eq_empty dissipate_subset le_rfl
exists_subset_dissipate_of_directed 📖	mathematical	Directed Set instHasSubset	Set instHasSubset dissipate	—	iInter_congr_Prop iInter_iInter_eq_left instReflSubset dissipate_succ
iInter_dissipate 📖	mathematical	—	iInter dissipate Preorder.toLE	—	Subset.antisymm le_rfl
iInter_subset_dissipate 📖	mathematical	—	Set instHasSubset iInter dissipate	—	iInter_subset_of_subset
mem_dissipate 📖	mathematical	—	Set instMembership dissipate	—	—

---

← Back to Index