Connected

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

Statistics

Metric	Count
Definitions	0
Theorems ball_contractible, contractibleSpace_ball, contractibleSpace_closedBall, contractibleSpace_closedEBall, contractibleSpace_eball, eball_contractible, isConnected_ball, isConnected_closedBall, isConnected_closedEBall, isConnected_eball, isPathConnected_ball, isPathConnected_closedBall, isPathConnected_closedEBall, isPathConnected_eball, isPreconnected_ball, isPreconnected_closedBall, isPreconnected_closedEBall, isPreconnected_eball, isConnected_compl_of_one_lt_rank, isPathConnected_compl_of_one_lt_rank, connectedComponentIn_eq_self_of_one_lt_codim, isConnected_compl_of_one_lt_codim, isConnected_compl_singleton_of_one_lt_rank, isConnected_sphere, isPathConnected_compl_of_one_lt_codim, isPathConnected_compl_singleton_of_one_lt_rank, isPathConnected_sphere, isPreconnected_sphere	28
Total	28

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ball_contractible 📖	mathematical	Real Real.instLT Real.instZero	ContractibleSpace Set.Elem ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	contractibleSpace_ball
contractibleSpace_ball 📖	mathematical	Real Real.instLT Real.instZero	ContractibleSpace Set.Elem ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Convex.contractibleSpace IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_ball
contractibleSpace_closedBall 📖	mathematical	Real Real.instLE Real.instZero	ContractibleSpace Set.Elem closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Convex.contractibleSpace IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_closedBall
contractibleSpace_closedEBall 📖	mathematical	—	ContractibleSpace Set.Elem closedEBall EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	Convex.contractibleSpace IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_closedEBall PseudoEMetricSpace.edist_self ENNReal.instCanonicallyOrderedAdd
contractibleSpace_eball 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	ContractibleSpace Set.Elem eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	Convex.contractibleSpace IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_eball PseudoEMetricSpace.edist_self
eball_contractible 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	ContractibleSpace Set.Elem eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	—	contractibleSpace_eball
isConnected_ball 📖	mathematical	Real Real.instLT Real.instZero	IsConnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ball	—	IsPathConnected.isConnected isPathConnected_ball
isConnected_closedBall 📖	mathematical	Real Real.instLE Real.instZero	IsConnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup closedBall	—	dist_self isPreconnected_closedBall
isConnected_closedEBall 📖	mathematical	—	IsConnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup closedEBall EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	mem_closedEBall_self isPreconnected_closedEBall
isConnected_eball 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	IsConnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	IsPathConnected.isConnected isPathConnected_eball
isPathConnected_ball 📖	mathematical	Real Real.instLT Real.instZero	IsPathConnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ball	—	Convex.isPathConnected IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_ball
isPathConnected_closedBall 📖	mathematical	Real Real.instLE Real.instZero	IsPathConnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup closedBall	—	Convex.isPathConnected IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_closedBall dist_self
isPathConnected_closedEBall 📖	mathematical	—	IsPathConnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup closedEBall EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	isPathConnected_iff_pathConnectedSpace ContractibleSpace.instPathConnectedSpace contractibleSpace_closedEBall
isPathConnected_eball 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	IsPathConnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	Convex.isPathConnected IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_eball PseudoEMetricSpace.edist_self
isPreconnected_ball 📖	mathematical	—	IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ball	—	Convex.isPreconnected IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_ball
isPreconnected_closedBall 📖	mathematical	—	IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup closedBall	—	Convex.isPreconnected IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_closedBall
isPreconnected_closedEBall 📖	mathematical	—	IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup closedEBall EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	Convex.isPreconnected IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_closedEBall
isPreconnected_eball 📖	mathematical	—	IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup eball EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	Convex.isPreconnected IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_eball

