AlexandrovDiscrete

📁 Source: Mathlib/Topology/AlexandrovDiscrete.lean

Statistics

Metric	Count
Definitions	0
Theorems `isOpen_sInter`, `sup`, `toFirstCountable`, `toLocallyCompactSpace`, `toAlexandrovDiscrete`, `toAlexandrovDiscrete`, `instAlexandrovDiscreteOfFinite`, `instAlexandrovDiscrete`, `instAlexandrovDiscrete`, `instAlexandrovDiscrete`, `instAlexandrovDiscrete`, `instAlexandrovDiscrete`, `alexandrovDiscrete`, `alexandrovDiscrete_coinduced`, `alexandrovDiscrete_iSup`, `alexandrovDiscrete_iff`, `alexandrovDiscrete_iff_isClosed`, `alexandrovDiscrete_iff_nhds`, `closure_iUnion`, `closure_sUnion`, `gc_nhdsKer_interior`, `interior_iInter`, `interior_sInter`, `isClopen_iInter`, `isClopen_iInter₂`, `isClopen_iUnion`, `isClopen_iUnion₂`, `isClopen_sInter`, `isClopen_sUnion`, `isClosed_iUnion`, `isClosed_iUnion₂`, `isClosed_sUnion`, `isOpen_iInter`, `isOpen_iInter₂`, `isOpen_iff_forall_specializes`, `isOpen_nhdsKer`, `isOpen_sInter`, `nhdsKer_eq_iff_isOpen`, `nhdsKer_mem_nhdsSet`, `nhdsKer_singleton_subset_iff_mem_nhds`, `nhdsKer_subset_iff`, `nhdsKer_subset_iff_isOpen`, `nhdsKer_subset_iff_mem_nhdsSet`, `nhdsSet_basis_nhdsKer`, `nhds_basis_nhdsKer_singleton`, `principal_nhdsKer`, `principal_nhdsKer_singleton`	47
Total	47

AlexandrovDiscrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen_sInter` 📖	mathematical	`IsOpen`	`Set.sInter`	—	—
`sup` 📖	mathematical	—	`AlexandrovDiscrete` `TopologicalSpace` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice`	—	`isOpen_sInter`
`toFirstCountable` 📖	mathematical	—	`FirstCountableTopology`	—	`Set.countable_singleton` `Filter.generate_singleton` `principal_nhdsKer` `nhdsSet_singleton`
`toLocallyCompactSpace` 📖	mathematical	—	`LocallyCompactSpace`	—	`IsOpen.mem_nhds` `isOpen_nhdsKer` `subset_nhdsKer` `Set.mem_singleton` `nhdsKer_singleton_subset_iff_mem_nhds` `IsCompact.nhdsKer` `isCompact_singleton`

DiscreteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toAlexandrovDiscrete` 📖	mathematical	—	`AlexandrovDiscrete`	—	`isOpen_discrete`

Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toAlexandrovDiscrete` 📖	mathematical	—	`AlexandrovDiscrete`	—	`Set.Finite.isOpen_sInter` `Set.toFinite` `Subtype.finite` `Set.instFinite`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAlexandrovDiscreteOfFinite` 📖	mathematical	`AlexandrovDiscrete`	`topologicalSpace`	—	`nhds_pi` `Filter.pi_principal` `nhdsKer_singleton_pi`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAlexandrovDiscrete` 📖	mathematical	—	`AlexandrovDiscrete` `instTopologicalSpaceProd`	—	`nhds_prod_eq` `Filter.prod_principal_principal` `nhdsKer_pair`

Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAlexandrovDiscrete` 📖	mathematical	—	`AlexandrovDiscrete` `instTopologicalSpaceQuotient`	—	`alexandrovDiscrete_coinduced`

Sigma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAlexandrovDiscrete` 📖	mathematical	`AlexandrovDiscrete`	`instTopologicalSpaceSigma`	—	`alexandrovDiscrete_iSup` `alexandrovDiscrete_coinduced`

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAlexandrovDiscrete` 📖	mathematical	—	`AlexandrovDiscrete` `instTopologicalSpaceSubtype`	—	`Topology.IsInducing.alexandrovDiscrete` `Topology.IsInducing.subtypeVal`

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAlexandrovDiscrete` 📖	mathematical	—	`AlexandrovDiscrete` `instTopologicalSpaceSum`	—	`AlexandrovDiscrete.sup` `alexandrovDiscrete_coinduced`

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`alexandrovDiscrete` 📖	mathematical	`Topology.IsInducing`	`AlexandrovDiscrete`	—	`isOpen_iff` `isOpen_iInter₂` `Set.preimage_iInter` `Set.iInter_congr_Prop` `Set.sInter_eq_biInter`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`alexandrovDiscrete_coinduced` 📖	mathematical	—	`AlexandrovDiscrete` `TopologicalSpace.coinduced`	—	`isOpen_coinduced` `Set.preimage_sInter` `isOpen_iInter₂`
`alexandrovDiscrete_iSup` 📖	mathematical	`AlexandrovDiscrete`	`iSup` `TopologicalSpace` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.instCompleteLattice`	—	`isOpen_iSup_iff` `isOpen_sInter`
`alexandrovDiscrete_iff` 📖	mathematical	—	`AlexandrovDiscrete` `IsOpen` `Set.sInter`	—	—
`alexandrovDiscrete_iff_isClosed` 📖	mathematical	—	`AlexandrovDiscrete` `IsClosed` `Set.sUnion`	—	`Function.Surjective.forall` `Function.Surjective.image_surjective` `compl_surjective`
`alexandrovDiscrete_iff_nhds` 📖	mathematical	—	`AlexandrovDiscrete` `nhds` `Filter.principal` `nhdsKer` `Set` `Set.instSingletonSet`	—	`principal_nhdsKer_singleton` `Filter.inf_principal` `Set.nonempty_biUnion` `Set.inter_iUnion₂` `Set.sUnion_eq_biUnion` `Set.mem_sUnion_of_mem`
`closure_iUnion` 📖	mathematical	—	`closure` `Set.iUnion`	—	`compl_injective` `Set.compl_iUnion` `interior_iInter`
`closure_sUnion` 📖	mathematical	—	`closure` `Set.sUnion` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.sUnion_eq_biUnion` `closure_iUnion`
`gc_nhdsKer_interior` 📖	mathematical	—	`GaloisConnection` `Set` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `nhdsKer` `interior`	—	—
`interior_iInter` 📖	mathematical	—	`interior` `Set.iInter`	—	`HasSubset.Subset.antisymm'` `Set.instAntisymmSubset` `interior_maximal` `Set.iInter_mono` `interior_subset` `isOpen_iInter` `isOpen_interior` `Set.subset_iInter` `interior_mono` `Set.iInter_subset`
`interior_sInter` 📖	mathematical	—	`interior` `Set.sInter` `Set.iInter` `Set` `Set.instMembership`	—	`Set.sInter_eq_biInter` `interior_iInter`
`isClopen_iInter` 📖	mathematical	`IsClopen`	`Set.iInter`	—	`isClosed_iInter` `isOpen_iInter`
`isClopen_iInter₂` 📖	mathematical	`IsClopen`	`Set.iInter`	—	`isClopen_iInter`
`isClopen_iUnion` 📖	mathematical	`IsClopen`	`Set.iUnion`	—	`isClosed_iUnion` `isOpen_iUnion`
`isClopen_iUnion₂` 📖	mathematical	`IsClopen`	`Set.iUnion`	—	`isClopen_iUnion`
`isClopen_sInter` 📖	mathematical	`IsClopen`	`Set.sInter`	—	`isClosed_sInter` `isOpen_sInter`
`isClopen_sUnion` 📖	mathematical	`IsClopen`	`Set.sUnion`	—	`isClosed_sUnion` `isOpen_sUnion`
`isClosed_iUnion` 📖	mathematical	`IsClosed`	`Set.iUnion`	—	`isClosed_sUnion` `Set.forall_mem_range`
`isClosed_iUnion₂` 📖	mathematical	`IsClosed`	`Set.iUnion`	—	`isClosed_iUnion`
`isClosed_sUnion` 📖	mathematical	`IsClosed`	`Set.sUnion`	—	`alexandrovDiscrete_iff_isClosed`
`isOpen_iInter` 📖	mathematical	`IsOpen`	`Set.iInter`	—	`isOpen_sInter` `Set.forall_mem_range`
`isOpen_iInter₂` 📖	mathematical	`IsOpen`	`Set.iInter`	—	`isOpen_iInter`
`isOpen_iff_forall_specializes` 📖	mathematical	—	`IsOpen` `Set` `Set.instMembership`	—	`forall_swap`
`isOpen_nhdsKer` 📖	mathematical	—	`IsOpen` `nhdsKer`	—	`nhdsKer_def` `isOpen_sInter`
`isOpen_sInter` 📖	mathematical	`IsOpen`	`Set.sInter`	—	`AlexandrovDiscrete.isOpen_sInter`
`nhdsKer_eq_iff_isOpen` 📖	mathematical	—	`nhdsKer` `IsOpen`	—	`isOpen_nhdsKer` `IsOpen.nhdsKer_eq`
`nhdsKer_mem_nhdsSet` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsSet` `nhdsKer`	—	`IsOpen.mem_nhdsSet` `isOpen_nhdsKer` `subset_nhdsKer`
`nhdsKer_singleton_subset_iff_mem_nhds` 📖	mathematical	—	`Set` `Set.instHasSubset` `nhdsKer` `Set.instSingletonSet` `Filter` `Filter.instMembership` `nhds`	—	`nhdsSet_singleton`
`nhdsKer_subset_iff` 📖	mathematical	—	`Set` `Set.instHasSubset` `nhdsKer` `IsOpen`	—	`isOpen_nhdsKer` `subset_nhdsKer` `HasSubset.Subset.trans` `Set.instIsTransSubset` `nhdsKer_minimal`
`nhdsKer_subset_iff_isOpen` 📖	mathematical	—	`Set` `Set.instHasSubset` `nhdsKer` `IsOpen`	—	`nhdsKer_eq_iff_isOpen`
`nhdsKer_subset_iff_mem_nhdsSet` 📖	mathematical	—	`Set` `Set.instHasSubset` `nhdsKer` `Filter` `Filter.instMembership` `nhdsSet`	—	`nhdsKer_subset_iff` `mem_nhdsSet_iff_exists`
`nhdsSet_basis_nhdsKer` 📖	mathematical	—	`Filter.HasBasis` `nhdsSet` `nhdsKer`	—	`Filter.hasBasis_principal` `principal_nhdsKer`
`nhds_basis_nhdsKer_singleton` 📖	mathematical	—	`Filter.HasBasis` `nhds` `nhdsKer` `Set` `Set.instSingletonSet`	—	`Filter.hasBasis_principal` `principal_nhdsKer_singleton`
`principal_nhdsKer` 📖	mathematical	—	`Filter.principal` `nhdsKer` `nhdsSet`	—	`nhdsSet_nhdsKer` `IsOpen.nhdsSet_eq` `isOpen_nhdsKer`
`principal_nhdsKer_singleton` 📖	mathematical	—	`Filter.principal` `nhdsKer` `Set` `Set.instSingletonSet` `nhds`	—	`principal_nhdsKer` `nhdsSet_singleton`

---

← Back to Index