English
There exists a lifting from EReal to ℝ defined on the finite elements (those not equal to ⊤ or ⊥); on finite elements, the lift agrees with the real value.
Русский
Существует частичное отображение из EReal в ℝ, определённое на конечных элементах (кроме ⊤ и ⊥); на конечных элементах отображение совпадает с вещественным значением.
LaTeX
$$$\exists L:\mathrm{EReal} \rightharpoonup \mathbb{R},\ \operatorname{dom}(L)=\mathrm{EReal}\setminus\{\top,\bot\},\ \forall r\in \mathbb{R},\ L(r_E)=r.$$$
Lean4
instance canLift : CanLift EReal ℝ (↑) fun r => r ≠ ⊤ ∧ r ≠ ⊥ where
prf x
hx := by
induction x
· simp at hx
· simp
· simp at hx
