Perfect

📁 Source: Mathlib/Topology/Perfect.lean

Statistics

Metric	Count
Definitions Perfect, Perfect, Preperfect	3
Theorems nhds_inter, preperfect_of_nontrivial, acc, closed, closure_nhds_inter, splitting, not_isolated, univ_perfect, univ_preperfect, open_inter, perfect_closure, exists_countable_union_perfect_of_isClosed, exists_perfect_nonempty_of_isClosed_of_not_countable, instPerfectSpaceOfT1SpaceOfConnectedSpaceOfNontrivial, perfectSpace_def, perfectSpace_iff_forall_not_isolated, perfect_def, preperfect_iff_nhds, preperfect_iff_perfect_closure	19
Total	22

AccPt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nhds_inter 📖	mathematical	Set Filter Filter.instMembership nhds	AccPt Filter.principal Set.instInter	—	Filter.le_principal_iff mem_nhdsWithin_of_mem_nhds eq_1 Filter.inf_principal inf_assoc inf_of_le_left

IsPreconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preperfect_of_nontrivial 📖	mathematical	Set.Nontrivial IsPreconnected	Preperfect	—	accPt_principal_iff_clusterPt mem_closure_iff_clusterPt Set.singleton_inter_nonempty Set.Nonempty.right isPreconnected_closed_iff isClosed_singleton isClosed_closure Set.union_diff_self Set.union_subset_union_right subset_closure Set.inter_singleton_nonempty Set.Nontrivial.exists_ne

Nat

Definitions

Name	Category	Theorems
Perfect 📖	MathDef	7 math math: abundant_iff_not_perfect_and_not_deficient, perfect_iff_sum_properDivisors, perfect_iff_sum_divisors_eq_two_mul, deficient_or_perfect_or_abundant, deficient_iff_not_abundant_and_not_perfect, perfect_iff_not_abundant_and_not_deficient, Prime.not_perfect

Perfect

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
acc 📖	mathematical	Perfect	Preperfect	—	—
closed 📖	mathematical	Perfect	IsClosed	—	—
closure_nhds_inter 📖	mathematical	Perfect Set Set.instMembership IsOpen	closure Set.instInter Set.Nonempty	—	Preperfect.perfect_closure Preperfect.open_inter acc Set.Nonempty.closure
splitting 📖	mathematical	Perfect Set.Nonempty	Set Set.instHasSubset Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	acc accPt_iff_nhds Filter.univ_mem exists_open_nhds_disjoint_closure closure_nhds_inter IsClosed.closure_subset_iff closed Set.inter_subset_right Disjoint.mono closure_mono Set.inter_subset_left

PerfectSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
not_isolated 📖	mathematical	—	Filter.NeBot nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	—	perfectSpace_iff_forall_not_isolated
univ_perfect 📖	mathematical	—	Perfect Set.univ	—	isClosed_univ univ_preperfect
univ_preperfect 📖	mathematical	—	Preperfect Set.univ	—	—

Preperfect

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
open_inter 📖	mathematical	Preperfect IsOpen	Set Set.instInter	—	AccPt.nhds_inter IsOpen.mem_nhds
perfect_closure 📖	mathematical	Preperfect	Perfect closure	—	isClosed_closure AccPt.mono Filter.principal_mono subset_closure AccPt.eq_1 nhdsWithin.eq_1 inf_assoc Filter.inf_principal closure_eq_cluster_pts

(root)

Definitions

Name	Category	Theorems
Perfect 📖	CompData	7 math math: exists_countable_union_perfect_of_isClosed, preperfect_iff_perfect_closure, Preperfect.perfect_closure, exists_perfect_nonempty_of_isClosed_of_not_countable, perfect_def, perfect_iff_eq_derivedSet, PerfectSpace.univ_perfect
Preperfect 📖	MathDef	8 math math: preperfect_iff_perfect_closure, Perfect.acc, preperfect_iff_nhds, perfectSpace_def, perfect_def, PerfectSpace.univ_preperfect, preperfect_iff_subset_derivedSet, IsPreconnected.preperfect_of_nontrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_countable_union_perfect_of_isClosed 📖	mathematical	—	Set.Countable Perfect Set Set.instUnion	—	TopologicalSpace.exists_countable_basis Set.iUnion_inter Set.Countable.biUnion Set.Countable.mono Set.inter_subset_left Set.inter_subset_right IsClosed.sdiff isOpen_biUnion TopologicalSpace.IsTopologicalBasis.isOpen preperfect_iff_nhds TopologicalSpace.IsTopologicalBasis.mem_nhds_iff Set.mem_union_right Set.mem_inter Set.mem_union_left Set.Countable.union Set.mem_biUnion Mathlib.Tactic.Push.not_and_eq Set.countable_singleton Set.inter_comm Set.inter_union_diff
exists_perfect_nonempty_of_isClosed_of_not_countable 📖	mathematical	Set.Countable	Perfect Set.Nonempty Set Set.instHasSubset	—	exists_countable_union_perfect_of_isClosed Set.nonempty_iff_ne_empty Set.union_empty Set.subset_union_right
instPerfectSpaceOfT1SpaceOfConnectedSpaceOfNontrivial 📖	mathematical	—	PerfectSpace	—	IsPreconnected.preperfect_of_nontrivial PreconnectedSpace.isPreconnected_univ ConnectedSpace.toPreconnectedSpace Set.nontrivial_univ_iff
perfectSpace_def 📖	mathematical	—	PerfectSpace Preperfect Set.univ	—	—
perfectSpace_iff_forall_not_isolated 📖	mathematical	—	PerfectSpace Filter.NeBot nhdsWithin Compl.compl Set Set.instCompl Set.instSingletonSet	—	Filter.principal_univ inf_of_le_left
perfect_def 📖	mathematical	—	Perfect IsClosed Preperfect	—	—
preperfect_iff_nhds 📖	mathematical	—	Preperfect Set Set.instMembership Set.instInter	—	—
preperfect_iff_perfect_closure 📖	mathematical	—	Preperfect Perfect closure	—	Preperfect.perfect_closure Perfect.acc subset_closure accPt_iff_frequently Ne.nhdsWithin_compl_singleton frequently_frequently_nhds Filter.Frequently.mono

---

← Back to Index