orderIsoIicCoe_symm_apply_coe

Mathlib.Data.ENNReal.Inv

URI: https://scilib.ai/kg/mathlib#ENNReal.orderIsoIicCoe_symm_apply_coe

English

For a ∈ NNReal and x ∈ (Iic a).Elem, ((orderIsoIicCoe a).symm x : ENNReal) = x.val in ENNReal.

Русский

Для a ∈ NNReal и x ∈ (Iic a).Elem выполняется (orderIsoIicCoe a).symm x = x как элемент ENNReal.

LaTeX

$$$$ ((orderIsoIicCoe\, a).symm\, x : \mathbb{R}_{\ge 0}^{\infty}) = x.val. $$$$

Lean4

@[simp]
theorem orderIsoIicCoe_symm_apply_coe (a : ℝ≥0) (b : Iic a) : ((orderIsoIicCoe a).symm b : ℝ≥0∞) = b :=
  rfl

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

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

Разделы

Аффилиация

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