Documentation Verification Report

RieszLemma

📁 Source: Mathlib/Analysis/Normed/Module/RieszLemma.lean

Statistics

Metric	Count
Definitions	0
Theorems `closedBall_infDist_compl_subset_closure`, `riesz_lemma`, `riesz_lemma_of_lt_one`, `riesz_lemma_of_norm_lt`	4
Total	4

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closedBall_infDist_compl_subset_closure` 📖	mathematical	`Set` `Set.instMembership`	`Set` `Set.instHasSubset` `closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `infDist` `Compl.compl` `Set.instCompl` `closure` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`eq_or_ne` `closedBall_zero'` `closure_mono` `Set.singleton_subset_iff` `closure_ball` `ball_infDist_compl_subset`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`riesz_lemma` 📖	mathematical	`Subspace` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Real` `Real.instLT` `Real.instOne`	`Subspace` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Real` `Real.instLE` `Real.instMul` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`Submodule.zero_mem` `lt_of_le_of_ne` `Metric.infDist_nonneg` `IsClosed.mem_iff_infDist_zero` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isNNRat_lt_true` `Real.instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_one` `lt_of_lt_of_le` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsOrderedRing` `Real.instNontrivial` `le_max_right` `lt_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `mul_lt_iff_lt_one_right` `Metric.infDist_lt_iff` `Submodule.add_mem` `sub_eq_add_neg` `neg_add_cancel_right` `le_of_lt` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `le_max_left` `norm_nonneg` `dist_eq_norm` `lt_div_iff₀'` `Metric.infDist_le_dist_of_mem` `sub_sub`
`riesz_lemma_of_lt_one` 📖	mathematical	`Subspace` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Real` `Real.instLT` `Real.instOne`	`Subspace` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `Real` `Real.instOne` `Real.instLE` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`riesz_lemma` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Submodule.smul_mem_iff` `IsScalarTower.left` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `norm_smul_inv_norm` `norm_smul` `NormedSpace.toNormSMulClass` `norm_inv` `norm_algebraMap'` `NormedDivisionRing.to_normOneClass` `norm_norm` `Submodule.smul_mem` `inv_smul_smul₀` `smul_sub` `le_inv_mul_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing`
`riesz_lemma_of_norm_lt` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Norm.norm` `NormedField.toNorm` `Subspace` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `AddCommGroup.toAddCommMonoid`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.instOne` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`LE.le.trans_lt` `norm_nonneg` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `one_mul` `riesz_lemma` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `rescale_to_shell` `LT.lt.le` `smul_smul` `mul_inv_cancel₀` `one_smul` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `lt_trans` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_pos` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `norm_smul` `NormedSpace.toNormSMulClass` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Submodule.smul_mem` `norm_pos_iff` `smul_sub`

---

← Back to Index