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`, `noncompactSpace_iff`, `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`, `noncompactSpace_iff`, `instCompactSpaceSet`, `isClopen_singleton_empty`, `isClosed_inter_nonempty_of_isClosed`, `isOpen_inter_nonempty_of_isOpen`, `specializes_closure`, `specializes_of_subset_closure`	38
Total	41

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`	`Set` `TopologicalSpace.vietoris` `Set.powerset`	—	`instIsEmptyFalse`

IsOpen

Theorems

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

TopologicalSpace

Definitions

Name	Category	Theorems
`vietoris` 📖	CompOp	15 math math: `vietoris.specializes_of_subset_closure`, `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.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	18 math math: `isClosed_subsets_of_isClosed`, `isEmbedding_coe`, `isClosed_inter_nonempty_of_isClosed`, `isClopen_singleton_bot`, `instCompactSpace`, `TopologicalSpace.NonemptyCompacts.continuous_toCompacts`, `compactSpace_iff`, `continuous_coe`, `isOpen_inter_nonempty_of_isOpen`, `TopologicalSpace.NonemptyCompacts.isOpenEmbedding_toCompacts`, `instNoncompactSpace`, `noncompactSpace_iff`, `continuous_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`	`Set.iUnion` `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`	`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`	`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`	`TopologicalSpace.Compacts` `topology` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`Continuous.isOpen_preimage` `continuous_coe` `IsOpen.powerset_vietoris`
`noncompactSpace_iff` 📖	mathematical	—	`NoncompactSpace` `TopologicalSpace.Compacts` `topology`	—	—

TopologicalSpace.NonemptyCompacts

Definitions

Name	Category	Theorems
`topology` 📖	CompOp	21 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`, `isOpenEmbedding_toCompacts`, `instCompactSpace`, `noncompactSpace_iff`, `continuous_toCloseds`, `instNoncompactSpace`, `EMetric.NonemptyCompacts.isClosed_subsets_of_isClosed`, `EMetric.NonemptyCompacts.continuous_toCloseds`, `continuous_coe`, `isEmbedding_toCompacts`, `compactSpace_iff`, `isCompact_subsets_of_isCompact`, `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`	`Set.iUnion` `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`	`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`	`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`	`TopologicalSpace.NonemptyCompacts` `topology` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`IsOpen.preimage` `continuous_coe` `IsOpen.powerset_vietoris`
`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`	`Set` `TopologicalSpace.vietoris` `setOf` `Set.Nonempty` `Set.instInter`	—	`TopologicalSpace.isOpen_generateFrom_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` `TopologicalSpace.vietoris`	—	`TopologicalSpace.nhds_generateFrom` `iInf₂_le` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.mem_image_of_mem` `mem_closure_iff`

---

← Back to Index