Documentation Verification Report

Disjoint

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

Statistics

Metric	Count
Definitions	0
Theorems `inter_eq`, `inter_left`, `inter_left'`, `inter_right`, `inter_right'`, `ne_of_mem`, `notMem_of_mem_left`, `notMem_of_mem_right`, `subset_left_of_subset_union`, `subset_right_of_subset_union`, `union_left`, `union_right`, `not_disjoint`, `disjoint_empty`, `disjoint_iff`, `disjoint_iff_forall_ne`, `disjoint_iff_inter_eq_empty`, `disjoint_left`, `disjoint_of_subset`, `disjoint_of_subset_left`, `disjoint_of_subset_right`, `disjoint_or_nonempty_inter`, `disjoint_range_iff`, `disjoint_right`, `disjoint_union_left`, `disjoint_union_right`, `disjoint_univ`, `empty_disjoint`, `mem_union_of_disjoint`, `not_disjoint_iff`, `not_disjoint_iff_nonempty_inter`, `univ_disjoint`	32
Total	32

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inter_eq` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Set.instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Set.instBoundedOrder`	`Set.instInter` `Set.instEmptyCollection`	—	`eq_bot`
`inter_left` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Set.instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Set.instBoundedOrder`	`Set.instInter`	—	`inf_left`
`inter_left'` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Set.instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Set.instBoundedOrder`	`Set.instInter`	—	`inf_left'`
`inter_right` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Set.instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Set.instBoundedOrder`	`Set.instInter`	—	`inf_right`
`inter_right'` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Set.instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Set.instBoundedOrder`	`Set.instInter`	—	`inf_right'`
`ne_of_mem` 📖	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Set.instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Set.instBoundedOrder` `Set.instMembership`	—	—	`Set.disjoint_iff_forall_ne`
`notMem_of_mem_left` 📖	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Set.instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Set.instBoundedOrder` `Set.instMembership`	—	—	`Set.disjoint_left`
`notMem_of_mem_right` 📖	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Set.instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Set.instBoundedOrder` `Set.instMembership`	—	—	`Set.disjoint_right`
`subset_left_of_subset_union` 📖	—	`Set` `Set.instHasSubset` `Set.instUnion` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Set.instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Set.instBoundedOrder`	—	—	`left_le_of_le_sup_right`
`subset_right_of_subset_union` 📖	—	`Set` `Set.instHasSubset` `Set.instUnion` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Set.instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Set.instBoundedOrder`	—	—	`left_le_of_le_sup_left`
`union_left` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Set.instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Set.instBoundedOrder`	`Set.instUnion`	—	`sup_left`
`union_right` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Set.instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Set.instBoundedOrder`	`Set.instUnion`	—	`sup_right`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_empty` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instEmptyCollection`	—	`disjoint_bot_right`
`disjoint_iff` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instHasSubset` `instInter` `instEmptyCollection`	—	`disjoint_iff_inf_le`
`disjoint_iff_forall_ne` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder`	—	—
`disjoint_iff_inter_eq_empty` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instInter` `instEmptyCollection`	—	`disjoint_iff`
`disjoint_left` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instMembership`	—	`disjoint_iff_inf_le`
`disjoint_of_subset` 📖	—	`Set` `instHasSubset` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder`	—	—	`Disjoint.mono`
`disjoint_of_subset_left` 📖	—	`Set` `instHasSubset` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder`	—	—	`Disjoint.mono_left`
`disjoint_of_subset_right` 📖	—	`Set` `instHasSubset` `Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder`	—	—	`Disjoint.mono_right`
`disjoint_or_nonempty_inter` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `Nonempty` `instInter`	—	`not_disjoint_iff_nonempty_inter` `em`
`disjoint_range_iff` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `range`	—	—
`disjoint_right` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instMembership`	—	`disjoint_comm` `disjoint_left`
`disjoint_union_left` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instUnion`	—	`disjoint_sup_left`
`disjoint_union_right` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instUnion`	—	`disjoint_sup_right`
`disjoint_univ` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `univ` `instEmptyCollection`	—	`disjoint_top`
`empty_disjoint` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instEmptyCollection`	—	`disjoint_bot_left`
`mem_union_of_disjoint` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder`	`instMembership` `instUnion` `Xor'`	—	—
`not_disjoint_iff` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instMembership`	—	—
`not_disjoint_iff_nonempty_inter` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `Nonempty` `instInter`	—	`not_disjoint_iff`
`univ_disjoint` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `univ` `instEmptyCollection`	—	`top_disjoint`

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_disjoint` 📖	mathematical	`Set.Nonempty` `Set` `Set.instInter`	`Disjoint` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `Set.instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Set.instBoundedOrder`	—	`Set.not_disjoint_iff_nonempty_inter`

---

← Back to Index