NhdsKer

📁 Source: Mathlib/Topology/NhdsKer.lean

Statistics

Metric	Count
Definitions	0
Theorems `nhdsKer_eq`, `nhdsKer_subset`, `mem_nhdsKer`, `mem_nhdsKer_iff_specializes`, `mem_nhdsKer_singleton`, `nhdsKer_biUnion`, `nhdsKer_def`, `nhdsKer_empty`, `nhdsKer_eq_empty`, `nhdsKer_eq_nhdsKer_iff_nhdsSet`, `nhdsKer_iInter_subset`, `nhdsKer_iUnion`, `nhdsKer_inter_subset`, `nhdsKer_minimal`, `nhdsKer_mono`, `nhdsKer_nhdsKer`, `nhdsKer_pair`, `nhdsKer_pi`, `nhdsKer_prod`, `nhdsKer_sInter_subset`, `nhdsKer_sUnion`, `nhdsKer_singleton_eq_ker_nhds`, `nhdsKer_singleton_pi`, `nhdsKer_subset_nhdsKer`, `nhdsKer_subset_nhdsKer_iff_nhdsSet`, `nhdsKer_union`, `nhdsKer_univ`, `nhdsSet_nhdsKer`, `specializes_iff_nhdsKer_subset`, `subset_nhdsKer`, `subset_nhdsKer_iff`	31
Total	31

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhdsKer_eq` 📖	mathematical	`IsOpen`	`nhdsKer`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `nhdsKer_minimal` `Set.Subset.rfl` `subset_nhdsKer`
`nhdsKer_subset` 📖	mathematical	`IsOpen`	`Set` `Set.instHasSubset` `nhdsKer`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_nhdsKer` `nhdsKer_minimal`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_nhdsKer` 📖	mathematical	—	`Set` `Set.instMembership` `nhdsKer`	—	`nhdsKer_def`
`mem_nhdsKer_iff_specializes` 📖	mathematical	—	`Set` `Set.instMembership` `nhdsKer` `Specializes`	—	`Set.biUnion_of_singleton` `nhdsKer_iUnion`
`mem_nhdsKer_singleton` 📖	mathematical	—	`Set` `Set.instMembership` `nhdsKer` `Set.instSingletonSet` `Specializes`	—	`nhdsKer_singleton_eq_ker_nhds` `ker_nhds_eq_specializes` `Set.mem_setOf`
`nhdsKer_biUnion` 📖	mathematical	—	`nhdsKer` `Set.iUnion` `Set` `Set.instMembership`	—	`nhdsKer_iUnion`
`nhdsKer_def` 📖	mathematical	—	`nhdsKer` `Set.sInter` `setOf` `Set` `IsOpen` `Set.instHasSubset`	—	`Filter.HasBasis.ker` `hasBasis_nhdsSet` `Set.sInter_eq_biInter`
`nhdsKer_empty` 📖	mathematical	—	`nhdsKer` `Set` `Set.instEmptyCollection`	—	`IsOpen.nhdsKer_eq` `isOpen_empty`
`nhdsKer_eq_empty` 📖	mathematical	—	`nhdsKer` `Set` `Set.instEmptyCollection`	—	`eq_bot_mono` `subset_nhdsKer` `nhdsKer_empty`
`nhdsKer_eq_nhdsKer_iff_nhdsSet` 📖	mathematical	—	`nhdsKer` `nhdsSet`	—	—
`nhdsKer_iInter_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `nhdsKer` `Set.iInter`	—	`Monotone.map_iInf_le` `nhdsKer_mono`
`nhdsKer_iUnion` 📖	mathematical	—	`nhdsKer` `Set.iUnion`	—	`nhdsSet_iUnion` `Filter.ker_iSup`
`nhdsKer_inter_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `nhdsKer` `Set.instInter`	—	`Monotone.map_inf_le` `nhdsKer_mono`
`nhdsKer_minimal` 📖	mathematical	`Set` `Set.instHasSubset` `IsOpen`	`nhdsKer`	—	`nhdsKer_def` `Set.sInter_subset_of_mem`
`nhdsKer_mono` 📖	mathematical	—	`Monotone` `Set` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `nhdsKer`	—	`Filter.ker_mono` `nhdsSet_mono`
`nhdsKer_nhdsKer` 📖	mathematical	—	`nhdsKer`	—	`nhdsSet_nhdsKer`
`nhdsKer_pair` 📖	mathematical	—	`nhdsKer` `instTopologicalSpaceProd` `Set` `Set.instSingletonSet` `SProd.sprod` `Set.instSProd`	—	`nhdsKer_singleton_eq_ker_nhds` `nhds_prod_eq` `Filter.ker_prod`
`nhdsKer_pi` 📖	mathematical	—	`nhdsKer` `Pi.topologicalSpace` `Set.pi` `Set.univ`	—	`Set.biUnion_of_singleton` `nhdsKer_biUnion` `Set.iUnion_congr_Prop` `nhdsKer_singleton_pi` `Set.biUnion_univ_pi`
`nhdsKer_prod` 📖	mathematical	—	`nhdsKer` `instTopologicalSpaceProd` `SProd.sprod` `Set` `Set.instSProd`	—	`Set.biUnion_of_singleton` `nhdsKer_biUnion` `Set.iUnion_congr_Prop` `nhdsKer_pair` `Set.biUnion_prod`
`nhdsKer_sInter_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `nhdsKer` `Set.sInter` `Set.iInter` `Set.instMembership`	—	`Monotone.map_sInf_le` `nhdsKer_mono`
`nhdsKer_sUnion` 📖	mathematical	—	`nhdsKer` `Set.sUnion` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.sUnion_eq_biUnion` `nhdsKer_iUnion`
`nhdsKer_singleton_eq_ker_nhds` 📖	mathematical	—	`nhdsKer` `Set` `Set.instSingletonSet` `Filter.ker` `nhds`	—	`nhdsSet_singleton`
`nhdsKer_singleton_pi` 📖	mathematical	—	`nhdsKer` `Pi.topologicalSpace` `Set` `Set.instSingletonSet` `Set.pi` `Set.univ`	—	`nhdsKer_singleton_eq_ker_nhds` `nhds_pi` `Filter.ker_pi`
`nhdsKer_subset_nhdsKer` 📖	mathematical	`Set` `Set.instHasSubset`	`nhdsKer`	—	`nhdsKer_mono`
`nhdsKer_subset_nhdsKer_iff_nhdsSet` 📖	mathematical	—	`Set` `Set.instHasSubset` `nhdsKer` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsSet`	—	`Filter.HasBasis.ge_iff` `hasBasis_nhdsSet`
`nhdsKer_union` 📖	mathematical	—	`nhdsKer` `Set` `Set.instUnion`	—	`nhdsSet_union` `Filter.ker_sup`
`nhdsKer_univ` 📖	mathematical	—	`nhdsKer` `Set.univ`	—	`IsOpen.nhdsKer_eq` `isOpen_univ`
`nhdsSet_nhdsKer` 📖	mathematical	—	`nhdsSet` `nhdsKer`	—	`le_antisymm` `Filter.HasBasis.ge_iff` `hasBasis_nhdsSet` `IsOpen.mem_nhdsSet` `IsOpen.nhdsKer_subset` `nhdsSet_mono` `subset_nhdsKer`
`specializes_iff_nhdsKer_subset` 📖	mathematical	—	`Specializes` `Set` `Set.instHasSubset` `nhdsKer` `Set.instSingletonSet`	—	`nhdsSet_singleton`
`subset_nhdsKer` 📖	mathematical	—	`Set` `Set.instHasSubset` `nhdsKer`	—	`subset_nhdsKer_iff`
`subset_nhdsKer_iff` 📖	mathematical	—	`Set` `Set.instHasSubset` `nhdsKer`	—	`nhdsKer_def`

---

← Back to Index