Documentation Verification Report

CountablyGenerated

📁 Source: Mathlib/Order/Filter/CountablyGenerated.lean

Statistics

Metric	Count
Definitions `CountableFilterBasis`, `toFilterBasis`, `HasCountableBasis`, `IsCountableBasis`, `IsCountablyGenerated`, `inhabitedCountableFilterBasis`	6
Theorems `countable`, `hasBasis_ge`, `mem`, `mem_iff`, `exists_antitone_subbasis`, `isCountablyGenerated`, `countable`, `isCountablyGenerated`, `toHasBasis`, `isCountablyGenerated`, `countable`, `toIsBasis`, `out`, `isCountablyGenerated`, `antitone_seq_of_seq`, `isCountablyGenerated`, `isCountablyGenerated`, `countable_biInf_eq_iInf_seq`, `countable_biInf_eq_iInf_seq'`, `countable_biInf_principal_eq_seq_iInf`, `exists_antitone_basis`, `exists_antitone_seq`, `isCountablyGenerated`, `isCountablyGenerated_biInf_principal`, `isCountablyGenerated_bot`, `isCountablyGenerated_iff_exists_antitone_basis`, `isCountablyGenerated_of_seq`, `isCountablyGenerated_principal`, `isCountablyGenerated_pure`, `isCountablyGenerated_seq`, `isCountablyGenerated_top`, `isCountablyGenerated`, `isCountablyGenerated`, `isCountablyGenerated`	34
Total	40

Filter

Definitions

