Documentation Verification Report

IntervalSucc

📁 Source: Mathlib/Order/SuccPred/IntervalSucc.lean

Statistics

Metric	Count
Definitions	0
Theorems `pairwise_disjoint_on_Ico_pred`, `pairwise_disjoint_on_Ico_succ`, `pairwise_disjoint_on_Ioc_pred`, `pairwise_disjoint_on_Ioc_succ`, `pairwise_disjoint_on_Ioo_pred`, `pairwise_disjoint_on_Ioo_succ`, `biUnion_Ico_Ioc_map_succ`, `pairwise_disjoint_on_Ico_pred`, `pairwise_disjoint_on_Ico_succ`, `pairwise_disjoint_on_Ioc_pred`, `pairwise_disjoint_on_Ioc_succ`, `pairwise_disjoint_on_Ioo_pred`, `pairwise_disjoint_on_Ioo_succ`, `biUnion_Ici_Ico_map_succ`, `biUnion_Ici_Ioc_map_succ`, `iUnion_Ico_map_succ_eq_Ici`, `iUnion_Ioc_map_succ_eq_Ioi`	17
Total	17

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pairwise_disjoint_on_Ico_pred` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Ico` `Order.pred`	—	`Monotone.pairwise_disjoint_on_Ico_succ` `dual_left`
`pairwise_disjoint_on_Ico_succ` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Ico` `Order.succ`	—	`Monotone.pairwise_disjoint_on_Ico_pred` `dual_left`
`pairwise_disjoint_on_Ioc_pred` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Ioc` `Order.pred`	—	`Monotone.pairwise_disjoint_on_Ioc_succ` `dual_left`
`pairwise_disjoint_on_Ioc_succ` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Ioc` `Order.succ`	—	`Monotone.pairwise_disjoint_on_Ioc_pred` `dual_left`
`pairwise_disjoint_on_Ioo_pred` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Ioo` `Order.pred`	—	`Monotone.pairwise_disjoint_on_Ioo_succ` `dual_left`
`pairwise_disjoint_on_Ioo_succ` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Ioo` `Order.succ`	—	`Monotone.pairwise_disjoint_on_Ioo_pred` `dual_left`

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion_Ico_Ioc_map_succ` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.iUnion` `Set` `Set.instMembership` `Set.Ico` `Set.Ioc` `Order.succ`	—	`le_total` `Set.Ico_eq_empty_of_le` `Set.Ioc_eq_empty_of_le` `Set.biUnion_empty` `Set.iUnion_congr_Prop` `Set.Ico_self` `Set.Ioc_self` `Set.Ioc_union_Ioc_eq_Ioc` `Order.le_succ` `Set.union_comm` `IsMax.succ_eq` `Set.empty_union` `Order.Ico_succ_right_eq_insert_of_not_isMax` `Set.biUnion_insert`
`pairwise_disjoint_on_Ico_pred` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Ico` `Order.pred`	—	`Set.Ioc_toDual` `pairwise_disjoint_on_Ioc_succ` `dual`
`pairwise_disjoint_on_Ico_succ` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Ico` `Order.succ`	—	`pairwise_disjoint_on` `disjoint_iff_inf_le` `LT.lt.not_ge` `LE.le.trans` `Order.succ_le_of_lt`
`pairwise_disjoint_on_Ioc_pred` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Ioc` `Order.pred`	—	`Set.Ico_toDual` `pairwise_disjoint_on_Ico_succ` `dual`
`pairwise_disjoint_on_Ioc_succ` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Ioc` `Order.succ`	—	`pairwise_disjoint_on` `disjoint_iff_inf_le` `LT.lt.not_ge` `LE.le.trans` `Order.succ_le_of_lt`
`pairwise_disjoint_on_Ioo_pred` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Ioo` `Order.pred`	—	`Set.Ioo_toDual` `pairwise_disjoint_on_Ioo_succ` `dual`
`pairwise_disjoint_on_Ioo_succ` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pairwise` `Function.onFun` `Set` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Ioo` `Order.succ`	—	`Pairwise.mono` `pairwise_disjoint_on_Ico_succ` `Disjoint.mono` `Set.Ioo_subset_Ico_self`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion_Ici_Ico_map_succ` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `BddAbove` `Set.image` `Set.Ici`	`Set.iUnion` `Set` `Set.instMembership` `Set.Ico` `Order.succ`	—	`subset_antisymm` `Set.instAntisymmSubset` `Set.iUnion₂_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.Ico_subset_Ico_left` `Set.Ico_subset_Ici_self` `Mathlib.Tactic.Contrapose.contrapose₂` `Set.iUnion_congr_Prop`
`biUnion_Ici_Ioc_map_succ` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `BddAbove` `Set.image` `Set.Ici`	`Set.iUnion` `Set` `Set.instMembership` `Set.Ioc` `Order.succ` `Set.Ioi`	—	`subset_antisymm` `Set.instAntisymmSubset` `Set.iUnion₂_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.Ioc_subset_Ioc_left` `Set.Ioc_subset_Ioi_self` `Mathlib.Tactic.Contrapose.contrapose₂` `Set.iUnion_congr_Prop`
`iUnion_Ico_map_succ_eq_Ici` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Bot.bot` `OrderBot.toBot` `BddAbove` `Set.range`	`Set.iUnion` `Set.Ico` `Order.succ` `Set.Ici`	—	`Set.iUnion_congr_Prop` `Set.Ici_bot` `Set.iUnion_true` `biUnion_Ici_Ico_map_succ` `Set.image_univ`
`iUnion_Ioc_map_succ_eq_Ioi` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Bot.bot` `OrderBot.toBot` `BddAbove` `Set.range`	`Set.iUnion` `Set.Ioc` `Order.succ` `Set.Ioi`	—	`Set.iUnion_congr_Prop` `Set.Ici_bot` `Set.iUnion_true` `biUnion_Ici_Ioc_map_succ` `Set.image_univ`

---

← Back to Index