Basic

📁 Source: Mathlib/Topology/Basic.lean

Statistics

Metric	Count
Definitions `ofClosed`	1
Theorems `and`, `inter`, `isLocallyClosed`, `not`, `sdiff`, `union`, `and`, `isClosed_compl`, `isLocallyClosed`, `sdiff`, `union`, `isClosed_biUnion`, `isOpen_biInter`, `isOpen_sInter`, `ext`, `ext_iff`, `ext_iff_isClosed`, `ext_isClosed`, `isClosed_biInter`, `isClosed_biUnion_finset`, `isClosed_compl_iff`, `isClosed_const`, `isClosed_empty`, `isClosed_iInter`, `isClosed_iUnion_of_finite`, `isClosed_imp`, `isClosed_sInter`, `isClosed_univ`, `isOpen_biInter_finset`, `isOpen_biUnion`, `isOpen_compl_iff`, `isOpen_const`, `isOpen_empty`, `isOpen_fold`, `isOpen_iInter_of_finite`, `isOpen_iUnion`, `isOpen_iff_of_cover`, `isOpen_mk`, `le_nhds_lim`, `limUnder_of_not_tendsto`, `tendsto_nhds_limUnder`	41
Total	42

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`and` 📖	mathematical	—	`IsClosed` `setOf`	—	`inter`
`inter` 📖	mathematical	—	`IsClosed` `Set` `Set.instInter`	—	`isOpen_compl_iff` `Set.compl_inter` `IsOpen.union`
`isLocallyClosed` 📖	mathematical	—	`IsLocallyClosed`	—	`isOpen_univ` `Set.univ_inter`
`not` 📖	mathematical	—	`IsOpen` `setOf`	—	`isOpen_compl_iff`
`sdiff` 📖	mathematical	`IsOpen`	`IsClosed` `Set` `Set.instSDiff`	—	`inter` `isClosed_compl_iff`
`union` 📖	mathematical	—	`IsClosed` `Set` `Set.instUnion`	—	`Set.compl_union` `IsOpen.inter`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`and` 📖	—	`IsOpen` `setOf`	—	—	`inter`
`isClosed_compl` 📖	mathematical	`IsOpen`	`IsClosed` `Compl.compl` `Set` `Set.instCompl`	—	`isClosed_compl_iff`
`isLocallyClosed` 📖	mathematical	`IsOpen`	`IsLocallyClosed`	—	`isClosed_univ` `Set.inter_univ`
`sdiff` 📖	mathematical	`IsOpen`	`Set` `Set.instSDiff`	—	`inter` `IsClosed.isOpen_compl`
`union` 📖	mathematical	`IsOpen`	`Set` `Set.instUnion`	—	`Set.union_eq_iUnion` `isOpen_iUnion`

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed_biUnion` 📖	mathematical	`IsClosed`	`Set.iUnion` `Set` `Set.instMembership`	—	`Set.compl_iUnion` `isOpen_biInter`
`isOpen_biInter` 📖	mathematical	`IsOpen`	`Set.iInter` `Set` `Set.instMembership`	—	`isOpen_sInter` `image` `Set.forall_mem_image` `Set.sInter_image`
`isOpen_sInter` 📖	mathematical	`IsOpen`	`Set.sInter`	—	`induction_on` `Set.sInter_empty` `isOpen_univ` `Set.sInter_insert` `IsOpen.inter`

TopologicalSpace

Definitions

Name	Category	Theorems
`ofClosed` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`IsOpen`	—	—	—
`ext_iff` 📖	mathematical	—	`IsOpen`	—	`ext`
`ext_iff_isClosed` 📖	mathematical	—	`IsClosed`	—	`ext_iff` `Function.Surjective.forall` `compl_surjective` `isOpen_compl_iff`
`ext_isClosed` 📖	—	`IsClosed`	—	—	`ext_iff_isClosed`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed_biInter` 📖	mathematical	`IsClosed`	`Set.iInter` `Set` `Set.instMembership`	—	`isClosed_iInter`
`isClosed_biUnion_finset` 📖	mathematical	`IsClosed`	`Set.iUnion` `Finset` `Finset.instMembership`	—	`Set.Finite.isClosed_biUnion` `Finset.finite_toSet`
`isClosed_compl_iff` 📖	mathematical	—	`IsClosed` `Compl.compl` `Set` `Set.instCompl` `IsOpen`	—	`isOpen_compl_iff` `compl_compl`
`isClosed_const` 📖	mathematical	—	`IsClosed` `setOf`	—	`isOpen_const`
`isClosed_empty` 📖	mathematical	—	`IsClosed` `Set` `Set.instEmptyCollection`	—	`isClosed_const`
`isClosed_iInter` 📖	mathematical	`IsClosed`	`Set.iInter`	—	`isClosed_sInter` `Set.forall_mem_range`
`isClosed_iUnion_of_finite` 📖	mathematical	`IsClosed`	`Set.iUnion`	—	`Set.compl_iUnion` `isOpen_iInter_of_finite`
`isClosed_imp` 📖	mathematical	`IsOpen` `setOf`	`IsClosed`	—	`IsClosed.union` `IsOpen.isClosed_compl`
`isClosed_sInter` 📖	mathematical	`IsClosed`	`Set.sInter`	—	`Set.compl_sInter` `Set.sUnion_image` `isOpen_biUnion`
`isClosed_univ` 📖	mathematical	—	`IsClosed` `Set.univ`	—	`isClosed_const`
`isOpen_biInter_finset` 📖	mathematical	`IsOpen`	`Set.iInter` `Finset` `Finset.instMembership`	—	`Set.Finite.isOpen_biInter` `Finset.finite_toSet`
`isOpen_biUnion` 📖	mathematical	`IsOpen`	`Set.iUnion` `Set` `Set.instMembership`	—	`isOpen_iUnion`
`isOpen_compl_iff` 📖	mathematical	—	`IsOpen` `Compl.compl` `Set` `Set.instCompl` `IsClosed`	—	`IsClosed.isOpen_compl`
`isOpen_const` 📖	mathematical	—	`IsOpen` `setOf`	—	—
`isOpen_empty` 📖	mathematical	—	`IsOpen` `Set` `Set.instEmptyCollection`	—	`Set.sUnion_empty` `isOpen_sUnion`
`isOpen_fold` 📖	mathematical	—	`TopologicalSpace.IsOpen` `IsOpen`	—	—
`isOpen_iInter_of_finite` 📖	mathematical	`IsOpen`	`Set.iInter`	—	`Set.Finite.isOpen_sInter` `Set.finite_range` `Set.forall_mem_range`
`isOpen_iUnion` 📖	mathematical	`IsOpen`	`Set.iUnion`	—	`isOpen_sUnion` `Set.forall_mem_range`
`isOpen_iff_of_cover` 📖	mathematical	`IsOpen` `Set.iUnion` `Set.univ`	`Set` `Set.instInter`	—	`IsOpen.inter` `Set.inter_univ` `Set.inter_comm` `Set.iUnion_inter` `isOpen_iUnion`
`isOpen_mk` 📖	mathematical	`Set.univ` `Set` `Set.instInter` `Set.sUnion`	`IsOpen`	—	—
`le_nhds_lim` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds`	`lim`	—	—
`limUnder_of_not_tendsto` 📖	mathematical	`Filter.Tendsto` `nhds`	`limUnder`	—	—
`tendsto_nhds_limUnder` 📖	mathematical	`Filter.Tendsto` `nhds`	`limUnder`	—	`le_nhds_lim`

---

← Back to Index