Documentation Verification Report

Pairwise

📁 Source: Mathlib/Data/Finset/Pairwise.lean

Statistics

Metric	Count
Definitions `instDecidablePairwiseCoeFinsetOfDecidableEqOfDecidableRel`	1
Theorems `pairwiseDisjoint_range_singleton`, `pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint`, `pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint`, `pairwise_iff_coe_toFinset_pairwise`, `pairwise_of_coe_toFinset_pairwise`, `attach`, `biUnion_finset`, `elim_finset`, `image_finset_of_le`	9
Total	10

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pairwiseDisjoint_range_singleton` 📖	mathematical	—	`Set.PairwiseDisjoint` `Finset` `partialOrder` `instOrderBot` `Set.range` `instSingleton`	—	`disjoint_singleton`

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint` 📖	mathematical	—	`Set.PairwiseDisjoint` `SetLike.coe` `Finset` `Finset.instSetLike` `toFinset` `Function.onFun` `Disjoint`	—	`pairwise_iff_coe_toFinset_pairwise` `Symmetric.comap` `symmetric_disjoint`
`pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint` 📖	mathematical	`Set.PairwiseDisjoint` `SetLike.coe` `Finset` `Finset.instSetLike` `toFinset`	`Function.onFun` `Disjoint`	—	`pairwise_of_coe_toFinset_pairwise`
`pairwise_iff_coe_toFinset_pairwise` 📖	mathematical	`Symmetric`	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `toFinset`	—	`coe_toFinset` `Nodup.pairwise_coe`
`pairwise_of_coe_toFinset_pairwise` 📖	—	`Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `toFinset`	—	—	`Nodup.pairwise_of_set_pairwise` `coe_toFinset`

Set.PairwiseDisjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`attach` 📖	mathematical	`Set.PairwiseDisjoint` `SemilatticeInf.toPartialOrder` `SetLike.coe` `Finset` `Finset.instSetLike`	`Finset.instMembership` `Finset.attach`	—	—
`biUnion_finset` 📖	mathematical	`Set.PairwiseDisjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `Finset.sup` `Lattice.toSemilatticeSup` `SetLike.coe` `Finset` `Finset.instSetLike`	`Set.iUnion` `Set` `Set.instMembership`	—	`eq_or_ne` `Disjoint.mono` `Finset.le_sup`
`elim_finset` 📖	—	`Set.PairwiseDisjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot` `Set` `Set.instMembership` `Finset.instMembership`	—	—	`elim` `Finset.not_disjoint_iff`
`image_finset_of_le` 📖	mathematical	`Set.PairwiseDisjoint` `SemilatticeInf.toPartialOrder` `SetLike.coe` `Finset` `Finset.instSetLike` `Preorder.toLE` `PartialOrder.toPreorder`	`Finset.image`	—	`Finset.coe_image` `image_of_le`

(root)

Definitions

Name	Category	Theorems
`instDecidablePairwiseCoeFinsetOfDecidableEqOfDecidableRel` 📖	CompOp	—

---

← Back to Index