Documentation Verification Report

Dissipate

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

Statistics

Metric	Count
Definitions `dissipate`	1
Theorems `antitone_dissipate`, `biInter_dissipate`, `dissipate_bot`, `dissipate_def`, `dissipate_subset`, `dissipate_subset_dissipate`, `dissipate_succ`, `dissipate_zero_nat`, `iInter_dissipate`, `iInter_subset_dissipate`, `mem_dissipate`	11
Total	12

Set

Definitions

Name	Category	Theorems
`dissipate` 📖	CompOp	11 math math: `iInter_dissipate`, `mem_dissipate`, `dissipate_def`, `dissipate_subset_dissipate`, `dissipate_bot`, `antitone_dissipate`, `dissipate_subset`, `biInter_dissipate`, `dissipate_succ`, `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`
`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_subset` 📖	mathematical	—	`Set` `instHasSubset` `dissipate`	—	`biInter_subset_of_mem`
`dissipate_subset_dissipate` 📖	mathematical	`Preorder.toLE`	`Set` `instHasSubset` `dissipate`	—	`antitone_dissipate`
`dissipate_succ` 📖	mathematical	—	`dissipate` `Set` `instInter`	—	`ext`
`dissipate_zero_nat` 📖	mathematical	—	`dissipate`	—	`iInter_congr_Prop` `iInter_iInter_eq_left`
`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