def Hex.RCF.Cmp.toProp : Cmp → ℝ → ℝ → Prop

Interpret a reflected comparison between two real numbers.

Equations

• Hex.RCF.Cmp.lt.toProp x✝¹ x✝ = (x✝¹ < x✝)
• Hex.RCF.Cmp.le.toProp x✝¹ x✝ = (x✝¹ ≤ x✝)
• Hex.RCF.Cmp.eq.toProp x✝¹ x✝ = (x✝¹ = x✝)
• Hex.RCF.Cmp.ge.toProp x✝¹ x✝ = (x✝¹ ≥ x✝)
• Hex.RCF.Cmp.gt.toProp x✝¹ x✝ = (x✝¹ > x✝)
• Hex.RCF.Cmp.ne.toProp x✝¹ x✝ = (x✝¹ ≠ x✝)

def Hex.RCF.Atom.toProp (a : Atom) (x : ℝ) : Prop

Interpret an atomic polynomial comparison at a real point.

Equations

• a.toProp x = a.cmp.toProp ((Polynomial.aeval x) (HexPolyZMathlib.toPolynomial a.p)) 0

def Hex.RCF.Formula.toProp : Formula → ℝ → Prop

Interpret a reflected formula at a real point.

Equations

• (Hex.RCF.Formula.atom a).toProp x✝ = a.toProp x✝
• Hex.RCF.Formula.tt.toProp x✝ = True
• Hex.RCF.Formula.ff.toProp x✝ = False
• φ.not.toProp x✝ = ¬φ.toProp x✝
• (φ.and ψ).toProp x✝ = (φ.toProp x✝ ∧ ψ.toProp x✝)
• (φ.or ψ).toProp x✝ = (φ.toProp x✝ ∨ ψ.toProp x✝)
• (φ.imp ψ).toProp x✝ = (φ.toProp x✝ → ψ.toProp x✝)

def Hex.RCF.Sentence.toProp : Sentence → Prop

Interpret a reflected sentence as a Lean proposition.

Equations

• (Hex.RCF.Sentence.forallReal φ).toProp = ∀ (x : ℝ), φ.toProp x
• (Hex.RCF.Sentence.existsReal φ).toProp = ∃ (x : ℝ), φ.toProp x
• (Hex.RCF.Sentence.forallIoc a b φ).toProp = ∀ x ∈ Set.Ioc (HexRealRootsMathlib.Dyadic.toReal a) (HexRealRootsMathlib.Dyadic.toReal b), φ.toProp x
• (Hex.RCF.Sentence.existsIoc a b φ).toProp = ∃ x ∈ Set.Ioc (HexRealRootsMathlib.Dyadic.toReal a) (HexRealRootsMathlib.Dyadic.toReal b), φ.toProp x