NhdsSet

📁 Source: Mathlib/Topology/NhdsSet.lean

Statistics

Metric	Count
Definitions	0
Theorems `eventually_nhdsSet`, `self_of_nhdsSet`, `union`, `union_nhdsSet`, `self_of_nhdsSet`, `nhdsSet_interior`, `nhdsSet_le_sup`, `nhdsSet_le_sup'`, `mem_nhdsSet`, `mem_nhdsSet_self`, `nhdsSet_eq`, `nhdsSet_neBot`, `bUnion_mem_nhdsSet`, `disjoint_nhdsSet_principal`, `disjoint_principal_nhdsSet`, `eventually_nhdsSet_iUnion`, `eventually_nhdsSet_iUnion₂`, `eventually_nhdsSet_iff_exists`, `eventually_nhdsSet_iff_forall`, `hasBasis_nhdsSet`, `lift'_nhdsSet_interior`, `mem_nhdsSet_empty`, `mem_nhdsSet_iff_exists`, `mem_nhdsSet_iff_forall`, `mem_nhdsSet_interior`, `monotone_nhdsSet`, `nhdsSet_diagonal`, `nhdsSet_empty`, `nhdsSet_eq_bot_iff`, `nhdsSet_eq_principal_iff`, `nhdsSet_iInter_le`, `nhdsSet_iUnion`, `nhdsSet_insert`, `nhdsSet_inter_le`, `nhdsSet_interior`, `nhdsSet_le`, `nhdsSet_mono`, `nhdsSet_neBot_iff`, `nhdsSet_sInter_le`, `nhdsSet_singleton`, `nhdsSet_union`, `nhdsSet_univ`, `nhds_le_nhdsSet`, `principal_le_nhdsSet`, `subset_interior_iff_mem_nhdsSet`, `subset_of_mem_nhdsSet`, `union_mem_nhdsSet`	47
Total	47

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_nhdsSet` 📖	mathematical	`Filter.Eventually` `nhdsSet`	`nhds`	—	`eventually_nhdsSet_iff_forall` `eventually_nhds`
`self_of_nhdsSet` 📖	—	`Filter.Eventually` `nhdsSet` `Set` `Set.instMembership`	—	—	`principal_le_nhdsSet`
`union` 📖	mathematical	`Filter.Eventually` `nhdsSet`	`Set` `Set.instUnion`	—	`union_nhdsSet`
`union_nhdsSet` 📖	mathematical	—	`Filter.Eventually` `nhdsSet` `Set` `Set.instUnion`	—	`nhdsSet_union` `Filter.eventually_sup`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`self_of_nhdsSet` 📖	mathematical	`Filter.EventuallyEq` `nhdsSet`	`Set.EqOn`	—	`Filter.Eventually.self_of_nhdsSet`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhdsSet_interior` 📖	mathematical	`Filter.HasBasis` `nhdsSet`	`interior`	—	`lift'_interior` `lift'_nhdsSet_interior`

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhdsSet_le_sup` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsSet` `Filter.instSup` `Set` `Set.instInter` `Filter.principal` `Compl.compl` `Set.instCompl`	—	`Set.inter_union_compl` `nhdsSet_union` `le_imp_le_of_le_of_le` `sup_le_sup` `le_refl` `nhdsSet_mono` `Set.inter_subset_right` `IsOpen.nhdsSet_eq` `isOpen_compl`
`nhdsSet_le_sup'` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsSet` `Filter.instSup` `Set` `Set.instInter` `Filter.principal` `Compl.compl` `Set.instCompl`	—	`Set.inter_comm` `nhdsSet_le_sup`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_nhdsSet` 📖	mathematical	`IsOpen`	`Set` `Filter` `Filter.instMembership` `nhdsSet` `Set.instHasSubset`	—	`subset_interior_iff_mem_nhdsSet` `interior_eq`
`mem_nhdsSet_self` 📖	mathematical	`IsOpen`	`Set` `Filter` `Filter.instMembership` `nhdsSet`	—	`mem_nhdsSet` `Set.Subset.rfl`
`nhdsSet_eq` 📖	mathematical	`IsOpen`	`nhdsSet` `Filter.principal`	—	`nhdsSet_eq_principal_iff`

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhdsSet_neBot` 📖	mathematical	—	`Set.Nonempty`	—	`nhdsSet_neBot_iff`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bUnion_mem_nhdsSet` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`nhdsSet` `Set.iUnion` `Set.instMembership`	—	`mem_nhdsSet_iff_forall` `Filter.mem_of_superset` `Set.subset_iUnion₂`
`disjoint_nhdsSet_principal` 📖	mathematical	—	`Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `nhdsSet` `Filter.principal` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `closure`	—	`disjoint_comm` `disjoint_principal_nhdsSet`
`disjoint_principal_nhdsSet` 📖	mathematical	—	`Disjoint` `Filter` `Filter.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Filter.instCompleteLatticeFilter` `Filter.principal` `nhdsSet` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `closure`	—	`Filter.disjoint_principal_left` `subset_interior_iff_mem_nhdsSet` `interior_compl` `Set.subset_compl_iff_disjoint_left`
`eventually_nhdsSet_iUnion` 📖	mathematical	—	`Filter.Eventually` `nhdsSet` `Set.iUnion`	—	`nhdsSet_iUnion`
`eventually_nhdsSet_iUnion₂` 📖	mathematical	—	`Filter.Eventually` `nhdsSet` `Set.iUnion`	—	`nhdsSet_iUnion`
`eventually_nhdsSet_iff_exists` 📖	mathematical	—	`Filter.Eventually` `nhdsSet` `IsOpen` `Set` `Set.instHasSubset`	—	`mem_nhdsSet_iff_exists`
`eventually_nhdsSet_iff_forall` 📖	mathematical	—	`Filter.Eventually` `nhdsSet` `nhds`	—	`mem_nhdsSet_iff_forall`
`hasBasis_nhdsSet` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhdsSet` `IsOpen` `Set.instHasSubset`	—	—
`lift'_nhdsSet_interior` 📖	mathematical	—	`Filter.lift'` `nhdsSet` `interior`	—	`Filter.HasBasis.lift'_interior_eq_self` `hasBasis_nhdsSet`
`mem_nhdsSet_empty` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsSet` `Set.instEmptyCollection`	—	`nhdsSet_empty`
`mem_nhdsSet_iff_exists` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsSet` `IsOpen` `Set.instHasSubset`	—	`subset_interior_iff_mem_nhdsSet` `subset_interior_iff`
`mem_nhdsSet_iff_forall` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsSet` `nhds`	—	—
`mem_nhdsSet_interior` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhdsSet` `interior`	—	`subset_interior_iff_mem_nhdsSet` `Set.Subset.rfl`
`monotone_nhdsSet` 📖	mathematical	—	`Monotone` `Set` `Filter` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `Filter.instPartialOrder` `nhdsSet`	—	`nhdsSet_mono`
`nhdsSet_diagonal` 📖	mathematical	—	`nhdsSet` `Set.diagonal` `iSup` `Filter` `Filter.instSupSet` `nhds`	—	`nhdsSet.eq_1` `Set.range_diag` `Set.range_comp`
`nhdsSet_empty` 📖	mathematical	—	`nhdsSet` `Set` `Set.instEmptyCollection` `Bot.bot` `Filter` `Filter.instBot`	—	`IsOpen.nhdsSet_eq` `isOpen_empty` `Filter.principal_empty`
`nhdsSet_eq_bot_iff` 📖	mathematical	—	`nhdsSet` `Bot.bot` `Filter` `Filter.instBot` `Set` `Set.instEmptyCollection`	—	`nhds_neBot` `nhdsSet_empty`
`nhdsSet_eq_principal_iff` 📖	mathematical	—	`nhdsSet` `Filter.principal` `IsOpen`	—	`LE.le.ge_iff_eq'` `principal_le_nhdsSet` `Filter.le_principal_iff` `mem_nhdsSet_iff_forall` `isOpen_iff_mem_nhds`
`nhdsSet_iInter_le` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsSet` `Set.iInter` `iInf` `Filter.instInfSet`	—	`Monotone.map_iInf_le` `monotone_nhdsSet`
`nhdsSet_iUnion` 📖	mathematical	—	`nhdsSet` `Set.iUnion` `iSup` `Filter` `Filter.instSupSet`	—	`Set.image_iUnion` `sSup_iUnion`
`nhdsSet_insert` 📖	mathematical	—	`nhdsSet` `Set` `Set.instInsert` `Filter` `Filter.instSup` `nhds`	—	`Set.insert_eq` `nhdsSet_union` `nhdsSet_singleton`
`nhdsSet_inter_le` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsSet` `Set` `Set.instInter` `Filter.instInf`	—	`Monotone.map_inf_le` `monotone_nhdsSet`
`nhdsSet_interior` 📖	mathematical	—	`nhdsSet` `interior` `Filter.principal`	—	`IsOpen.nhdsSet_eq` `isOpen_interior`
`nhdsSet_le` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsSet` `nhds`	—	—
`nhdsSet_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsSet`	—	`sSup_le_sSup` `Set.image_mono`
`nhdsSet_neBot_iff` 📖	mathematical	—	`Filter.NeBot` `nhdsSet` `Set.Nonempty`	—	`not_iff_not`
`nhdsSet_sInter_le` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsSet` `Set.sInter` `iInf` `Set` `Filter.instInfSet` `Set.instMembership`	—	`Monotone.map_sInf_le` `monotone_nhdsSet`
`nhdsSet_singleton` 📖	mathematical	—	`nhdsSet` `Set` `Set.instSingletonSet` `nhds`	—	`Set.image_singleton` `sSup_singleton`
`nhdsSet_union` 📖	mathematical	—	`nhdsSet` `Set` `Set.instUnion` `Filter` `Filter.instSup`	—	`Set.image_union` `sSup_union`
`nhdsSet_univ` 📖	mathematical	—	`nhdsSet` `Set.univ` `Top.top` `Filter` `Filter.instTop`	—	`IsOpen.nhdsSet_eq` `isOpen_univ` `Filter.principal_univ`
`nhds_le_nhdsSet` 📖	mathematical	`Set` `Set.instMembership`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds` `nhdsSet`	—	`le_sSup` `Set.mem_image_of_mem`
`principal_le_nhdsSet` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal` `nhdsSet`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_interior_iff_mem_nhdsSet` `interior_subset`
`subset_interior_iff_mem_nhdsSet` 📖	mathematical	—	`Set` `Set.instHasSubset` `interior` `Filter` `Filter.instMembership` `nhdsSet`	—	—
`subset_of_mem_nhdsSet` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsSet`	`Set.instHasSubset`	—	`principal_le_nhdsSet`
`union_mem_nhdsSet` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsSet`	`Set.instUnion`	—	`nhdsSet_union` `Filter.union_mem_sup`

---

← Back to Index