Name	Category	Theorems
`CountableFilterBasis` 📖	CompData	—
`HasCountableBasis` 📖	CompData	4 math math: `atBot_countable_basis`, `atTop_hasCountableBasis_of_archimedean`, `atTop_countable_basis`, `atBot_hasCountableBasis_of_archimedean`
`IsCountableBasis` 📖	CompData	—
`IsCountablyGenerated` 📖	CompData	44 math math: `IsUniformGroup.uniformity_countably_generated`, `instIsCountablyGenerated_atBot`, `Rat.not_countably_generated_cocompact`, `Inf.isCountablyGenerated`, `isCountablyGenerated_of_seq`, `instIsCountablyGeneratedProdUniformity`, `map.isCountablyGenerated`, `OrderDual.instIsCountablyGeneratedAtBot`, `UniformOnFun.isCountablyGenerated_uniformity`, `IsUniformAddGroup.uniformity_countably_generated`, `OrderDual.instIsCountablyGeneratedAtTop`, `isCountablyGenerated_bot`, `SummationFilter.instIsCountablyGeneratedFinsetFilterUnconditionalOfCountable`, `isCountablyGenerated_seq`, `EMetric.instIsCountablyGeneratedUniformity`, `isCountablyGenerated_iff_exists_antitone_basis`, `prod.isCountablyGenerated`, `isCountablyGenerated_biInf_principal`, `instIsCountablyGeneratedAtTopProd`, `HasCountableBasis.isCountablyGenerated`, `Rat.not_countably_generated_nhds_infty_opc`, `Subsingleton.isCountablyGenerated`, `instIsCountablyGeneratedNhds`, `TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated`, `instIsCountablyGenerated_atTop`, `instIsCountablyGeneratedProdSumUniformity`, `atTop.isCountablyGenerated`, `isCountablyGenerated_principal`, `isCountablyGenerated_pure`, `atBot_isCountablyGenerated_of_archimedean`, `isCountablyGenerated_top`, `ContinuousMap.instIsCountablyGeneratedProdUniformityOfWeaklyLocallyCompactSpaceOfSigmaCompactSpace`, `instIsCountablyGeneratedAtBotProd`, `TopologicalSpace.isCountablyGenerated_nhdsWithin`, `TopologicalSpace.PseudoMetrizableSpace.exists_countably_generated`, `Sup.isCountablyGenerated`, `instIsCountablyGeneratedProdElemUniformity`, `comap.isCountablyGenerated`, `atTop_isCountablyGenerated_of_archimedean`, `HasBasis.isCountablyGenerated`, `coprod.isCountablyGenerated`, `FirstCountableTopology.nhds_generated_countable`, `SummationFilter.instIsCountablyGeneratedFinsetFilterConditionalOfAtTopOfAtBot`, `atBot.isCountablyGenerated`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitone_seq_of_seq` 📖	mathematical	—	`Antitone` `Set` `Nat.instPreorder` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `iInf` `Filter` `instInfSet` `principal`	—	`Set.biInter_mono` `Set.Iic_subset_Iic` `Set.Subset.rfl` `le_antisymm` `le_iInf_iff` `le_principal_iff` `biInter_mem` `Set.finite_le_nat` `mem_iInf_of_mem` `mem_principal_self` `iInf_le_of_le` `principal_mono` `Set.iInter₂_subset` `le_refl`
`countable_biInf_eq_iInf_seq` 📖	mathematical	`Set.Nonempty`	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Set` `Set.instMembership`	—	`Set.Countable.exists_eq_range` `iInf_range`
`countable_biInf_eq_iInf_seq'` 📖	mathematical	`Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`iInf` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Set` `Set.instMembership`	—	`Set.eq_empty_or_nonempty` `iInf_emptyset` `iInf_top` `countable_biInf_eq_iInf_seq`
`countable_biInf_principal_eq_seq_iInf` 📖	mathematical	—	`iInf` `Filter` `Set` `instInfSet` `Set.instMembership` `principal`	—	`countable_biInf_eq_iInf_seq'` `principal_univ`
`exists_antitone_basis` 📖	mathematical	—	`HasAntitoneBasis` `Nat.instPreorder`	—	`HasBasis.exists_antitone_subbasis` `basis_sets`
`exists_antitone_seq` 📖	mathematical	—	`Antitone` `Set` `Nat.instPreorder` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Filter` `instMembership` `Set.instHasSubset`	—	`exists_antitone_basis` `HasAntitoneBasis.antitone` `HasBasis.mem_iff` `HasAntitoneBasis.toHasBasis`
`isCountablyGenerated_biInf_principal` 📖	mathematical	—	`IsCountablyGenerated` `iInf` `Filter` `Set` `instInfSet` `Set.instMembership` `principal`	—	`isCountablyGenerated_of_seq` `countable_biInf_principal_eq_seq_iInf`
`isCountablyGenerated_bot` 📖	mathematical	—	`IsCountablyGenerated` `Bot.bot` `Filter` `instBot`	—	`isCountablyGenerated_principal` `principal_empty`
`isCountablyGenerated_iff_exists_antitone_basis` 📖	mathematical	—	`IsCountablyGenerated` `HasAntitoneBasis` `Nat.instPreorder`	—	`exists_antitone_basis` `HasBasis.eq_iInf` `HasAntitoneBasis.toHasBasis` `isCountablyGenerated_seq` `instCountableNat`
`isCountablyGenerated_of_seq` 📖	mathematical	`iInf` `Filter` `instInfSet` `principal`	`IsCountablyGenerated`	—	`isCountablyGenerated_seq` `instCountableNat`
`isCountablyGenerated_principal` 📖	mathematical	—	`IsCountablyGenerated` `principal`	—	`isCountablyGenerated_of_seq` `iInf_const`
`isCountablyGenerated_pure` 📖	mathematical	—	`IsCountablyGenerated` `Filter` `instPure`	—	`principal_singleton` `isCountablyGenerated_principal`
`isCountablyGenerated_seq` 📖	mathematical	—	`IsCountablyGenerated` `iInf` `Filter` `instInfSet` `principal`	—	`Set.countable_range` `generate_eq_biInf` `iInf_range`
`isCountablyGenerated_top` 📖	mathematical	—	`IsCountablyGenerated` `Top.top` `Filter` `instTop`	—	`isCountablyGenerated_principal` `principal_univ`

Filter.CountableFilterBasis

Definitions

Name	Category	Theorems
`toFilterBasis` 📖	CompOp	1 math math: `countable`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countable` 📖	mathematical	—	`Set.Countable` `Set` `FilterBasis.sets` `toFilterBasis`	—	—

Filter.HasAntitoneBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasBasis_ge` 📖	mathematical	`Filter.HasAntitoneBasis`	`Filter.HasBasis` `Preorder.toLE`	—	`Filter.HasBasis.to_hasBasis` `toHasBasis` `antitone` `exists_ge_ge` `Set.Subset.rfl`
`mem` 📖	mathematical	`Filter.HasAntitoneBasis`	`Set` `Filter` `Filter.instMembership`	—	`Filter.HasBasis.mem_of_mem` `toHasBasis`
`mem_iff` 📖	mathematical	`Filter.HasAntitoneBasis`	`Set` `Filter` `Filter.instMembership` `Set.instHasSubset`	—	`Filter.HasBasis.mem_iff` `toHasBasis`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_antitone_subbasis` 📖	mathematical	`Filter.HasBasis`	`Filter.HasAntitoneBasis` `Nat.instPreorder`	—	`Filter.generate_eq_biInf` `Filter.countable_biInf_principal_eq_seq_iInf` `iInf_le` `Filter.mem_principal_self` `Filter.inter_mem` `mem_of_mem` `antitone_nat_of_succ_le` `HasSubset.Subset.trans` `Set.instIsTransSubset` `set_index_subset` `Set.inter_subset_right` `Set.inter_subset_left` `Filter.HasAntitoneBasis.iInf_principal` `SemilatticeSup.instIsDirectedOrder` `le_antisymm` `le_iInf` `Filter.le_principal_iff` `set_index_mem` `mem_iff` `Filter.HasAntitoneBasis.toHasBasis`
`isCountablyGenerated` 📖	mathematical	`Filter.HasBasis`	`Filter.IsCountablyGenerated`	—	`Filter.HasCountableBasis.isCountablyGenerated` `Set.to_countable` `SetCoe.countable`

