le_iff_toReal_le
plain-language theorem explainer
The equivalence between the order on recovered reals and the standard real order under the transport map. Foundation-layer work cites it when moving inequalities across the wrapper. The proof is immediate by reflexivity because the order on LogicReal is defined by pullback along toReal.
Claim. For all $x, y$ in the recovered reals, $x$ is less than or equal to $y$ if and only if the image of $x$ under the transport map to the standard reals is less than or equal to the image of $y$.
background
LogicReal is the wrapper around Mathlib's Bourbaki completion of the rationals, built from the recovered LogicRat layer. The map toReal sends each LogicReal to the corresponding Mathlib real via CompareReals.compareEquiv. The module recovers the reals from the Law-of-Logic rationals by completing those rationals and defining all algebra and order by transport along toReal.
proof idea
One-line wrapper that applies Iff.rfl. The order relation on LogicReal is defined precisely so that the desired equivalence holds by construction.
why it matters
It supplies the order transport needed by downstream results such as sqrtL_nonneg in LogicRealTranscendentals. The declaration belongs to the transport-first API that lets every recovered-real theorem reduce to a standard real theorem and be read back. In the Recognition framework it completes the step from LogicRat to the completed reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.