97structure LogicSupported (K : Type*) [Mul K] [Zero K] [One K] [LT K] where 98 zero_lt_one_in_K : (0 : K) < 1 99 C : ComparisonOperatorOn K 100 identity : IdentityOn C 101 non_contradiction : NonContradictionOn C 102 scale_invariant : ScaleInvariantOn C 103 distinguishability : DistinguishabilityOn C 104 105/-- **Bootstrap theorem (named-hypothesis form)**: a linearly ordered 106field on which the Law of Logic is supported and which is Archimedean 107and conditionally complete is canonically isomorphic to `ℝ` as an 108ordered field. The Archimedean and conditional-completeness 109hypotheses are the analytic content the Law of Logic does not on its 110own provide; they are named here as inputs. 111 112The conclusion is the existence of an order-preserving ring 113isomorphism with `ℝ`. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.