BundledFun

📁 Source: Mathlib/Topology/MetricSpace/BundledFun.lean

Statistics

Metric	Count
Definitions `PseudoMetric`, `IsUltra`, `instBot`, `instFunLikeForall`, `instLE`, `instMaxOfAddLeftMonoOfAddRightMono`, `instOrderBot`, `instPartialOrder`, `instSemilatticeSupOfAddLeftMonoOfAddRightMono`, `toFun`	10
Theorems `bot`, `finsetSup`, `isTrans_ball`, `isTrans_closedBall`, `isTransitiveRel_ball`, `isTransitiveRel_closedBall`, `le_sup`, `le_sup'`, `sup`, `bot_apply`, `coe_bot`, `coe_finsetSup`, `coe_le_coe`, `coe_mk`, `coe_sup`, `ext`, `ext_iff`, `finsetSup_apply`, `isSymm_ball`, `isSymm_closedBall`, `isSymmetricRel_ball`, `isSymmetricRel_closedBall`, `mk_apply`, `nonneg`, `refl`, `refl'`, `sup_apply`, `symm'`, `triangle`, `triangle'`	30
Total	40

PseudoMetric

Definitions

Name	Category	Theorems
`IsUltra` 📖	CompData	2 math math: `IsUltra.sup`, `IsUltra.bot`
`instBot` 📖	CompOp	3 math math: `IsUltra.bot`, `bot_apply`, `coe_bot`
`instFunLikeForall` 📖	CompOp	23 math math: `refl`, `IsUltra.isTransitiveRel_closedBall`, `IsUltra.isTrans_closedBall`, `IsUltra.le_sup'`, `isSymm_closedBall`, `coe_le_coe`, `isSymm_ball`, `IsUltra.isTransitiveRel_ball`, `triangle`, `IsUltra.le_sup`, `coe_mk`, `IsUltra.isTrans_ball`, `coe_sup`, `symm`, `bot_apply`, `coe_finsetSup`, `mk_apply`, `isSymmetricRel_closedBall`, `isSymmetricRel_ball`, `coe_bot`, `finsetSup_apply`, `sup_apply`, `nonneg`
`instLE` 📖	CompOp	1 math math: `coe_le_coe`
`instMaxOfAddLeftMonoOfAddRightMono` 📖	CompOp	3 math math: `IsUltra.sup`, `coe_sup`, `sup_apply`
`instOrderBot` 📖	CompOp	3 math math: `IsUltra.finsetSup`, `coe_finsetSup`, `finsetSup_apply`
`instPartialOrder` 📖	CompOp	—
`instSemilatticeSupOfAddLeftMonoOfAddRightMono` 📖	CompOp	3 math math: `IsUltra.finsetSup`, `coe_finsetSup`, `finsetSup_apply`
`toFun` 📖	CompOp	4 math math: `triangle'`, `symm'`, `refl'`, `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_apply` 📖	mathematical	—	`DFunLike.coe` `PseudoMetric` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd` `Preorder.toLE` `instFunLikeForall` `Bot.bot` `instBot`	—	—
`coe_bot` 📖	mathematical	—	`DFunLike.coe` `PseudoMetric` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd` `Preorder.toLE` `instFunLikeForall` `Bot.bot` `instBot` `Pi.instZero`	—	—
`coe_finsetSup` 📖	mathematical	`Finset.Nonempty`	`DFunLike.coe` `PseudoMetric` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeForall` `Finset.sup` `instSemilatticeSupOfAddLeftMonoOfAddRightMono` `Lattice.toSemilatticeSup` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `SemilatticeSup.toPartialOrder` `instOrderBot` `Finset.sup'`	—	`IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `Finset.sup'_eq_sup`
`coe_le_coe` 📖	mathematical	—	`Pi.hasLe` `DFunLike.coe` `PseudoMetric` `instFunLikeForall` `instLE`	—	—
`coe_mk` 📖	mathematical	—	`DFunLike.coe` `PseudoMetric` `instFunLikeForall`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `PseudoMetric` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instFunLikeForall` `instMaxOfAddLeftMonoOfAddRightMono` `Pi.instMaxForall_mathlib` `SemilatticeSup.toMax`	—	—
`ext` 📖	—	`toFun`	—	—	—
`ext_iff` 📖	mathematical	—	`toFun`	—	`ext`
`finsetSup_apply` 📖	mathematical	`Finset.Nonempty`	`DFunLike.coe` `PseudoMetric` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instFunLikeForall` `Finset.sup` `instSemilatticeSupOfAddLeftMonoOfAddRightMono` `Lattice.toSemilatticeSup` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `SemilatticeSup.toPartialOrder` `instOrderBot` `Finset.sup'`	—	`Finset.Nonempty.cons_induction` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `Finset.sup_singleton` `Finset.cons_nonempty` `Finset.sup_cons` `Finset.sup'_cons`
`isSymm_ball` 📖	mathematical	—	`SetRel.IsSymm` `setOf` `Preorder.toLT` `DFunLike.coe` `PseudoMetric` `Preorder.toLE` `instFunLikeForall`	—	`symm`
`isSymm_closedBall` 📖	mathematical	—	`SetRel.IsSymm` `setOf` `DFunLike.coe` `PseudoMetric` `instFunLikeForall`	—	`symm`
`isSymmetricRel_ball` 📖	mathematical	—	`SetRel.IsSymm` `setOf` `Preorder.toLT` `DFunLike.coe` `PseudoMetric` `Preorder.toLE` `instFunLikeForall`	—	`isSymm_ball`
`isSymmetricRel_closedBall` 📖	mathematical	—	`SetRel.IsSymm` `setOf` `DFunLike.coe` `PseudoMetric` `instFunLikeForall`	—	`isSymm_closedBall`
`mk_apply` 📖	mathematical	—	`DFunLike.coe` `PseudoMetric` `instFunLikeForall`	—	—
`nonneg` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DFunLike.coe` `PseudoMetric` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `instFunLikeForall`	—	`triangle'` `add_lt_add` `covariant_swap_add_of_covariant_add` `symm` `add_zero` `LT.lt.ne` `refl`
`refl` 📖	mathematical	—	`DFunLike.coe` `PseudoMetric` `instFunLikeForall`	—	`refl'`
`refl'` 📖	mathematical	—	`toFun`	—	—
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `PseudoMetric` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `instFunLikeForall` `instMaxOfAddLeftMonoOfAddRightMono` `SemilatticeSup.toMax`	—	—
`symm'` 📖	mathematical	—	`toFun`	—	—
`triangle` 📖	mathematical	—	`DFunLike.coe` `PseudoMetric` `instFunLikeForall`	—	`triangle'`
`triangle'` 📖	mathematical	—	`toFun`	—	—

