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.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	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	Norm.norm NormedAddCommGroup.toNorm 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.instLE NormedAddCommGroup.toNorm 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