Documentation Verification Report

Gaps

📁 Source: Mathlib/Order/Interval/Finset/Gaps.lean

Statistics

Metric	Count
Definitions `intervalGapsWithin`, `fst`, `snd`	3
Theorems `intervalGapsWithin_fst_le_snd`, `intervalGapsWithin_fst_of_lt_lt`, `intervalGapsWithin_injOn`, `intervalGapsWithin_last_snd`, `intervalGapsWithin_le_fst`, `intervalGapsWithin_mapsTo`, `intervalGapsWithin_pairwiseDisjoint_Ioc`, `intervalGapsWithin_snd_le`, `intervalGapsWithin_snd_of_lt`, `intervalGapsWithin_succ_fst_of_lt`, `intervalGapsWithin_surjOn`, `intervalGapsWithin_zero_fst`	12
Total	15

Finset

Definitions

Name	Category	Theorems
`intervalGapsWithin` 📖	CompOp	18 math math: `sum_eq_sum_range_intervalGapsWithin`, `prod_intervalGapsWithin_mul_prod_eq_div`, `intervalGapsWithin_le_fst`, `intervalGapsWithin_fst_le_snd`, `prod_intervalGapsWithin_eq_div_div_prod`, `intervalGapsWithin_surjOn`, `intervalGapsWithin_injOn`, `prod_eq_prod_range_intervalGapsWithin`, `intervalGapsWithin_pairwiseDisjoint_Ioc`, `intervalGapsWithin_snd_of_lt`, `intervalGapsWithin_succ_fst_of_lt`, `intervalGapsWithin_snd_le`, `sum_intervalGapsWithin_eq_sub_sub_sum`, `sum_intervalGapsWithin_add_sum_eq_sub`, `intervalGapsWithin_fst_of_lt_lt`, `intervalGapsWithin_last_snd`, `intervalGapsWithin_mapsTo`, `intervalGapsWithin_zero_fst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`intervalGapsWithin_fst_le_snd` 📖	mathematical	`card` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.PairwiseDisjoint` `Set` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Finset` `instSetLike` `Set.Icc`	`intervalGapsWithin`	—	`intervalGapsWithin.congr_simp` `Fin.natCast_zero` `intervalGapsWithin_zero_fst` `intervalGapsWithin_last_snd` `intervalGapsWithin_mapsTo` `Fin.natCast_eq_last` `intervalGapsWithin_fst_of_lt_lt` `intervalGapsWithin_snd_of_lt` `orderEmbOfFin_mem` `RelEmbedding.injective` `Mathlib.Tactic.Contrapose.contrapose₁` `Prod.Lex.le_iff'` `OrderEmbedding.monotone` `LT.lt.le`
`intervalGapsWithin_fst_of_lt_lt` 📖	mathematical	`card`	`intervalGapsWithin` `DFunLike.coe` `OrderEmbedding` `Lex` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Prod.Lex.instLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfFin`	—	`intervalGapsWithin_succ_fst_of_lt`
`intervalGapsWithin_injOn` 📖	mathematical	`card`	`Set.InjOn` `intervalGapsWithin` `Set.Iio` `Nat.instPreorder`	—	`Set.mem_Iio` `intervalGapsWithin_snd_of_lt` `intervalGapsWithin_succ_fst_of_lt`
`intervalGapsWithin_last_snd` 📖	mathematical	`card`	`intervalGapsWithin`	—	—
`intervalGapsWithin_le_fst` 📖	mathematical	`card` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`intervalGapsWithin`	—	`intervalGapsWithin.congr_simp` `Fin.natCast_zero` `intervalGapsWithin_zero_fst` `intervalGapsWithin_mapsTo`
`intervalGapsWithin_mapsTo` 📖	mathematical	`card`	`Set.MapsTo` `intervalGapsWithin` `Set.Iio` `Nat.instPreorder` `SetLike.coe` `Finset` `instSetLike`	—	`Set.mem_Iio` `intervalGapsWithin_snd_of_lt` `intervalGapsWithin_succ_fst_of_lt` `orderEmbOfFin_mem`
`intervalGapsWithin_pairwiseDisjoint_Ioc` 📖	mathematical	`card` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set.PairwiseDisjoint` `Set` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.Iio` `Nat.instPreorder` `Set.Ioc` `intervalGapsWithin`	—	`Function.onFun.eq_1` `Set.disjoint_iff_inter_eq_empty` `intervalGapsWithin_mapsTo` `le_imp_le_of_le_of_le` `le_refl` `intervalGapsWithin.congr_simp` `intervalGapsWithin_snd_of_lt` `Prod.Lex.le_iff'` `OrderEmbedding.monotone` `Set.mem_Iio` `Disjoint.symm`
`intervalGapsWithin_snd_le` 📖	mathematical	`card` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`intervalGapsWithin`	—	`intervalGapsWithin.congr_simp` `Fin.natCast_eq_last` `intervalGapsWithin_last_snd` `intervalGapsWithin_mapsTo`
`intervalGapsWithin_snd_of_lt` 📖	mathematical	`card`	`intervalGapsWithin` `DFunLike.coe` `OrderEmbedding` `Lex` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Prod.Lex.instLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfFin`	—	—
`intervalGapsWithin_succ_fst_of_lt` 📖	mathematical	`card`	`intervalGapsWithin` `DFunLike.coe` `OrderEmbedding` `Lex` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Prod.Lex.instLinearOrder` `instFunLikeOrderEmbedding` `orderEmbOfFin`	—	—
`intervalGapsWithin_surjOn` 📖	mathematical	`card`	`Set.SurjOn` `intervalGapsWithin` `Set.Iio` `Nat.instPreorder` `SetLike.coe` `Finset` `instSetLike`	—	`range_orderEmbOfFin` `Fin.prop` `intervalGapsWithin_snd_of_lt` `intervalGapsWithin_succ_fst_of_lt`
`intervalGapsWithin_zero_fst` 📖	mathematical	`card`	`intervalGapsWithin`	—	—

Finset.intervalGapsWithin

Definitions

Name	Category	Theorems
`fst` 📖	CompOp	—
`snd` 📖	CompOp	—

---

← Back to Index