Documentation Verification Report

CountablyCompact

📁 Source: Mathlib/Topology/Compactness/CountablyCompact.lean

Statistics

Metric	Count
Definitions `CountablyCompactSpace`, `IsCountablyCompact`	2
Theorems `CountablyCompactSpace`, `SeqCompactSpace`, `isCountablyCompact_univ`, `isCountablyCompact_biUnion`, `isCountablyCompact`, `elim_directed_cover`, `elim_finite_subcover`, `elim_finite_subcover_image`, `exists_accPt_of_infinite`, `image`, `isCompact`, `isSeqCompact`, `of_isClosed_subset`, `of_seq_clusterPt`, `seq_clusterPt`, `union`, `isCompact`, `isCountablyCompact`, `CompactSpace`, `CountablyCompactSpace`, `isCountablyCompact_biUnion`, `isCountablyCompact_sUnion`, `isCountablyCompact_empty`, `isCountablyCompact_iUnion`, `isCountablyCompact_iff_countable_open_cover`, `isCountablyCompact_iff_countable_open_cover'`, `isCountablyCompact_iff_infinite_subset_has_accPt`, `isCountablyCompact_iff_isSeqCompact`, `isCountablyCompact_iff_seq_clusterPt`, `isCountablyCompact_singleton`	30
Total	32

CompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`CountablyCompactSpace` 📖	mathematical	—	`CountablyCompactSpace`	—	`IsCompact.isCountablyCompact` `isCompact_univ`

CountablyCompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SeqCompactSpace` 📖	mathematical	—	`SeqCompactSpace`	—	`IsCountablyCompact.isSeqCompact` `isCountablyCompact_univ`
`isCountablyCompact_univ` 📖	mathematical	—	`IsCountablyCompact` `Set.univ`	—	—

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCountablyCompact_biUnion` 📖	mathematical	`IsCountablyCompact`	`IsCountablyCompact` `Set.iUnion` `Finset` `SetLike.instMembership` `instSetLike`	—	`induction_on` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `isCountablyCompact_empty` `Set.iUnion_iUnion_eq_or_left` `IsCountablyCompact.union` `mem_insert_self` `mem_insert_of_mem`

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCountablyCompact` 📖	mathematical	`IsCompact`	`IsCountablyCompact`	—	—

IsCountablyCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`elim_directed_cover` 📖	mathematical	`IsCountablyCompact` `IsOpen` `Set` `Set.instHasSubset` `Set.iUnion` `Directed`	`Set` `Set.instHasSubset`	—	`Filter.principal_mono` `Set.diff_subset_diff_right` `Filter.iInf_neBot_of_directed'` `Set.Nonempty.principal_neBot` `Set.diff_nonempty` `iInf_le_of_le` `Set.diff_subset` `Filter.iInf.isCountablyGenerated` `Filter.isCountablyGenerated_principal` `Set.mem_iUnion` `closure_minimal` `IsOpen.isClosed_compl` `ClusterPt.mem_closure` `ClusterPt.mono` `iInf_le`
`elim_finite_subcover` 📖	mathematical	`IsCountablyCompact` `IsOpen` `Set` `Set.instHasSubset` `Set.iUnion`	`Finset` `Set` `Set.instHasSubset` `Set.iUnion` `SetLike.instMembership` `Finset.instSetLike`	—	`elim_directed_cover` `Finset.countable` `isOpen_biUnion` `Set.iUnion_eq_iUnion_finset` `directed_of_isDirected_le` `Finset.isDirected_le` `Set.biUnion_subset_biUnion_left`
`elim_finite_subcover_image` 📖	mathematical	`IsCountablyCompact` `IsOpen` `Set` `Set.instHasSubset` `Set.iUnion` `Set.instMembership`	`Set` `Set.instHasSubset` `Set.Finite` `Set.iUnion` `Set.instMembership`	—	`Set.Countable.to_subtype` `elim_finite_subcover` `Subtype.prop` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop` `Set.biUnion_eq_iUnion` `Subtype.coe_preimage_self` `Set.Finite.image` `Finset.finite_toSet` `Set.biUnion_image`
`exists_accPt_of_infinite` 📖	mathematical	`IsCountablyCompact` `Set` `Set.instHasSubset` `Set.Infinite`	`Set` `Set.instMembership` `AccPt` `Filter.principal`	—	`Subtype.val_injective` `Function.Embedding.injective` `seq_clusterPt` `Filter.Eventually.of_forall` `accPt_iff_clusterPt` `ClusterPt.mono` `le_inf` `Filter.tendsto_principal` `Set.Finite.compl_mem_cofinite` `Set.Finite.preimage` `Function.Injective.injOn` `Set.finite_singleton` `Nat.cofinite_eq_atTop`
`image` 📖	mathematical	`IsCountablyCompact` `Continuous`	`IsCountablyCompact` `Set.image`	—	`Filter.comap_inf_principal_neBot_of_image_mem` `Filter.le_principal_iff` `Filter.Inf.isCountablyGenerated` `Filter.comap.isCountablyGenerated` `Filter.isCountablyGenerated_principal` `inf_le_right` `ClusterPt.neBot` `ClusterPt.mono` `inf_le_left` `Set.mem_image_of_mem` `Filter.Tendsto.neBot` `Filter.Tendsto.inf` `Continuous.continuousAt` `Filter.tendsto_comap`
`isCompact` 📖	mathematical	`IsCountablyCompact`	`IsCompact`	—	`IsLindelof.isCompact` `HereditarilyLindelofSpace.isLindelof`
`isSeqCompact` 📖	mathematical	`IsCountablyCompact`	`IsSeqCompact`	—	`seq_clusterPt` `Filter.Eventually.of_forall` `TopologicalSpace.FirstCountableTopology.tendsto_subseq`
`of_isClosed_subset` 📖	mathematical	`IsCountablyCompact` `Set` `Set.instHasSubset`	`IsCountablyCompact`	—	`LE.le.trans` `Filter.principal_mono` `isClosed_iff_clusterPt` `ClusterPt.mono`
`of_seq_clusterPt` 📖	mathematical	`Set` `Set.instMembership` `MapClusterPt` `Filter.atTop` `Nat.instPreorder`	`IsCountablyCompact`	—	`isCountablyCompact_iff_seq_clusterPt`
`seq_clusterPt` 📖	mathematical	`IsCountablyCompact` `Filter.Eventually` `Set` `Set.instMembership` `Filter.atTop` `Nat.instPreorder`	`Set` `Set.instMembership` `MapClusterPt` `Filter.atTop` `Nat.instPreorder`	—	`isCountablyCompact_iff_seq_clusterPt`
`union` 📖	mathematical	`IsCountablyCompact`	`IsCountablyCompact` `Set` `Set.instUnion`	—	`isCountablyCompact_iff_countable_open_cover'` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.subset_union_left` `Set.subset_union_right` `Set.ext` `Set.iUnion_congr_Prop` `Set.Finite.union` `Set.union_subset_union`

