Documentation Verification Report

VietorisTopology

📁 Source: Mathlib/Topology/Sets/VietorisTopology.lean

Statistics

Metric	Count
Definitions `topology`, `topology`, `vietoris`	3
Theorems `powerset_vietoris`, `powerset_vietoris`, `powerset_vietoris`, `compactSpace_iff`, `continuous_coe`, `instCompactSpace`, `instNoncompactSpace`, `isClopen_singleton_bot`, `isClosed_inter_nonempty_of_isClosed`, `isClosed_subsets_of_isClosed`, `isCompact_biUnion_coe_of_isCompact`, `isCompact_subsets_of_isCompact`, `isEmbedding_coe`, `isOpen_inter_nonempty_of_isOpen`, `isOpen_subsets_of_isOpen`, `isTopologicalBasis`, `noncompactSpace_iff`, `compacts`, `nonemptyCompacts`, `vietoris`, `compactSpace_iff`, `continuous_coe`, `continuous_toCompacts`, `instCompactSpace`, `instNoncompactSpace`, `isClosedEmbedding_toCompacts`, `isClosed_inter_nonempty_of_isClosed`, `isClosed_subsets_of_isClosed`, `isCompact_biUnion_coe_of_isCompact`, `isCompact_subsets_of_isCompact`, `isEmbedding_coe`, `isEmbedding_toCompacts`, `isOpenEmbedding_toCompacts`, `isOpen_inter_nonempty_of_isOpen`, `isOpen_subsets_of_isOpen`, `isTopologicalBasis`, `noncompactSpace_iff`, `instCompactSpaceSet`, `isClopen_singleton_empty`, `isClosed_inter_nonempty_of_isClosed`, `isOpen_inter_nonempty_of_isOpen`, `isTopologicalBasis`, `specializes_closure`, `specializes_of_subset_closure`	44
Total	47

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`powerset_vietoris` 📖	mathematical	—	`IsClosed` `Set` `TopologicalSpace.vietoris` `Set.powerset`	—	`TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen` `isOpen_compl`

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`powerset_vietoris` 📖	mathematical	`IsCompact`	`IsCompact` `Set` `TopologicalSpace.vietoris` `Set.powerset`	—	`instIsEmptyFalse`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`powerset_vietoris` 📖	mathematical	`IsOpen`	`IsOpen` `Set` `TopologicalSpace.vietoris` `Set.powerset`	—	`TopologicalSpace.isOpen_generateFrom_of_mem`

TopologicalSpace

Definitions

Name	Category	Theorems
`vietoris` 📖	CompOp	17 math math: `vietoris.specializes_of_subset_closure`, `IsTopologicalBasis.vietoris`, `Compacts.isEmbedding_coe`, `vietoris.specializes_closure`, `vietoris.isClopen_singleton_empty`, `NonemptyCompacts.isEmbedding_coe`, `vietoris.instCompactSpaceSet`, `vietoris.isClosed_inter_nonempty_of_isClosed`, `Compacts.continuous_coe`, `vietoris.isTopologicalBasis`, `vietoris.isOpen_inter_nonempty_of_isOpen`, `IsOpen.powerset_vietoris`, `IsClosed.powerset_vietoris`, `TotallyBounded.nhds_vietoris_le_nhds_hausdorff`, `IsCompact.powerset_vietoris`, `NonemptyCompacts.continuous_coe`, `IsCompact.nhds_hausdorff_eq_nhds_vietoris`

TopologicalSpace.Compacts

Definitions

