lt_nil_empty — Mathlib

English

No element is strictly less than the nil element; the set of elements below nil is empty.

Русский

Нет элементов строго меньше нуля; множество элементов меньше нуля пусто.

LaTeX

$$$$\\{m\\;|\\; m < \\mathrm{nil}\\} = \\emptyset$$$$

Lean4

theorem lt_nil_empty {I} [LinearOrder I] : {m : Products I | m < Products.nil} = ∅ :=
  by
  ext ⟨m, hm⟩
  refine ⟨fun h ↦ ?_, by tauto⟩
  simp only [Set.mem_setOf_eq, lt_iff_lex_lt, nil, List.not_lex_nil] at h

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