definition of real.lt

Stream: new members

[Bart Michels]

Hi everyone. I have trouble using (and finding the definition of) "less than" for the reals.
docs#real.has_lt uses "lt", but I can't find the definition of lt in the right-hand side.

My guess is that every has_le structure is also a has_lt structure by defining a < b as (a \le b and not b \le a), but I can't seem to use h.1 when h : x < y.

[Ruben Van de Velde]

For some reason the lt definition is private - it's a few lines up in the source: https://github.com/leanprover-community/mathlib/blob/1a1895cd74de2b3272df34347fa37e69bea8d1b3/src/data/real/basic.lean#L137

[Kevin Buzzard]

Hi! You might be thinking about things the wrong way. Are you _sure_ you want to know how the reals work, under the hood? If you just want to develop some theory which uses the real numbers, then you should have everything you need. All the theorem about < will be there -- which one of them is the actual definition is an implementation issue and not relevant to mathematicians. Or are you precisely interested in implementation issue details for some reason?