Name	Category	Theorems
`topology` 📖	CompOp	21 math math: `isClosed_subsets_of_isClosed`, `isEmbedding_coe`, `isClosed_inter_nonempty_of_isClosed`, `isClopen_singleton_bot`, `TopologicalSpace.IsTopologicalBasis.compacts`, `instCompactSpace`, `TopologicalSpace.NonemptyCompacts.continuous_toCompacts`, `compactSpace_iff`, `continuous_coe`, `isOpen_inter_nonempty_of_isOpen`, `TopologicalSpace.NonemptyCompacts.isOpenEmbedding_toCompacts`, `instNoncompactSpace`, `noncompactSpace_iff`, `continuous_toCloseds`, `isTopologicalBasis`, `isClosedEmbedding_toCloseds`, `isCompact_subsets_of_isCompact`, `isEmbedding_toCloseds`, `isOpen_subsets_of_isOpen`, `TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts`, `TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCompacts`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactSpace_iff` 📖	mathematical	—	`CompactSpace` `TopologicalSpace.Compacts` `topology`	—	`Set.biUnion_univ` `Set.mem_singleton` `isCompact_biUnion_coe_of_isCompact` `isCompact_univ` `instCompactSpace`
`continuous_coe` 📖	mathematical	—	`Continuous` `TopologicalSpace.Compacts` `Set` `topology` `TopologicalSpace.vietoris` `SetLike.coe` `instSetLike`	—	`Topology.IsEmbedding.continuous` `isEmbedding_coe`
`instCompactSpace` 📖	mathematical	—	`CompactSpace` `TopologicalSpace.Compacts` `topology`	—	`isCompact_subsets_of_isCompact` `isCompact_univ`
`instNoncompactSpace` 📖	mathematical	—	`NoncompactSpace` `TopologicalSpace.Compacts` `topology`	—	`noncompactSpace_iff`
`isClopen_singleton_bot` 📖	mathematical	—	`IsClopen` `TopologicalSpace.Compacts` `topology` `Set` `Set.instSingletonSet` `Bot.bot` `instBot`	—	`coe_bot` `Set.image_singleton` `Function.Injective.preimage_image` `SetLike.coe_injective` `IsClopen.preimage` `TopologicalSpace.vietoris.isClopen_singleton_empty` `continuous_coe`
`isClosed_inter_nonempty_of_isClosed` 📖	mathematical	—	`IsClosed` `TopologicalSpace.Compacts` `topology` `setOf` `Set.Nonempty` `Set` `Set.instInter` `SetLike.coe` `instSetLike`	—	`compl_compl` `IsOpen.isClosed_compl` `isOpen_subsets_of_isOpen` `IsClosed.isOpen_compl`
`isClosed_subsets_of_isClosed` 📖	mathematical	—	`IsClosed` `TopologicalSpace.Compacts` `topology` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`isOpen_inter_nonempty_of_isOpen` `IsClosed.isOpen_compl`
`isCompact_biUnion_coe_of_isCompact` 📖	mathematical	`IsCompact` `TopologicalSpace.Compacts` `topology`	`IsCompact` `Set.iUnion` `TopologicalSpace.Compacts` `Set` `Set.instMembership` `SetLike.coe` `instSetLike`	—	`isCompact_iff_finite_subcover` `IsCompact.elim_finite_subcover` `isOpen_subsets_of_isOpen` `isOpen_biUnion` `Set.mem_iUnion` `isCompact` `Set.iUnion₂_subset_iff` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.biUnion_subset_biUnion_left` `Set.biUnion_iUnion` `Finset.set_biUnion_biUnion` `Set.subset_iUnion₂_of_subset`
`isCompact_subsets_of_isCompact` 📖	mathematical	`IsCompact`	`IsCompact` `TopologicalSpace.Compacts` `topology` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`Topology.IsEmbedding.isCompact_iff` `isEmbedding_coe` `IsCompact.of_subset_of_specializes` `IsCompact.powerset_vietoris` `IsCompact.inter_right` `isClosed_closure` `Set.mem_image_of_mem` `Set.inter_subset_left` `TopologicalSpace.vietoris.specializes_of_subset_closure` `Set.subset_inter` `subset_closure` `Set.inter_subset_right`
`isEmbedding_coe` 📖	mathematical	—	`Topology.IsEmbedding` `TopologicalSpace.Compacts` `Set` `topology` `TopologicalSpace.vietoris` `SetLike.coe` `instSetLike`	—	`SetLike.coe_injective`
`isOpen_inter_nonempty_of_isOpen` 📖	mathematical	`IsOpen`	`IsOpen` `TopologicalSpace.Compacts` `topology` `setOf` `Set.Nonempty` `Set` `Set.instInter` `SetLike.coe` `instSetLike`	—	`Continuous.isOpen_preimage` `continuous_coe` `TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen`
`isOpen_subsets_of_isOpen` 📖	mathematical	`IsOpen`	`IsOpen` `TopologicalSpace.Compacts` `topology` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`Continuous.isOpen_preimage` `continuous_coe` `IsOpen.powerset_vietoris`
`isTopologicalBasis` 📖	mathematical	—	`TopologicalSpace.IsTopologicalBasis` `TopologicalSpace.Compacts` `topology` `Set.image` `Set` `setOf` `Set.instHasSubset` `SetLike.coe` `instSetLike` `Set.sUnion` `Set.Finite`	—	`TopologicalSpace.IsTopologicalBasis.compacts` `TopologicalSpace.isTopologicalBasis_opens`
`noncompactSpace_iff` 📖	mathematical	—	`NoncompactSpace` `TopologicalSpace.Compacts` `topology`	—	—

