Revision #341 → #1634 · back to history
addedTotal orderd5a392860cd6
addedReflexivity from strong connectedness228100e8f892
addedTotally ordered sete726f177fb14
addedLinear extensionc3b1bfaa6dad
addedStrict total order associatedf141246754e8
addedReflexive closure of strict total ordercb625b2ace9b
addedStrict total order545caba0d0db
addedAsymmetry from transitivity and irreflexivity8e69690f88d0
addedSubset of totally ordered seta0e40d08bd52
addedOrder on empty setb6c56bef23c0
addedOrdinal numbers6fd423d30d1f
addedInduced order via injective functionbbf6e536072b
addedLexicographical order on a product86ef72a7738f
addedReal numbers totally ordereddd102789b340
addedNatural numbers as initial total order7e55901ad32a
addedIntegers as initial total orderf80618e9e99f
addedRational numbers as initial total ordera86a33b7dd1c
addedReal numbers as initial unbounded total order043812aa98e7
addedOrdered fields179f332c9eb0
addedDedekind-complete ordered field13eaba8df340
addedAlphabet dictionary orderbe5e72141563
addedZorn's lemma6a08f6c9f3e4
addedAscending and descending chainc47afd0d345a
addedDescending chain conditionec2adefa4bd9
addedNoetherian ringa307e15c3d25
addedLength of a chaind1b925413adc
addedTotal order as a lattice0e89a120d27c
addedTotally ordered set is distributive lattice61bcb8207260
addedFinite total order is a well ordera1702114b608
addedFinite total order isomorphic to initial segmentc886c1c7fa95
addedTotal order induces bijectiona0b2169e6f3d
addedTosets as full subcategoryba3621bc66f6
addedOrder-respecting bijection is isomorphism84dce8237c62
addedOpen intervalsdaf1a9b29e31
addedOrder topology88044c5d9cdf
addedOrder topology is hereditarily normal8f26d9fc47a4
addedComplete totally ordered setb7a10720ba55
addedConnected order topology implies complete828d685564ed
addedConnectedness iff complete with no gap38095859be46
addedCompleteness iff closed bounded sets compactacc0722f129e
addedComplete lattice total order is compact8470bd3ce724
addedSum of two ordersf4cd24c79c00
addedSum over an index setb99fa737799e
addedLexicographical order on productb31c23ba7bbf
addedProduct order079d26838972
addedReflexive closure of direct productc90cdc85e27c
addedReal function defines strict weak order997fa1d7ab7e
addedPartial orderbcb4829073a1
addedTotally ordered group10939db6eced