Theorems · Theorem · real analysis

EReal.le_iff_sign

∀ {x y : EReal},
  x ≤ y ↔
    SignType.sign x < SignType.sign y ∨
      SignType.sign x = SignType.neg ∧ SignType.sign y = SignType.neg ∧ y.abs ≤ x.abs ∨
        SignType.sign x = SignType.zero ∧ SignType.sign y = SignType.zero ∨
          SignType.sign x = SignType.pos ∧ SignType.sign y = SignType.pos ∧ x.abs ≤ y.abs

Defined in

Mathlib.Data.EReal.Inv

Cited by

0 results in Mathlib

Foundations

Depth 130 from the axioms · uses propext, Classical.choice, Quot.sound