TopologicalSpace.IsTopologicalBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compacts` 📖	mathematical	`TopologicalSpace.IsTopologicalBasis`	`TopologicalSpace.IsTopologicalBasis` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.topology` `Set.image` `Set` `setOf` `Set.instHasSubset` `SetLike.coe` `TopologicalSpace.Compacts.instSetLike` `Set.sUnion` `Set.Finite`	—	`isTopologicalBasis_of_exists_subset` `isInducing` `Topology.IsEmbedding.isInducing` `TopologicalSpace.Compacts.isEmbedding_coe` `vietoris` `Set.setOf_forall` `IsOpen.inter` `TopologicalSpace.Compacts.isOpen_subsets_of_isOpen` `isOpen_sUnion` `isOpen` `Set.Finite.isOpen_biInter` `TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen` `open_eq_sUnion` `Eq.subset` `Set.instReflSubset` `Set.exists_mem_image` `IsCompact.elim_finite_subcover_image` `TopologicalSpace.Compacts.isCompact` `Set.sUnion_eq_biUnion` `Set.mem_sUnion` `Set.mem_sUnion_of_mem`
`nonemptyCompacts` 📖	mathematical	`TopologicalSpace.IsTopologicalBasis`	`TopologicalSpace.IsTopologicalBasis` `TopologicalSpace.NonemptyCompacts` `TopologicalSpace.NonemptyCompacts.topology` `Set.image` `Set` `setOf` `Set.instHasSubset` `SetLike.coe` `TopologicalSpace.NonemptyCompacts.instSetLike` `Set.sUnion` `Set.Finite` `Set.Nonempty`	—	`isTopologicalBasis_of_exists_subset` `isInducing` `Topology.IsEmbedding.isInducing` `TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts` `compacts` `Set.setOf_forall` `IsOpen.inter` `TopologicalSpace.NonemptyCompacts.isOpen_subsets_of_isOpen` `isOpen_sUnion` `isOpen` `Set.Finite.isOpen_biInter` `TopologicalSpace.NonemptyCompacts.isOpen_inter_nonempty_of_isOpen` `Set.eq_empty_or_nonempty` `Set.Nonempty.mono` `TopologicalSpace.NonemptyCompacts.nonempty` `Set.sUnion_empty` `Set.exists_mem_image` `subset_refl` `Set.instReflSubset`
`vietoris` 📖	mathematical	`TopologicalSpace.IsTopologicalBasis`	`TopologicalSpace.IsTopologicalBasis` `Set` `TopologicalSpace.vietoris` `Set.image` `setOf` `Set.instHasSubset` `IsOpen` `Set.Finite`	—	`isTopologicalBasis_of_exists_subset` `TopologicalSpace.vietoris.isTopologicalBasis` `Set.forall_mem_image` `Set.setOf_forall` `IsOpen.inter` `IsOpen.powerset_vietoris` `Set.Finite.isOpen_biInter` `TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen` `isOpen` `Set.exists_mem_image` `isOpen_sUnion` `Set.Finite.image` `Set.Nonempty.mono` `Set.inter_subset_inter` `subset_refl` `Set.instReflSubset` `exists_subset_of_mem_open` `Function.sometimes_spec`

TopologicalSpace.NonemptyCompacts

Definitions

