lt_last_of_mem_eraseLast — Mathlib

English

Let s be a Composition Series with length > 0 and x ∈ s.eraseLast. Then x < s.last.

Русский

Пусть s — композиционная последовательность с длиной > 0 и x ∈ s.eraseLast. Тогда x < s.last.

LaTeX

$$$\\forall s:\\text{CompositionSeries }X,\\; \\forall x:\\,X,\\; 0< s.length \\rightarrow x \\in s.eraseLast \\rightarrow x < s.last.$$$

Lean4

theorem lt_last_of_mem_eraseLast {s : CompositionSeries X} {x : X} (h : 0 < s.length) (hx : x ∈ s.eraseLast) :
    x < s.last :=
  lt_of_le_of_ne (le_last_of_mem ((mem_eraseLast h).1 hx).2) ((mem_eraseLast h).1 hx).1

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