English
Let X be a lattice with a Jordan–Holder structure and s a Composition Series with positive length. For any element x, x ∈ s.eraseLast iff x ≠ s.last and x ∈ s.
Русский
Пусть X — решётка с структурой Джордан-Холдер, и s — композиционная последовательность с положительной длиной. Тогда для любого элемента x выполняется: x ∈ s.eraseLast тогда и только тогда, когда x ≠ s.last и x ∈ s.
LaTeX
$$$\\forall X \\text{ with a lattice structure and } s:\\text{CompositionSeries }X,\\; 0< s.length \\Rightarrow (x \\in s.eraseLast \\iff (x \\neq s.last \\land x \\in s)).$$$
Lean4
theorem mem_eraseLast {s : CompositionSeries X} {x : X} (h : 0 < s.length) : x ∈ s.eraseLast ↔ x ≠ s.last ∧ x ∈ s :=
by
simp only [RelSeries.mem_def, eraseLast]
constructor
· rintro ⟨i, rfl⟩
have hi : (i : ℕ) < s.length := by omega
simp [last, Fin.ext_iff, ne_of_lt hi, -Set.mem_range, Set.mem_range_self]
· intro h
exact mem_eraseLast_of_ne_of_mem h.1 h.2
