preimage_coe_Ico

Mathlib.Data.EReal.Basic

URI: https://scilib.ai/kg/mathlib#EReal.preimage_coe_Ico

English

Real.toEReal^{-1}(Ico(x,y)) = Ico(x,y) for all x,y ∈ ℝ.

Русский

Real.toEReal^{-1}(Ico(x,y)) = Ico(x,y) для любых x,y ∈ ℝ.

LaTeX

$$$\\\\operatorname{Real.toEReal}^{-1}(\\\\mathrm{Ico}(x,y)) = \\\\mathrm{Ico}(x,y)$$$

Lean4

@[simp]
theorem preimage_coe_Ico (x y : ℝ) : Real.toEReal ⁻¹' Ico x y = Ico x y :=
  by
  simp_rw [← Ici_inter_Iio]
  simp

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru