insert — Mathlib

English

If s is a chain and every element of s is comparable with a new element a, then insert a s is a chain.

Русский

Если s цепь и каждый b ∈ s сравним с новым элементом a, то insert a s — цепь.

LaTeX

$$$\operatorname{IsChain}(r, \operatorname{insert}(a,s))$$$

Lean4

protected theorem insert (hs : IsChain r s) (ha : ∀ b ∈ s, a ≠ b → a ≺ b ∨ b ≺ a) : IsChain r (insert a s) :=
  hs.insert_of_symmetric (fun _ _ => Or.symm) ha

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