Theorems · Definition · general topology
WithZeroTopology.topologicalSpace
{Γ₀ : Type u_2} → [LinearOrderedCommGroupWithZero Γ₀] → TopologicalSpace Γ₀The topology on a linearly ordered commutative group with a zero element adjoined.
A subset U is open if 0 ∉ U or if there is an invertible element γ₀ such that
{γ | γ < γ₀} ⊆ U.
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- iInfproof · cited by 1,690
- Set.Iioproof · cited by 1,166
- Filter.principalproof · cited by 740
- LinearOrderedCommGroupWithZerostatement and proof · cited by 528
- nhdsAdjointproof · cited by 9
Cited by27
Results whose statement or proof uses this declaration.
- WithZeroTopology.nhds_of_ne_zerostatement · cited by 8
- WithZeroTopology.tendsto_of_ne_zerostatement · cited by 5
- WithZeroTopology.hasBasis_nhds_zerostatement · cited by 4
- Valued.continuous_extensionstatement · cited by 2
- Valued.continuous_valuationstatement · cited by 2
- Valued.continuous_valuation_of_surjectivestatement · cited by 2
- WithZeroTopology.hasBasis_nhds_of_ne_zerostatement · cited by 2
- WithZeroTopology.nhds_zerostatement · cited by 2
- WithZeroTopology.tendsto_zerostatement · cited by 2
- Valued.valuation_isClosedMapstatement · cited by 1
- LaurentSeries.valuation_LaurentSeries_equal_extensionstatement · cited by 1
- WithZeroTopology.Iio_mem_nhdsstatement · cited by 1