Infty

Stream: new members

[tsuki hao]

import Mathlib

theorem toReal_mono (hb : b ≠ ∞) (h : a ≤ b) : a.toReal ≤ b.toReal := by sorry

Can b is not infinite be formalized as b \neq \infty?If not, how should it be modified? :sob:

[Adam Topaz]

What is the type of b?

[tsuki hao]

Adam Topaz said:

What is the type of b?

I tried EReal，but failed :sob: ,I'd like to ask how to find out what space should I OPEN :face_holding_back_tears:

[Alex J. Best]

There is no notation ∞ scoped for EReal. There is for ENNReal but you are better off deciding what type you want to describe your problem first. And then setting up whatever notation you like later.

open scoped ENNReal
#check (∞ : ENNReal)

[Daniel Weber]

For EReal there's ⊤