Name	Category	Theorems
`topology` 📖	CompOp	24 math math: `isEmbedding_coe`, `continuous_toCompacts`, `isOpen_inter_nonempty_of_isOpen`, `isEmbedding_toCloseds`, `isOpen_subsets_of_isOpen`, `GromovHausdorff.toGHSpace_continuous`, `isClosed_inter_nonempty_of_isClosed`, `isClosedEmbedding_toCloseds`, `isOpenEmbedding_toCompacts`, `instCompactSpace`, `noncompactSpace_iff`, `TopologicalSpace.IsTopologicalBasis.nonemptyCompacts`, `continuous_toCloseds`, `instNoncompactSpace`, `EMetric.NonemptyCompacts.isClosed_subsets_of_isClosed`, `EMetric.NonemptyCompacts.continuous_toCloseds`, `continuous_coe`, `isEmbedding_toCompacts`, `compactSpace_iff`, `isCompact_subsets_of_isCompact`, `isTopologicalBasis`, `isClosedEmbedding_toCompacts`, `isClosed_subsets_of_isClosed`, `instSecondCountableTopology`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactSpace_iff` 📖	mathematical	—	`CompactSpace` `TopologicalSpace.NonemptyCompacts` `topology`	—	`Set.biUnion_univ` `Set.mem_singleton` `isCompact_biUnion_coe_of_isCompact` `isCompact_univ` `instCompactSpace`
`continuous_coe` 📖	mathematical	—	`Continuous` `TopologicalSpace.NonemptyCompacts` `Set` `topology` `TopologicalSpace.vietoris` `SetLike.coe` `instSetLike`	—	`Topology.IsEmbedding.continuous` `isEmbedding_coe`
`continuous_toCompacts` 📖	mathematical	—	`Continuous` `TopologicalSpace.NonemptyCompacts` `TopologicalSpace.Compacts` `topology` `TopologicalSpace.Compacts.topology` `toCompacts`	—	`Topology.IsEmbedding.continuous` `isEmbedding_toCompacts`
`instCompactSpace` 📖	mathematical	—	`CompactSpace` `TopologicalSpace.NonemptyCompacts` `topology`	—	`Topology.IsClosedEmbedding.compactSpace` `TopologicalSpace.Compacts.instCompactSpace` `isClosedEmbedding_toCompacts`
`instNoncompactSpace` 📖	mathematical	—	`NoncompactSpace` `TopologicalSpace.NonemptyCompacts` `topology`	—	`noncompactSpace_iff`
`isClosedEmbedding_toCompacts` 📖	mathematical	—	`Topology.IsClosedEmbedding` `TopologicalSpace.NonemptyCompacts` `TopologicalSpace.Compacts` `topology` `TopologicalSpace.Compacts.topology` `toCompacts`	—	`isEmbedding_toCompacts` `range_toCompacts` `IsClopen.isClosed` `IsClopen.compl` `TopologicalSpace.Compacts.isClopen_singleton_bot`
`isClosed_inter_nonempty_of_isClosed` 📖	mathematical	—	`IsClosed` `TopologicalSpace.NonemptyCompacts` `topology` `setOf` `Set.Nonempty` `Set` `Set.instInter` `SetLike.coe` `instSetLike`	—	`IsClosed.preimage` `continuous_coe` `TopologicalSpace.vietoris.isClosed_inter_nonempty_of_isClosed`
`isClosed_subsets_of_isClosed` 📖	mathematical	—	`IsClosed` `TopologicalSpace.NonemptyCompacts` `topology` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`IsClosed.preimage` `continuous_coe` `IsClosed.powerset_vietoris`
`isCompact_biUnion_coe_of_isCompact` 📖	mathematical	`IsCompact` `TopologicalSpace.NonemptyCompacts` `topology`	`IsCompact` `Set.iUnion` `TopologicalSpace.NonemptyCompacts` `Set` `Set.instMembership` `SetLike.coe` `instSetLike`	—	`Set.biUnion_image` `Set.iUnion_congr_Prop` `TopologicalSpace.Compacts.isCompact_biUnion_coe_of_isCompact` `IsCompact.image` `continuous_toCompacts`
`isCompact_subsets_of_isCompact` 📖	mathematical	`IsCompact`	`IsCompact` `TopologicalSpace.NonemptyCompacts` `topology` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`Topology.IsClosedEmbedding.isCompact_preimage` `isClosedEmbedding_toCompacts` `TopologicalSpace.Compacts.isCompact_subsets_of_isCompact`
`isEmbedding_coe` 📖	mathematical	—	`Topology.IsEmbedding` `TopologicalSpace.NonemptyCompacts` `Set` `topology` `TopologicalSpace.vietoris` `SetLike.coe` `instSetLike`	—	`SetLike.coe_injective`
`isEmbedding_toCompacts` 📖	mathematical	—	`Topology.IsEmbedding` `TopologicalSpace.NonemptyCompacts` `TopologicalSpace.Compacts` `topology` `TopologicalSpace.Compacts.topology` `toCompacts`	—	`induced_compose` `toCompacts_injective`
`isOpenEmbedding_toCompacts` 📖	mathematical	—	`Topology.IsOpenEmbedding` `TopologicalSpace.NonemptyCompacts` `TopologicalSpace.Compacts` `topology` `TopologicalSpace.Compacts.topology` `toCompacts`	—	`isEmbedding_toCompacts` `range_toCompacts` `IsClopen.isOpen` `IsClopen.compl` `TopologicalSpace.Compacts.isClopen_singleton_bot`
`isOpen_inter_nonempty_of_isOpen` 📖	mathematical	`IsOpen`	`IsOpen` `TopologicalSpace.NonemptyCompacts` `topology` `setOf` `Set.Nonempty` `Set` `Set.instInter` `SetLike.coe` `instSetLike`	—	`IsOpen.preimage` `continuous_coe` `TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen`
`isOpen_subsets_of_isOpen` 📖	mathematical	`IsOpen`	`IsOpen` `TopologicalSpace.NonemptyCompacts` `topology` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`IsOpen.preimage` `continuous_coe` `IsOpen.powerset_vietoris`
`isTopologicalBasis` 📖	mathematical	—	`TopologicalSpace.IsTopologicalBasis` `TopologicalSpace.NonemptyCompacts` `topology` `Set.image` `Set` `setOf` `Set.instHasSubset` `SetLike.coe` `instSetLike` `Set.sUnion` `Set.Finite` `Set.Nonempty`	—	`TopologicalSpace.IsTopologicalBasis.nonemptyCompacts` `TopologicalSpace.isTopologicalBasis_opens`
`noncompactSpace_iff` 📖	mathematical	—	`NoncompactSpace` `TopologicalSpace.NonemptyCompacts` `topology`	—	—

TopologicalSpace.vietoris

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCompactSpaceSet` 📖	mathematical	—	`CompactSpace` `Set` `TopologicalSpace.vietoris`	—	`IsCompact.powerset_vietoris` `isCompact_univ` `Set.powerset_univ`
`isClopen_singleton_empty` 📖	mathematical	—	`IsClopen` `Set` `TopologicalSpace.vietoris` `Set.instSingletonSet` `Set.instEmptyCollection`	—	`Set.powerset_empty` `IsClosed.powerset_vietoris` `isClosed_empty` `IsOpen.powerset_vietoris` `isOpen_empty`
`isClosed_inter_nonempty_of_isClosed` 📖	mathematical	—	`IsClosed` `Set` `TopologicalSpace.vietoris` `setOf` `Set.Nonempty` `Set.instInter`	—	`compl_compl` `IsOpen.isClosed_compl` `IsOpen.powerset_vietoris` `IsClosed.isOpen_compl`
`isOpen_inter_nonempty_of_isOpen` 📖	mathematical	`IsOpen`	`IsOpen` `Set` `TopologicalSpace.vietoris` `setOf` `Set.Nonempty` `Set.instInter`	—	`TopologicalSpace.isOpen_generateFrom_of_mem`
`isTopologicalBasis` 📖	mathematical	—	`TopologicalSpace.IsTopologicalBasis` `Set` `TopologicalSpace.vietoris` `Set.image` `setOf` `Set.instHasSubset` `Set.sUnion` `Set.Finite`	—	`TopologicalSpace.IsTopologicalBasis.isTopologicalBasis_of_exists_subset` `TopologicalSpace.isTopologicalBasis_of_subbasis` `Set.forall_mem_image` `Set.setOf_forall` `IsOpen.inter` `IsOpen.powerset_vietoris` `isOpen_sUnion` `Set.Finite.isOpen_biInter` `isOpen_inter_nonempty_of_isOpen` `Set.exists_mem_image` `Set.eq_empty_or_nonempty` `instIsEmptyFalse` `Set.sUnion_empty` `Set.inter_subset_right` `Set.inter_union_distrib_left` `Set.inter_eq_left` `Set.exists_subset_image_finite_and` `Set.finite_union` `Set.Finite.isOpen_sInter` `Set.sInter_union` `Set.ext` `Set.sInter_image` `Set.sUnion_insert` `Set.sUnion_image` `Set.mem_iInter₂` `Set.mem_powerset_iff` `Set.mem_inter_iff` `Set.Finite.image` `Set.mem_iInter₂_of_mem`
`specializes_closure` 📖	mathematical	—	`Specializes` `Set` `TopologicalSpace.vietoris` `closure`	—	`specializes_of_subset_closure` `subset_closure` `Set.Subset.rfl`
`specializes_of_subset_closure` 📖	mathematical	`Set` `Set.instHasSubset` `closure`	`Specializes` `Set` `TopologicalSpace.vietoris`	—	`TopologicalSpace.nhds_generateFrom` `iInf₂_le` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.mem_image_of_mem` `mem_closure_iff`

---

← Back to Index