Documentation Verification Report

Clopen

📁 Source: Mathlib/Topology/Clopen.lean

Statistics

Metric	Count
Definitions	0
Theorems `preimage_isClopen_of_isClopen`, `compl`, `diff`, `frontier_eq`, `himp`, `inter`, `isClosed`, `isOpen`, `preimage`, `prod`, `union`, `isClopen_biInter`, `isClopen_biUnion`, `isClopen_preimage`, `continuousOn_boolIndicator_iff_isClopen`, `continuous_boolIndicator_iff_isClopen`, `isClopen_biInter_finset`, `isClopen_biUnion_finset`, `isClopen_compl_iff`, `isClopen_discrete`, `isClopen_empty`, `isClopen_iInter_of_finite`, `isClopen_iUnion_of_finite`, `isClopen_iff_frontier_eq_empty`, `isClopen_inter_of_disjoint_cover_clopen`, `isClopen_inter_of_disjoint_cover_clopen'`, `isClopen_of_disjoint_cover_open`, `isClopen_range_inl`, `isClopen_range_inr`, `isClopen_range_sigmaMk`, `isClopen_univ`	31
Total	31

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage_isClopen_of_isClopen` 📖	mathematical	`ContinuousOn` `IsClopen`	`IsClopen` `Set` `Set.instInter` `Set.preimage`	—	`preimage_isClosed_of_isClosed` `isOpen_inter_preimage`

IsClopen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl` 📖	mathematical	`IsClopen`	`IsClopen` `Compl.compl` `Set` `Set.instCompl`	—	`IsOpen.isClosed_compl` `IsClosed.isOpen_compl`
`diff` 📖	mathematical	`IsClopen`	`IsClopen` `Set` `Set.instSDiff`	—	`inter` `compl`
`frontier_eq` 📖	mathematical	`IsClopen`	`frontier` `Set` `Set.instEmptyCollection`	—	`isClopen_iff_frontier_eq_empty`
`himp` 📖	mathematical	`IsClopen`	`IsClopen` `HImp.himp` `Set` `Set.instHImp`	—	`himp_eq` `union` `compl`
`inter` 📖	mathematical	`IsClopen`	`IsClopen` `Set` `Set.instInter`	—	`IsClosed.inter` `IsOpen.inter`
`isClosed` 📖	mathematical	`IsClopen`	`IsClosed`	—	—
`isOpen` 📖	mathematical	`IsClopen`	`IsOpen`	—	—
`preimage` 📖	mathematical	`IsClopen` `Continuous`	`IsClopen` `Set.preimage`	—	`IsClosed.preimage` `IsOpen.preimage`
`prod` 📖	mathematical	`IsClopen`	`IsClopen` `instTopologicalSpaceProd` `SProd.sprod` `Set` `Set.instSProd`	—	`IsClosed.prod` `IsOpen.prod`
`union` 📖	mathematical	`IsClopen`	`IsClopen` `Set` `Set.instUnion`	—	`IsClosed.union` `IsOpen.union`

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClopen_biInter` 📖	mathematical	`IsClopen`	`IsClopen` `Set.iInter` `Set` `Set.instMembership`	—	`isClosed_biInter` `isOpen_biInter`
`isClopen_biUnion` 📖	mathematical	`IsClopen`	`IsClopen` `Set.iUnion` `Set` `Set.instMembership`	—	`isClosed_biUnion` `isOpen_biUnion`

Topology.IsQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClopen_preimage` 📖	mathematical	`Topology.IsQuotientMap`	`IsClopen` `Set.preimage`	—	`isClosed_preimage` `isOpen_preimage`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn_boolIndicator_iff_isClopen` 📖	mathematical	—	`ContinuousOn` `instTopologicalSpaceBool` `Set.boolIndicator` `IsClopen` `Set` `Set.instMembership` `instTopologicalSpaceSubtype` `Set.preimage`	—	`continuousOn_iff_continuous_restrict` `continuous_boolIndicator_iff_isClopen`
`continuous_boolIndicator_iff_isClopen` 📖	mathematical	—	`Continuous` `instTopologicalSpaceBool` `Set.boolIndicator` `IsClopen`	—	`continuous_bool_rng` `Set.preimage_boolIndicator_true`
`isClopen_biInter_finset` 📖	mathematical	`IsClopen`	`IsClopen` `Set.iInter` `Finset` `SetLike.instMembership` `Finset.instSetLike`	—	`Set.Finite.isClopen_biInter` `Finset.finite_toSet`
`isClopen_biUnion_finset` 📖	mathematical	`IsClopen`	`IsClopen` `Set.iUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike`	—	`Set.Finite.isClopen_biUnion` `Finset.finite_toSet`
`isClopen_compl_iff` 📖	mathematical	—	`IsClopen` `Compl.compl` `Set` `Set.instCompl`	—	`IsClopen.compl` `compl_compl`
`isClopen_discrete` 📖	mathematical	—	`IsClopen`	—	`isClosed_discrete` `isOpen_discrete`
`isClopen_empty` 📖	mathematical	—	`IsClopen` `Set` `Set.instEmptyCollection`	—	`isClosed_empty` `isOpen_empty`
`isClopen_iInter_of_finite` 📖	mathematical	`IsClopen`	`IsClopen` `Set.iInter`	—	`isClosed_iInter` `isOpen_iInter_of_finite`
`isClopen_iUnion_of_finite` 📖	mathematical	`IsClopen`	`IsClopen` `Set.iUnion`	—	`isClosed_iUnion_of_finite` `isOpen_iUnion`
`isClopen_iff_frontier_eq_empty` 📖	mathematical	—	`IsClopen` `frontier` `Set` `Set.instEmptyCollection`	—	`IsClopen.eq_1` `closure_eq_iff_isClosed` `interior_eq_iff_isOpen` `frontier.eq_1` `Set.diff_eq_empty` `Eq.subset` `Set.instReflSubset` `HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `interior_subset` `subset_closure`
`isClopen_inter_of_disjoint_cover_clopen` 📖	mathematical	`IsClopen` `Set` `Set.instHasSubset` `Set.instUnion` `IsOpen` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`IsClopen` `Set` `Set.instInter`	—	`IsClosed.inter` `isClosed_compl_iff` `HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Set.inter_subset_inter_right` `Disjoint.subset_compl_right` `Set.notMem_of_mem_compl` `IsOpen.inter`
`isClopen_inter_of_disjoint_cover_clopen'` 📖	mathematical	`IsClopen` `Set` `Set.instHasSubset` `Set.instUnion` `IsOpen` `Set.instInter` `Set.instEmptyCollection`	`IsClopen` `Set` `Set.instInter`	—	`isClopen_inter_of_disjoint_cover_clopen` `Set.inter_union_distrib_left` `Set.subset_inter` `Set.Subset.rfl` `IsOpen.inter` `Set.disjoint_iff_inter_eq_empty` `Set.inter_comm` `Set.inter_assoc` `Set.empty_inter`
`isClopen_of_disjoint_cover_open` 📖	mathematical	`Set` `Set.instHasSubset` `Set.univ` `Set.instUnion` `IsOpen` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	`IsClopen`	—	`isClopen_inter_of_disjoint_cover_clopen` `isClopen_univ` `Set.univ_inter`
`isClopen_range_inl` 📖	mathematical	—	`IsClopen` `instTopologicalSpaceSum` `Set.range`	—	`isClosed_range_inl` `isOpen_range_inl`
`isClopen_range_inr` 📖	mathematical	—	`IsClopen` `instTopologicalSpaceSum` `Set.range`	—	`isClosed_range_inr` `isOpen_range_inr`
`isClopen_range_sigmaMk` 📖	mathematical	—	`IsClopen` `instTopologicalSpaceSigma` `Set.range`	—	`Topology.IsClosedEmbedding.isClosed_range` `Topology.IsClosedEmbedding.sigmaMk` `Topology.IsOpenEmbedding.isOpen_range` `Topology.IsOpenEmbedding.sigmaMk`
`isClopen_univ` 📖	mathematical	—	`IsClopen` `Set.univ`	—	`isClosed_univ` `isOpen_univ`

---

← Back to Index