PseudoMetric.IsUltra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot` 📖	mathematical	—	`PseudoMetric.IsUltra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax` `Bot.bot` `PseudoMetric` `PseudoMetric.instBot`	—	`sup_of_le_left`
`finsetSup` 📖	mathematical	`PseudoMetric.IsUltra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	`Finset.sup` `PseudoMetric` `PseudoMetric.instSemilatticeSupOfAddLeftMonoOfAddRightMono` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `SemilatticeSup.toPartialOrder` `PseudoMetric.instOrderBot`	—	`IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `Finset.eq_empty_or_nonempty` `Finset.sup_empty` `max_self` `PseudoMetric.finsetSup_apply` `Finset.sup'_le` `le_sup'`
`isTrans_ball` 📖	mathematical	—	`SetRel.IsTrans` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `PseudoMetric` `Preorder.toLE` `PseudoMetric.instFunLikeForall`	—	`LE.le.trans_lt` `le_sup` `max_lt`
`isTrans_closedBall` 📖	mathematical	—	`SetRel.IsTrans` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `DFunLike.coe` `PseudoMetric` `PseudoMetric.instFunLikeForall`	—	`LE.le.trans` `le_sup` `sup_le`
`isTransitiveRel_ball` 📖	mathematical	—	`SetRel.IsTrans` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `PseudoMetric` `Preorder.toLE` `PseudoMetric.instFunLikeForall`	—	`isTrans_ball`
`isTransitiveRel_closedBall` 📖	mathematical	—	`SetRel.IsTrans` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `DFunLike.coe` `PseudoMetric` `PseudoMetric.instFunLikeForall`	—	`isTrans_closedBall`
`le_sup` 📖	mathematical	—	`DFunLike.coe` `PseudoMetric` `PseudoMetric.instFunLikeForall`	—	`le_sup'`
`le_sup'` 📖	mathematical	—	`DFunLike.coe` `PseudoMetric` `PseudoMetric.instFunLikeForall`	—	—
`sup` 📖	mathematical	—	`PseudoMetric.IsUltra` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatticeSup.toMax` `PseudoMetric` `PseudoMetric.instMaxOfAddLeftMonoOfAddRightMono`	—	`sup_le_sup` `le_sup` `sup_left_comm` `sup_comm`

(root)

Definitions

Name	Category	Theorems
`PseudoMetric` 📖	CompData	26 math math: `PseudoMetric.IsUltra.sup`, `PseudoMetric.refl`, `PseudoMetric.IsUltra.isTransitiveRel_closedBall`, `PseudoMetric.IsUltra.isTrans_closedBall`, `PseudoMetric.IsUltra.bot`, `PseudoMetric.IsUltra.le_sup'`, `PseudoMetric.isSymm_closedBall`, `PseudoMetric.coe_le_coe`, `PseudoMetric.isSymm_ball`, `PseudoMetric.IsUltra.isTransitiveRel_ball`, `PseudoMetric.IsUltra.finsetSup`, `PseudoMetric.triangle`, `PseudoMetric.IsUltra.le_sup`, `PseudoMetric.coe_mk`, `PseudoMetric.IsUltra.isTrans_ball`, `PseudoMetric.coe_sup`, `PseudoMetric.symm`, `PseudoMetric.bot_apply`, `PseudoMetric.coe_finsetSup`, `PseudoMetric.mk_apply`, `PseudoMetric.isSymmetricRel_closedBall`, `PseudoMetric.isSymmetricRel_ball`, `PseudoMetric.coe_bot`, `PseudoMetric.finsetSup_apply`, `PseudoMetric.sup_apply`, `PseudoMetric.nonneg`

---

← Back to Index