IsLindelof

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCompact` 📖	mathematical	`IsCountablyCompact` `IsLindelof`	`IsCompact`	—	`isCompact_of_finite_subcover` `indexed_countable_subcover` `isCountablyCompact_iff_countable_open_cover` `Set.iUnion_congr_Prop` `Set.iUnion_exists` `Set.biUnion_and'` `Set.iUnion_iUnion_eq_right` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.instReflSubset`

IsSeqCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCountablyCompact` 📖	mathematical	`IsSeqCompact`	`IsCountablyCompact`	—	`IsCountablyCompact.of_seq_clusterPt` `subseq_of_frequently_in` `Filter.Eventually.frequently` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder` `MapClusterPt.of_comp` `StrictMono.tendsto_atTop` `Filter.Tendsto.mapClusterPt`

LindelofSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`CompactSpace` 📖	mathematical	—	`CompactSpace`	—	`IsLindelof.isCompact` `CountablyCompactSpace.isCountablyCompact_univ` `isLindelof_univ`

SeqCompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`CountablyCompactSpace` 📖	mathematical	—	`CountablyCompactSpace`	—	`IsSeqCompact.isCountablyCompact` `isSeqCompact_univ`

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCountablyCompact_biUnion` 📖	mathematical	`IsCountablyCompact`	`IsCountablyCompact` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.iUnion_congr_Prop` `Finset.isCountablyCompact_biUnion` `mem_toFinset`
`isCountablyCompact_sUnion` 📖	mathematical	`IsCountablyCompact`	`IsCountablyCompact` `Set.sUnion`	—	`Set.sUnion_eq_biUnion` `isCountablyCompact_biUnion`

(root)

Definitions