Set.Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isConnected_compl_of_one_lt_rank 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instOne Module.rank Real Real.semiring AddCommGroup.toAddCommMonoid	IsConnected Compl.compl Set Set.instCompl	—	IsPathConnected.isConnected isPathConnected_compl_of_one_lt_rank
isPathConnected_compl_of_one_lt_rank 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instOne Module.rank Real Real.semiring AddCommGroup.toAddCommMonoid	IsPathConnected Compl.compl Set Set.instCompl	—	rank_pos_iff_nontrivial Real.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors LT.lt.trans zero_lt_one IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing NeZero.charZero_one Cardinal.instCharZero Dense.nonempty Nontrivial.to_nonempty dense_compl Real.instCompleteSpace eq_or_ne JoinedIn.refl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval Mathlib.Tactic.Module.NF.sub_eq_eval Mathlib.Tactic.Module.NF.smul_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval Mathlib.Tactic.Module.NF.atom_eq_eval Mathlib.Tactic.Module.NF.add_eq_eval₁ zero_add Mathlib.Tactic.Module.NF.eval_algebraMap AddCommMonoid.nat_isScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval₃ sub_zero AddCommGroup.intIsScalarTower Mathlib.Tactic.Module.NF.sub_eq_eval₂ Mathlib.Tactic.Module.NF.zero_sub_eq_eval Mathlib.Tactic.Module.NF.eq_cons_cons eq_natCast RingHom.instRingHomClass Nat.cast_one eq_intCast Int.cast_neg Int.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one 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_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.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Module.NF.eq_cons_const Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Module.NF.add_eq_eval₂ Mathlib.Tactic.Ring.add_congr sub_ne_zero exists_linearIndependent_pair_of_one_lt_rank DivisionRing.hasRankNullity IsNoetherianRing.strongRankCondition Real.instNontrivial PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain Set.countable_setOf_nonempty_of_disjoint Set.disjoint_iff_inter_eq_empty Set.inter_assoc Set.inter_comm Set.inter_self Set.subset_empty_iff Set.inter_subset_inter_left Eq.subset Set.instReflSubset segment_inter_eq_endpoint_of_linearIndependent_of_ne Real.instIsOrderedRing Set.inter_subset_right sub_eq_add_neg Matrix.cons_val_succ Matrix.cons_val_fin_one Units.neg_smul one_smul LinearIndependent.units_smul IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul union JoinedIn.of_segment_subset Set.subset_compl_iff_disjoint_right Set.compl_union JoinedIn.trans JoinedIn.symm

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
connectedComponentIn_eq_self_of_one_lt_codim 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instOne Module.rank Real HasQuotient.Quotient Submodule Real.semiring AddCommGroup.toAddCommMonoid hasQuotient Real.instRing Quotient.addCommGroup Quotient.module SetLike.instMembership setLike	connectedComponentIn Compl.compl Set Set.instCompl SetLike.coe	—	IsPreconnected.connectedComponentIn isConnected_compl_of_one_lt_codim

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isConnected_compl_of_one_lt_codim 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instOne Module.rank Real HasQuotient.Quotient Submodule Real.semiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient Real.instRing Submodule.Quotient.addCommGroup Submodule.Quotient.module	IsConnected Compl.compl Set Set.instCompl SetLike.coe Submodule.setLike	—	IsPathConnected.isConnected isPathConnected_compl_of_one_lt_codim
isConnected_compl_singleton_of_one_lt_rank 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instOne Module.rank Real Real.semiring AddCommGroup.toAddCommMonoid	IsConnected Compl.compl Set Set.instCompl Set.instSingletonSet	—	IsPathConnected.isConnected isPathConnected_compl_singleton_of_one_lt_rank
isConnected_sphere 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instOne Module.rank Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Real.instLE Real.instZero	IsConnected Metric.sphere	—	IsPathConnected.isConnected isPathConnected_sphere
isPathConnected_compl_of_one_lt_codim 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instOne Module.rank Real HasQuotient.Quotient Submodule Real.semiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient Real.instRing Submodule.Quotient.addCommGroup Submodule.Quotient.module	IsPathConnected Compl.compl Set Set.instCompl SetLike.coe Submodule.setLike	—	Submodule.exists_isCompl isPathConnected_compl_of_isPathConnected_compl_zero IsTopologicalAddGroup.toContinuousAdd IsCompl.symm isPathConnected_compl_singleton_of_one_lt_rank Submodule.topologicalAddGroup SMulMemClass.continuousSMul Submodule.smulMemClass LinearEquiv.rank_eq
isPathConnected_compl_singleton_of_one_lt_rank 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instOne Module.rank Real Real.semiring AddCommGroup.toAddCommMonoid	IsPathConnected Compl.compl Set Set.instCompl Set.instSingletonSet	—	Set.Countable.isPathConnected_compl_of_one_lt_rank Set.countable_singleton
isPathConnected_sphere 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instOne Module.rank Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Real.instLE Real.instZero	IsPathConnected Metric.sphere	—	LE.le.eq_or_lt Metric.sphere_zero isPathConnected_singleton ContinuousAt.continuousWithinAt ContinuousAt.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup continuousAt_const ContinuousAt.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousAt.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousAt.inv₀ IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal ContinuousAt.norm continuousAt_id isPathConnected_compl_singleton_of_one_lt_rank IsPathConnected.image' Set.Subset.antisymm add_sub_cancel_left norm_smul NormedSpace.toNormSMulClass norm_mul NormedDivisionRing.toNormMulClass abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid norm_inv norm_norm mul_assoc inv_mul_cancel₀ mul_one LT.lt.ne sub_self norm_zero mem_sphere_iff_norm mul_inv_cancel₀ LT.lt.ne' one_smul add_sub_cancel
isPreconnected_sphere 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.instOne Module.rank Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField	IsPreconnected Metric.sphere	—	le_or_gt IsConnected.isPreconnected isConnected_sphere Metric.sphere_eq_empty_of_neg isPreconnected_empty

---

← Back to Index