length_pos

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#RelSeries.length_pos

English

For infinite-dimensional r, RelSeries.withLength r n has length n.

Русский

Для бесконечно размерного r, RelSeries.withLength r n имеет длину n.

LaTeX

$$$(RelSeries.withLength r n).length = n$$$

Lean4

theorem length_pos [r.IsIrrefl] : 0 < s.length ↔ {x | x ∈ s}.Nontrivial :=
  Nat.pos_iff_ne_zero.trans length_ne_zero

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

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

Разделы

Аффилиация

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