Documentation Verification Report

BetweenList

📁 Source: Mathlib/Analysis/Convex/BetweenList.lean

Statistics

Metric	Count
Definitions `Sbtw`, `Wbtw`	2
Theorems `list_sbtw_map_iff`, `list_wbtw_map_iff`, `list_sbtw_map_iff`, `list_wbtw_map_iff`, `pairwise_ne`, `wbtw`, `sbtw`, `wbtw`, `wbtw`, `sbtw`, `map`, `exists_map_eq_of_sorted_iff_sbtw`, `exists_map_eq_of_sorted_iff_wbtw`, `exists_map_eq_of_sorted_nonempty_iff_sbtw`, `exists_map_eq_of_sorted_nonempty_iff_wbtw`, `sbtw_cons`, `sbtw_four`, `sbtw_iff_triplewise_and_ne_pair`, `sbtw_nil`, `sbtw_pair`, `sbtw_singleton`, `sbtw_triple`, `wbtw_cons`, `wbtw_four`, `wbtw_nil`, `wbtw_pair`, `wbtw_singleton`, `wbtw_triple`	28
Total	30

AffineEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`list_sbtw_map_iff` 📖	mathematical	—	`List.Sbtw` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	`injective` `Function.Injective.list_sbtw_map_iff`
`list_wbtw_map_iff` 📖	mathematical	—	`List.Wbtw` `DFunLike.coe` `AffineEquiv` `EquivLike.toFunLike` `equivLike`	—	`injective` `Function.Injective.list_wbtw_map_iff`

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`list_sbtw_map_iff` 📖	mathematical	`DFunLike.coe` `AffineMap` `AffineMap.instFunLike`	`List.Sbtw`	—	`List.Sbtw.eq_1` `list_wbtw_map_iff`
`list_wbtw_map_iff` 📖	mathematical	`DFunLike.coe` `AffineMap` `AffineMap.instFunLike`	`List.Wbtw`	—	`List.Triplewise.of_map` `wbtw_map_iff` `List.Wbtw.map`

List

Definitions

