WithZeroTopology

📁 Source: Mathlib/Topology/Algebra/WithZeroTopology.lean

Statistics

Metric	Count
Definitions `topologicalSpace`	1
Theorems `Iio_mem_nhds`, `Iio_mem_nhds_zero`, `hasBasis_nhds_of_ne_zero`, `hasBasis_nhds_units`, `hasBasis_nhds_zero`, `instContinuousInv₀`, `instContinuousMul`, `isClosed_iff`, `isOpen_Iio`, `isOpen_iff`, `nhds_coe_units`, `nhds_eq_update`, `nhds_of_ne_zero`, `nhds_zero`, `nhds_zero_of_units`, `orderClosedTopology`, `singleton_mem_nhds_of_ne_zero`, `singleton_mem_nhds_of_units`, `t5Space`, `tendsto_of_ne_zero`, `tendsto_units`, `tendsto_zero`	22
Total	23

WithZeroTopology

Definitions

Name	Category	Theorems
`topologicalSpace` 📖	CompOp	29 math math: `Valued.continuous_extension`, `nhds_zero`, `nhds_zero_of_units`, `tendsto_of_ne_zero`, `Iio_mem_nhds`, `Valued.continuous_valuation`, `hasBasis_nhds_of_ne_zero`, `IsValuativeTopology.continuous_valuation`, `Valued.continuous_extensionValuation`, `isClosed_iff`, `hasBasis_nhds_zero`, `Valued.valuation_isClosedMap`, `nhds_coe_units`, `nhds_of_ne_zero`, `LaurentSeries.valuation_LaurentSeries_equal_extension`, `isOpen_iff`, `instContinuousMul`, `t5Space`, `singleton_mem_nhds_of_ne_zero`, `LaurentSeries.tendsto_valuation`, `tendsto_units`, `Iio_mem_nhds_zero`, `tendsto_zero`, `orderClosedTopology`, `isOpen_Iio`, `singleton_mem_nhds_of_units`, `nhds_eq_update`, `hasBasis_nhds_units`, `instContinuousInv₀`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Iio_mem_nhds` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero`	`Set` `Filter` `Filter.instMembership` `nhds` `topologicalSpace` `Set.Iio`	—	`eq_or_ne` `LT.lt.ne'` `nhds_of_ne_zero`
`Iio_mem_nhds_zero` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `topologicalSpace` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero`	—	`Filter.HasBasis.mem_of_mem` `hasBasis_nhds_zero`
`hasBasis_nhds_of_ne_zero` 📖	mathematical	—	`Filter.HasBasis` `nhds` `topologicalSpace` `Set` `Set.instSingletonSet`	—	`nhds_of_ne_zero` `Filter.hasBasis_pure`
`hasBasis_nhds_units` 📖	mathematical	—	`Filter.HasBasis` `nhds` `topologicalSpace` `Units.val` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Set` `Set.instSingletonSet`	—	`hasBasis_nhds_of_ne_zero` `Units.ne_zero` `GroupWithZero.toNontrivial`
`hasBasis_nhds_zero` 📖	mathematical	—	`Filter.HasBasis` `nhds` `topologicalSpace` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero`	—	`nhds_zero` `Filter.hasBasis_biInf_principal` `directedOn_iff_directed` `Monotone.directed_ge` `SemilatticeInf.instIsCodirectedOrder` `Set.Iio_subset_Iio` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`
`instContinuousInv₀` 📖	mathematical	—	`ContinuousInv₀` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `topologicalSpace`	—	`ContinuousAt.eq_1` `nhds_of_ne_zero` `pure_le_nhds`
`instContinuousMul` 📖	mathematical	—	`ContinuousMul` `topologicalSpace` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero`	—	`eq_or_ne` `MulZeroClass.zero_mul` `Filter.HasBasis.tendsto_iff` `Filter.HasBasis.prod_nhds` `hasBasis_nhds_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `LT.lt.trans_eq` `mul_lt_mul''` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `MulPosStrictMono.toMulPosMono` `LinearOrderedCommMonoidWithZero.toMulPosStrictMono` `zero_le'` `mul_one` `nhds_prod_eq` `nhds_of_ne_zero` `Filter.prod_pure` `Filter.tendsto_map'_iff` `div_ne_zero` `mul_lt_mul_of_pos_right` `zero_lt_iff` `div_mul_cancel₀` `LT.lt.ne'` `LT.lt.trans_le` `Filter.prod_pure_pure` `pure_le_nhds` `Filter.Tendsto.comp` `le_of_not_ge` `Continuous.tendsto` `continuous_swap` `mul_comm`
`isClosed_iff` 📖	mathematical	—	`IsClosed` `topologicalSpace` `Set` `Set.instMembership` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Set.instHasSubset` `Set.Ici` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero`	—	—
`isOpen_Iio` 📖	mathematical	—	`IsOpen` `topologicalSpace` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero`	—	`isOpen_iff` `imp_iff_not_or` `ne_of_gt` `Set.Subset.rfl`
`isOpen_iff` 📖	mathematical	—	`IsOpen` `topologicalSpace` `Set` `Set.instMembership` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Set.instHasSubset` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero`	—	`isOpen_iff_mem_nhds` `and_forall_ne` `Filter.HasBasis.mem_iff` `hasBasis_nhds_zero` `nhds_of_ne_zero`
`nhds_coe_units` 📖	mathematical	—	`nhds` `topologicalSpace` `Units.val` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Filter` `Filter.instPure`	—	`nhds_of_ne_zero` `Units.ne_zero` `GroupWithZero.toNontrivial`
`nhds_eq_update` 📖	mathematical	—	`nhds` `topologicalSpace` `Function.update` `Filter` `LinearOrder.toDecidableEq` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Filter.instPure` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `iInf` `Filter.instInfSet` `Filter.principal` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`nhds_nhdsAdjoint` `sup_of_le_right` `le_iInf₂` `Filter.le_principal_iff` `zero_lt_iff`
`nhds_of_ne_zero` 📖	mathematical	—	`nhds` `topologicalSpace` `Filter` `Filter.instPure`	—	`nhds_nhdsAdjoint_of_ne`
`nhds_zero` 📖	mathematical	—	`nhds` `topologicalSpace` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `iInf` `Filter` `Filter.instInfSet` `Filter.principal` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero`	—	`nhds_eq_update` `Function.update_self`
`nhds_zero_of_units` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `topologicalSpace` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `Units.val` `MonoidWithZero.toMonoid`	—	`Iio_mem_nhds_zero` `Units.ne_zero` `GroupWithZero.toNontrivial`
`orderClosedTopology` 📖	mathematical	—	`OrderClosedTopology` `topologicalSpace` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero`	—	`nhds_prod_eq` `nhds_of_ne_zero` `LT.lt.ne'` `LE.le.trans_lt` `zero_le'` `Filter.pure_prod` `Iio_mem_nhds`
`singleton_mem_nhds_of_ne_zero` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `topologicalSpace` `Set.instSingletonSet`	—	`nhds_of_ne_zero`
`singleton_mem_nhds_of_units` 📖	mathematical	—	`Set` `Filter` `Filter.instMembership` `nhds` `topologicalSpace` `Units.val` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Set.instSingletonSet`	—	`nhds_of_ne_zero` `GroupWithZero.toNontrivial`
`t5Space` 📖	mathematical	—	`T5Space` `topologicalSpace`	—	`T2Space.t1Space` `OrderClosedTopology.to_t2Space` `orderClosedTopology` `Set.disjoint_left` `subset_closure` `IsOpen.nhdsSet_eq` `isOpen_iff` `disjoint_nhdsSet_principal` `disjoint_principal_nhdsSet`
`tendsto_of_ne_zero` 📖	mathematical	—	`Filter.Tendsto` `nhds` `topologicalSpace` `Filter.Eventually`	—	`nhds_of_ne_zero` `Filter.tendsto_pure`
`tendsto_units` 📖	mathematical	—	`Filter.Tendsto` `nhds` `topologicalSpace` `Units.val` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Filter.Eventually`	—	`tendsto_of_ne_zero` `Units.ne_zero` `GroupWithZero.toNontrivial`
`tendsto_zero` 📖	mathematical	—	`Filter.Tendsto` `nhds` `topologicalSpace` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `Filter.Eventually` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero`	—	`nhds_zero`

---

← Back to Index