coe_ne_coe

Mathlib.Data.ENNReal.Basic

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

English

Let p,q ∈ NNReal. Then (p : ENNReal) ≠ q iff p ≠ q.

Русский

Пусть p,q ∈ NNReal. Тогда (p : ENNReal) ≠ q тогда и только тогда, когда p ≠ q.

LaTeX

$$$ (p : \mathbb{R}_{\ge 0}^{\infty}) \neq q \iff p \neq q $$$

Lean4

theorem coe_ne_coe : (p : ℝ≥0∞) ≠ q ↔ p ≠ q :=
  coe_inj.not

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

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

Разделы

Аффилиация

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