Name	Category	Theorems
`Sbtw` 📖	MathDef	13 math math: `sbtw_cons`, `Function.Injective.list_sbtw_map_iff`, `sbtw_four`, `exists_map_eq_of_sorted_nonempty_iff_sbtw`, `sbtw_singleton`, `exists_map_eq_of_sorted_iff_sbtw`, `Sorted.sbtw`, `sbtw_iff_triplewise_and_ne_pair`, `sbtw_pair`, `sbtw_nil`, `SortedLT.sbtw`, `AffineEquiv.list_sbtw_map_iff`, `sbtw_triple`
`Wbtw` 📖	MathDef	13 math math: `wbtw_pair`, `SortedLE.wbtw`, `Sbtw.wbtw`, `wbtw_four`, `exists_map_eq_of_sorted_nonempty_iff_wbtw`, `AffineEquiv.list_wbtw_map_iff`, `wbtw_cons`, `wbtw_nil`, `exists_map_eq_of_sorted_iff_wbtw`, `Sorted.wbtw`, `wbtw_singleton`, `wbtw_triple`, `Function.Injective.list_wbtw_map_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_map_eq_of_sorted_iff_sbtw` 📖	mathematical	—	`SortedLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `AffineMap` `DivisionRing.toRing` `Field.toDivisionRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap` `Sbtw`	—	`Function.Injective.list_sbtw_map_iff` `AffineMap.lineMap_injective` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `SortedLT.sbtw` `exists_pair_ne` `exists_ne` `instIsEmptyFalse` `AffineMap.lineMap_apply_zero` `exists_map_eq_of_sorted_nonempty_iff_sbtw`
`exists_map_eq_of_sorted_iff_wbtw` 📖	mathematical	—	`SortedLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `AffineMap` `DivisionRing.toRing` `Field.toDivisionRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap` `Wbtw`	—	`Wbtw.map` `SortedLE.wbtw` `AddTorsor.nonempty` `AffineMap.lineMap_same` `exists_map_eq_of_sorted_nonempty_iff_wbtw`
`exists_map_eq_of_sorted_nonempty_iff_sbtw` 📖	mathematical	—	`SortedLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `AffineMap` `DivisionRing.toRing` `Field.toDivisionRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap` `Sbtw`	—	`exists_map_eq_of_sorted_nonempty_iff_wbtw` `Pairwise.sortedLE` `LT.lt.le` `SortedLT.pairwise` `AffineMap.lineMap_injective` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `LT.lt.ne` `Sbtw.eq_1` `Pairwise.sortedLT` `lt_iff_le_and_ne` `SortedLE.pairwise` `AddRightCancelSemigroup.toIsRightCancelAdd`
`exists_map_eq_of_sorted_nonempty_iff_wbtw` 📖	mathematical	—	`SortedLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `AffineMap` `DivisionRing.toRing` `Field.toDivisionRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap` `Wbtw`	—	`Wbtw.map` `SortedLE.wbtw` `instIsEmptyFalse` `AffineMap.lineMap_same` `wbtw_cons` `IsStrictOrderedRing.toZeroLEOneClass` `AffineMap.lineMap_apply_zero` `AffineMap.lineMap_apply_one` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `add_le_add_right` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `SortedLE.pairwise` `AffineMap.lineMap_lineMap_left` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `add_zero` `Mathlib.Tactic.RingNF.add_assoc_rev` `Mathlib.Tactic.RingNF.add_neg`
`sbtw_cons` 📖	mathematical	—	`Sbtw` `Sbtw`	—	`sbtw_iff_triplewise_and_ne_pair` `triplewise_cons` `instIsEmptyFalse`
`sbtw_four` 📖	mathematical	—	`Sbtw` `Sbtw`	—	`instIsEmptyFalse`
`sbtw_iff_triplewise_and_ne_pair` 📖	mathematical	—	`Sbtw` `Triplewise` `Sbtw`	—	`Sbtw.eq_1` `wbtw_cons` `triplewise_cons` `Sbtw.wbtw` `Triplewise.imp` `instIsEmptyFalse`
`sbtw_nil` 📖	mathematical	—	`Sbtw`	—	—
`sbtw_pair` 📖	mathematical	—	`Sbtw`	—	`instIsEmptyFalse`
`sbtw_singleton` 📖	mathematical	—	`Sbtw`	—	`instIsEmptyFalse`
`sbtw_triple` 📖	mathematical	—	`Sbtw` `Sbtw`	—	`instIsEmptyFalse` `Sbtw.left_ne_right`
`wbtw_cons` 📖	mathematical	—	`Wbtw` `Wbtw`	—	`triplewise_cons`
`wbtw_four` 📖	mathematical	—	`Wbtw` `Wbtw`	—	`instIsEmptyFalse`
`wbtw_nil` 📖	mathematical	—	`Wbtw`	—	—
`wbtw_pair` 📖	mathematical	—	`Wbtw`	—	—
`wbtw_singleton` 📖	mathematical	—	`Wbtw`	—	—
`wbtw_triple` 📖	mathematical	—	`Wbtw` `Wbtw`	—	—

List.Sbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pairwise_ne` 📖	—	`List.Sbtw`	—	—	—
`wbtw` 📖	mathematical	`List.Sbtw`	`List.Wbtw`	—	—

List.Sorted

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sbtw` 📖	mathematical	`List.SortedLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`List.Sbtw` `DivisionRing.toRing` `Field.toDivisionRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`List.SortedLT.sbtw`
`wbtw` 📖	mathematical	`List.SortedLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`List.Wbtw` `DivisionRing.toRing` `Field.toDivisionRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`List.SortedLE.wbtw`

List.SortedLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`wbtw` 📖	mathematical	`List.SortedLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`List.Wbtw` `DivisionRing.toRing` `Field.toDivisionRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`List.wbtw_cons` `Wbtw.of_le_of_le` `List.Pairwise.sortedLE` `pairwise`

List.SortedLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sbtw` 📖	mathematical	`List.SortedLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`List.Sbtw` `DivisionRing.toRing` `Field.toDivisionRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`List.SortedLE.wbtw` `sortedLE` `nodup`

List.Wbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	`List.Wbtw`	`DFunLike.coe` `AffineMap` `AffineMap.instFunLike`	—	`List.Triplewise.map` `Wbtw.map`

---

← Back to Index