le_last_of_mem — Mathlib

English

If x ∈ s, then x ≤ s.last.

Русский

Если x принадлежит композиционной серии, то x ≤ последний элемент серии.

LaTeX

$$$\\forall {X} [\\mathrm{Lattice}\\ X] [\\mathrm{JordanHolderLattice}\\ X],\\ {s : \\mathrm{CompositionSeries}\\ X},\\ {x : X},\\ x \\in s \\to x \\le s.last.$$$

Lean4

theorem le_last_of_mem {s : CompositionSeries X} {x : X} (hx : x ∈ s) : x ≤ s.last :=
  let ⟨_i, hi⟩ := Set.mem_range.2 hx
  hi ▸ le_last _

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