Documentation Verification Report

Lattice

📁 Source: Mathlib/Analysis/Normed/Order/Lattice.lean

Statistics

Metric	Count
Definitions `HasSolidNorm`	1
Theorems `continuousInf`, `continuousSup`, `orderClosedTopology`, `solid`, `toTopologicalLattice`, `hasSolidNorm`, `isSolid_ball`, `instHasSolidNorm`, `continuous_negPart`, `continuous_posPart`, `dual_solid`, `instHasSolidNormRat`, `instHasSolidNormReal`, `isClosed_le_of_isClosed_nonneg`, `isClosed_nonneg`, `lipschitzWith_negPart`, `lipschitzWith_posPart`, `lipschitzWith_sup_right`, `norm_abs_eq_norm`, `norm_abs_sub_abs`, `norm_inf_le_add`, `norm_inf_sub_inf_le_add_norm`, `norm_inf_sub_inf_le_norm`, `norm_le_norm_of_abs_le_abs`, `norm_sup_le_add`, `norm_sup_sub_sup_le_add_norm`, `norm_sup_sub_sup_le_norm`	27
Total	28

HasSolidNorm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousInf` 📖	mathematical	—	`ContinuousInf` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`continuous_iff_continuousAt` `tendsto_iff_norm_sub_tendsto_zero` `norm_inf_sub_inf_le_add_norm` `squeeze_zero` `norm_nonneg` `sub_self` `norm_zero` `add_zero` `Filter.Tendsto.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Filter.Tendsto.norm` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Continuous.tendsto` `continuous_fst` `tendsto_const_nhds` `continuous_snd`
`continuousSup` 📖	mathematical	—	`ContinuousSup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`OrderDual.continuousSup` `continuousInf` `OrderDual.instHasSolidNorm` `OrderDual.isOrderedAddMonoid` `ESeminormedAddCommMonoid.add_comm`
`orderClosedTopology` 📖	mathematical	—	`OrderClosedTopology` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	`isClosed_le_of_isClosed_nonneg` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `isClosed_nonneg`
`solid` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `abs` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm`	—	—
`toTopologicalLattice` 📖	mathematical	—	`TopologicalLattice` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`continuousInf` `continuousSup`

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSolidNorm` 📖	mathematical	—	`HasSolidNorm` `instNormedAddCommGroup` `instLatticeInt`	—	`Real.instIsStrictOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero`

LatticeOrderedAddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSolid_ball` 📖	mathematical	—	`IsSolid` `NormedAddCommGroup.toAddCommGroup` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`mem_ball_zero_iff` `LE.le.trans_lt` `HasSolidNorm.solid`

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasSolidNorm` 📖	mathematical	—	`HasSolidNorm` `OrderDual` `normedAddCommGroup` `instLattice`	—	`dual_solid`

(root)

Definitions

Name	Category	Theorems
`HasSolidNorm` 📖	CompData	6 math math: `MeasureTheory.Lp.instHasSolidNorm`, `instHasSolidNormReal`, `OrderDual.instHasSolidNorm`, `BoundedContinuousFunction.instHasSolidNorm`, `instHasSolidNormRat`, `Int.hasSolidNorm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_negPart` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegPart.negPart` `instNegPart` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`LipschitzWith.continuous` `lipschitzWith_negPart`
`continuous_posPart` 📖	mathematical	—	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `PosPart.posPart` `instPosPart` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`LipschitzWith.continuous` `lipschitzWith_posPart`
`dual_solid` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `SemilatticeInf.toMin` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`HasSolidNorm.solid` `abs.eq_1` `neg_neg` `neg_inf` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `neg_le_neg_iff` `inf_comm`
`instHasSolidNormRat` 📖	mathematical	—	`HasSolidNorm` `Rat.instNormedAddCommGroup` `Rat.instLattice`	—	`Real.instIsStrictOrderedRing`
`instHasSolidNormReal` 📖	mathematical	—	`HasSolidNorm` `Real` `Real.normedAddCommGroup` `Real.lattice`	—	—
`isClosed_le_of_isClosed_nonneg` 📖	mathematical	—	`IsClosed` `instTopologicalSpaceProd` `setOf` `Preorder.toLE` `PartialOrder.toPreorder`	—	`Set.ext` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsClosed.preimage` `Continuous.sub` `continuous_snd` `continuous_fst`
`isClosed_nonneg` 📖	mathematical	—	`IsClosed` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `setOf` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Set.ext` `IsOrderedAddMonoid.toAddLeftMono` `IsClosed.preimage` `continuous_negPart` `isClosed_singleton` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`lipschitzWith_negPart` 📖	mathematical	—	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NNReal` `instOneNNReal` `NegPart.negPart` `instNegPart` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`one_mul` `LipschitzWith.comp` `lipschitzWith_posPart` `LipschitzWith.neg` `LipschitzWith.id`
`lipschitzWith_posPart` 📖	mathematical	—	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NNReal` `instOneNNReal` `PosPart.posPart` `instPosPart` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`lipschitzWith_sup_right`
`lipschitzWith_sup_right` 📖	mathematical	—	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `NNReal` `instOneNNReal` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`LipschitzWith.of_dist_le_mul` `NNReal.coe_one` `one_mul` `dist_eq_norm` `norm_sup_sub_sup_le_norm`
`norm_abs_eq_norm` 📖	mathematical	—	`Norm.norm` `NormedAddCommGroup.toNorm` `abs` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`LE.le.antisymm` `HasSolidNorm.solid` `Eq.le` `abs_abs` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`norm_abs_sub_abs` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `abs`	—	`HasSolidNorm.solid` `abs_abs_sub_abs_le` `IsOrderedAddMonoid.toAddLeftMono`
`norm_inf_le_add` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `Real.instAdd`	—	`norm_inf_sub_inf_le_add_norm` `inf_idem` `sub_zero`
`norm_inf_sub_inf_le_add_norm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `Real.instAdd`	—	`norm_abs_eq_norm` `le_trans` `HasSolidNorm.solid` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `add_nonneg` `abs_nonneg` `covariant_swap_add_of_covariant_add` `sub_add_sub_cancel` `abs_add_le` `add_le_add` `abs_inf_sub_inf_le_abs` `inf_comm` `norm_add_le`
`norm_inf_sub_inf_le_norm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`HasSolidNorm.solid` `abs_inf_sub_inf_le_abs` `IsOrderedAddMonoid.toAddLeftMono`
`norm_le_norm_of_abs_le_abs` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `abs` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`HasSolidNorm.solid`
`norm_sup_le_add` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `Real.instAdd`	—	`norm_sup_sub_sup_le_add_norm` `sup_idem` `sub_zero`
`norm_sup_sub_sup_le_add_norm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `Real.instAdd`	—	`norm_abs_eq_norm` `le_trans` `HasSolidNorm.solid` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `add_nonneg` `abs_nonneg` `covariant_swap_add_of_covariant_add` `sub_add_sub_cancel` `abs_add_le` `add_le_add` `abs_sup_sub_sup_le_abs` `sup_comm` `norm_add_le`
`norm_sup_sub_sup_le_norm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`HasSolidNorm.solid` `abs_sup_sub_sup_le_abs` `IsOrderedAddMonoid.toAddLeftMono`

---

← Back to Index