instNontrivial

Mathlib.Data.NNRat.Defs

URI: https://scilib.ai/kg/mathlib#NNRat.instNontrivial

English

There exist two distinct elements in the nonnegative rational numbers.

Русский

Существуют два различных элемента ℚ≥0.

LaTeX

$$$\exists a,b \in \mathbb{Q}_{\ge 0}, a \neq b$$$

Lean4

instance instNontrivial : Nontrivial ℚ≥0 where exists_pair_ne := ⟨1, 0, by decide⟩

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

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

Разделы

Аффилиация

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