length_pos_of_nontrivial

Mathlib.Order.RelSeries

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

English

If the set {x | x ∈ s} is nontrivial, then 0 < s.length.

Русский

Если множество элементов s ненулево, то 0 < длина s.

LaTeX

$$(setOf fun x => RelSeries.membership.mem s x).Nontrivial \\Rightarrow 0 < s.length$$

Lean4

theorem length_pos_of_nontrivial (h : {x | x ∈ s}.Nontrivial) : 0 < s.length :=
  Nat.pos_iff_ne_zero.mpr <| length_ne_zero_of_nontrivial h

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

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

Разделы

Аффилиация

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