Name	Category	Theorems
`CountablyCompactSpace` 📖	CompData	2 math math: `CompactSpace.CountablyCompactSpace`, `SeqCompactSpace.CountablyCompactSpace`
`IsCountablyCompact` 📖	MathDef	18 math math: `IsCountablyCompact.of_seq_clusterPt`, `IsCountablyCompact.union`, `IsCountablyCompact.image`, `isCountablyCompact_singleton`, `isCountablyCompact_iff_countable_open_cover'`, `IsCompact.isCountablyCompact`, `isCountablyCompact_iUnion`, `CountablyCompactSpace.isCountablyCompact_univ`, `isCountablyCompact_iff_countable_open_cover`, `Finset.isCountablyCompact_biUnion`, `isCountablyCompact_empty`, `Set.Finite.isCountablyCompact_sUnion`, `isCountablyCompact_iff_isSeqCompact`, `Set.Finite.isCountablyCompact_biUnion`, `IsCountablyCompact.of_isClosed_subset`, `IsSeqCompact.isCountablyCompact`, `isCountablyCompact_iff_infinite_subset_has_accPt`, `isCountablyCompact_iff_seq_clusterPt`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCountablyCompact_empty` 📖	mathematical	—	`IsCountablyCompact` `Set` `Set.instEmptyCollection`	—	`Filter.empty_mem_iff_bot` `Filter.le_principal_iff` `Filter.NeBot.ne'`
`isCountablyCompact_iUnion` 📖	mathematical	`IsCountablyCompact`	`IsCountablyCompact` `Set.iUnion`	—	`Set.Finite.isCountablyCompact_sUnion` `Set.finite_range` `Set.forall_mem_range`
`isCountablyCompact_iff_countable_open_cover` 📖	mathematical	—	`IsCountablyCompact` `Finset` `Set` `Set.instHasSubset` `Set.iUnion` `SetLike.instMembership` `Finset.instSetLike`	—	`IsCountablyCompact.elim_finite_subcover` `instCountableNat` `IsCountablyCompact.of_seq_clusterPt` `Set.compl_subset_compl` `closure_mono` `Set.image_mono` `Set.Ici_subset_Ici` `Set.mem_iUnion` `SemilatticeSup.instIsDirectedOrder` `Mathlib.Tactic.Push.not_and_eq` `IsClosed.isOpen_compl` `isClosed_closure` `Filter.eventually_atTop` `Set.mem_iUnion₂` `le_max_left` `LE.le.trans` `Finset.le_sup` `le_max_right` `subset_closure` `Set.mem_Ici` `le_rfl`
`isCountablyCompact_iff_countable_open_cover'` 📖	mathematical	—	`IsCountablyCompact` `Set` `Set.Finite` `Set.instHasSubset` `Set.iUnion` `Set.instMembership`	—	`Set.iUnion_congr_Prop`
`isCountablyCompact_iff_infinite_subset_has_accPt` 📖	mathematical	—	`IsCountablyCompact` `Set` `Set.instMembership` `AccPt` `Filter.principal`	—	`IsCountablyCompact.exists_accPt_of_infinite` `IsCountablyCompact.of_seq_clusterPt` `Nat.cofinite_eq_atTop` `IsCompact.exists_mapClusterPt_of_frequently` `Set.Finite.isCompact` `Set.Finite.inter_of_left` `Filter.Frequently.mp` `Filter.Eventually.frequently` `Filter.cofinite_neBot` `instInfiniteNat` `Set.inter_subset_right` `Set.Infinite.inter_of_finite_diff` `Set.Finite.subset` `Set.Finite.image` `Set.compl_setOf` `Filter.mem_cofinite` `Filter.eventually_iff` `Set.Infinite.of_image` `Set.Infinite.mono` `Set.Infinite.of_accPt` `AccPt.nhds_inter`
`isCountablyCompact_iff_isSeqCompact` 📖	mathematical	—	`IsCountablyCompact` `IsSeqCompact`	—	`IsCountablyCompact.isSeqCompact` `IsSeqCompact.isCountablyCompact`
`isCountablyCompact_iff_seq_clusterPt` 📖	mathematical	—	`IsCountablyCompact` `Set` `Set.instMembership` `MapClusterPt` `Filter.atTop` `Nat.instPreorder`	—	`Filter.map_neBot` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder` `Filter.map.isCountablyGenerated` `Filter.atTop.isCountablyGenerated` `instCountableNat` `Filter.tendsto_principal` `Filter.exists_seq_tendsto` `Filter.Tendsto.mono_right` `ClusterPt.mono` `MapClusterPt.clusterPt`
`isCountablyCompact_singleton` 📖	mathematical	—	`IsCountablyCompact` `Set` `Set.instSingletonSet`	—	`ClusterPt.of_le_nhds` `LE.le.trans` `pure_le_nhds` `Filter.principal_singleton`

---

← Back to Index