Filter.HasCountableBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countable` 📖	mathematical	`Filter.HasCountableBasis`	`Set.Countable` `setOf`	—	—
`isCountablyGenerated` 📖	mathematical	`Filter.HasCountableBasis`	`Filter.IsCountablyGenerated`	—	`Set.Countable.image` `countable` `Filter.HasBasis.eq_generate` `toHasBasis`
`toHasBasis` 📖	mathematical	`Filter.HasCountableBasis`	`Filter.HasBasis`	—	—

Filter.Inf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCountablyGenerated` 📖	mathematical	—	`Filter.IsCountablyGenerated` `Filter` `Filter.instInf`	—	`Filter.exists_antitone_basis` `Filter.HasCountableBasis.isCountablyGenerated` `Filter.HasBasis.inf` `Filter.HasAntitoneBasis.toHasBasis` `Set.to_countable` `SetCoe.countable` `instCountableProd` `instCountableNat`

Filter.IsCountableBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`countable` 📖	mathematical	`Filter.IsCountableBasis`	`Set.Countable` `setOf`	—	—
`toIsBasis` 📖	mathematical	`Filter.IsCountableBasis`	`Filter.IsBasis`	—	—

Filter.IsCountablyGenerated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`out` 📖	mathematical	—	`Set.Countable` `Set` `Filter.generate`	—	—

Filter.Nat

Definitions

Name	Category	Theorems
`inhabitedCountableFilterBasis` 📖	CompOp	—

Filter.Sup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCountablyGenerated` 📖	mathematical	—	`Filter.IsCountablyGenerated` `Filter` `Filter.instSup`	—	`Filter.exists_antitone_basis` `Filter.HasCountableBasis.isCountablyGenerated` `Filter.HasBasis.sup` `Filter.HasAntitoneBasis.toHasBasis` `Set.to_countable` `SetCoe.countable` `instCountableProd` `instCountableNat`

Filter.comap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCountablyGenerated` 📖	mathematical	—	`Filter.IsCountablyGenerated` `Filter.comap`	—	`Filter.exists_antitone_basis` `Filter.HasBasis.isCountablyGenerated` `instCountableNat` `Filter.HasAntitoneBasis.toHasBasis` `Filter.HasAntitoneBasis.comap`

Filter.coprod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCountablyGenerated` 📖	mathematical	—	`Filter.IsCountablyGenerated` `Filter.coprod`	—	`Filter.Sup.isCountablyGenerated` `Filter.comap.isCountablyGenerated`

Filter.iInf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCountablyGenerated` 📖	mathematical	`Filter.IsCountablyGenerated`	`iInf` `Filter` `Filter.instInfSet`	—	`Function.Surjective.iInf_comp` `PLift.down_surjective` `Filter.HasCountableBasis.isCountablyGenerated` `Filter.HasBasis.iInf` `Filter.HasAntitoneBasis.toHasBasis` `Set.Countable.mono` `CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `Set.countable_range` `instCountableSigma` `Finset.countable` `instCountablePLift` `instCountableForallOfFinite` `Finite.of_fintype` `instCountableNat` `Filter.exists_antitone_basis`

Filter.map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCountablyGenerated` 📖	mathematical	—	`Filter.IsCountablyGenerated` `Filter.map`	—	`Filter.exists_antitone_basis` `Filter.HasBasis.isCountablyGenerated` `instCountableNat` `Filter.HasAntitoneBasis.toHasBasis` `Filter.HasAntitoneBasis.map`

Filter.pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCountablyGenerated` 📖	mathematical	`Filter.IsCountablyGenerated`	`Filter.pi`	—	`Filter.iInf.isCountablyGenerated` `Filter.comap.isCountablyGenerated`

Filter.prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCountablyGenerated` 📖	mathematical	—	`Filter.IsCountablyGenerated` `SProd.sprod` `Filter` `Filter.instSProd`	—	`Filter.Inf.isCountablyGenerated` `Filter.comap.isCountablyGenerated`

---

← Back to Index