FredholmAlternative

📁 Source: Mathlib/Analysis/Normed/Operator/FredholmAlternative.lean

Statistics

Metric	Count
Definitions	0
Theorems antilipschitz_of_not_hasEigenvalue, hasEigenvalue_iff_mem_spectrum, hasEigenvalue_or_mem_resolventSet	3
Total	3

IsCompactOperator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antilipschitz_of_not_hasEigenvalue 📖	mathematical	IsCompactOperator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain ContinuousLinearMap.toLinearMap	NNReal AntilipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike ContinuousLinearMap.sub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Ring.toSemiring CommRing.toRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul ContinuousLinearMap.one	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul antilipschitzWith_iff_exists_mul_le_norm DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq Mathlib.Tactic.Push.not_forall_eq NormedField.exists_one_lt_norm inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing lt_trans Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one map_zero AddMonoidHomClass.toZeroHomClass smul_zero sub_self norm_zero MulZeroClass.mul_zero rescale_to_shell Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike LT.lt.le one_div map_smul SemilinearMapClass.toMulActionSemiHomClass norm_smul NormedSpace.toNormSMulClass lt_imp_lt_of_le_of_le mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono le_of_lt norm_pos_iff le_refl mul_left_comm Mathlib.Tactic.LinearCombination.lt_of_lt Real.instIsOrderedCancelAddMonoid Mathlib.Tactic.LinearCombination.mul_const_lt Mathlib.Tactic.LinearCombination.le_rearrange Real.instIsOrderedAddMonoid Mathlib.Tactic.Ring.le_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero exists_seq_strictAnti_tendsto instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered instNoMaxOrderOfNontrivial TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace squeeze_zero_norm Nat.instAtLeastTwoHAddOfNat div_pos mul_pos Mathlib.Meta.NormNum.instAtLeastTwo Filter.mp_mem Filter.Tendsto.eventually_le_const instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Filter.univ_mem' norm_le_norm_add_norm_sub Mathlib.Tactic.LinearCombination.le_of_lt add_lt_add_of_lt_of_le IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE contravariant_lt_of_covariant_le covariant_swap_add_of_covariant_add add_lt_add_of_le_of_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono Mathlib.Tactic.LinearCombination.mul_const_le Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz image_closedBall_subset_compact IsCompact.tendsto_subseq dist_zero_right map_sub Filter.Tendsto.comp ContinuousAt.tendsto Continuous.continuousAt ContinuousLinearMap.continuous tendsto_nhds_unique TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder StarOrderedRing.toIsOrderedRing Nat.instStarOrderedRing instArchimedeanNat Continuous.clm_apply continuous_const continuous_id' StrictMono.tendsto_atTop NormedAddGroup.tendsto_nhds_zero Filter.Tendsto.eventually Filter.eventually_const Module.End.hasEigenvalue_of_hasEigenvector
hasEigenvalue_iff_mem_spectrum 📖	mathematical	IsCompactOperator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike	Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set Set.instMembership spectrum ContinuousLinearMap Semifield.toCommSemiring ContinuousLinearMap.ring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul AddCommGroup.toAddCommMonoid IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul ContinuousLinearMap.spectrum_eq Module.End.HasEigenvalue.mem_spectrum hasEigenvalue_or_mem_resolventSet
hasEigenvalue_or_mem_resolventSet 📖	mathematical	IsCompactOperator NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike	Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set Set.instMembership resolventSet ContinuousLinearMap Semifield.toCommSemiring ContinuousLinearMap.ring NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.algebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul AddCommGroup.toAddCommMonoid IsBoundedSMul.toUniformContinuousConstSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedSpace.toIsBoundedSMul	—	SeminormedAddCommGroup.toIsTopologicalAddGroup smulCommClass_self IsScalarTower.left UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul antilipschitz_of_not_hasEigenvalue ContinuousLinearMap.ext neg_sub ContinuousLinearMap.isUnit_iff_bijective IsUnit.neg_iff spectrum.mem_resolventSet_iff NormedField.exists_one_lt_norm RingHomSurjective.ids AntilipschitzWith.isClosedEmbedding ContinuousLinearMap.uniformContinuous SeminormedAddCommGroup.to_isUniformAddGroup IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike OrderHom.monotone RingHomCompTriple.ids Module.End.iterate_succ' LinearMap.range_comp Pairwise.of_lt smul_sub smul_inv_smul₀ Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.eq_rearrange Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower AddCommGroup.intIsScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval₁ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval₃ sub_zero Mathlib.Tactic.Module.NF.add_eq_eval₁ Mathlib.Tactic.Module.NF.add_eq_eval₂ add_zero Mathlib.Tactic.Module.NF.sub_eq_eval₂ Mathlib.Tactic.Module.NF.zero_eq_eval Mathlib.Tactic.Module.NF.eq_cons_const eq_natCast RingHom.instRingHomClass Nat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_congr 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero eq_intCast Int.cast_one Int.cast_neg Mathlib.Tactic.Ring.add_congr Submodule.smul_mem Submodule.add_mem Submodule.sub_mem LT.lt.le le_rfl norm_smul NormedSpace.toNormSMulClass mul_comm le_imp_le_of_le_of_le le_refl mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing le_of_lt norm_pos_iff one_mul image_closedBall_subset_compact IsCompact.tendsto_subseq TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace dist_zero_right Filter.Tendsto.cauchySeq Metric.cauchySeq_iff' Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT Nat.instIsOrderedCancelAddMonoid Nat.instCanonicallyOrderedAdd dist_eq_norm_sub LT.lt.not_ge StrictMono.injective

---

← Back to Index