mem_initSeg — Mathlib

English

Membership in initSeg s is characterized by equality of cardinalities and the Colex order relation: t ∈ initSeg s iff |s|=|t| and toColex t ≤ toColex s.

Русский

Членство в initSeg s определяется равенством кардинальностей и отношением колекс: t ∈ initSeg s тогда и только если |s|=|t| и toColex t ≤ toColex s.

LaTeX

$$$t \in initSeg(s) \iff |s|=|t| \land toColex\,t \le toColex\,s$$$

Lean4

@[simp]
theorem mem_initSeg : t ∈ initSeg s ↔ #s = #t ∧ toColex t ≤ toColex s := by simp [initSeg]

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