insert — Mathlib

English

In a linear order, if b is the greatest element of s, then max(a,b) is the greatest element of s ∪ {a}.

Русский

В линейном порядке, если b — наибольший элемент множества s, то max(a,b) является наибольшим элементом множества s ∪ {a}.

LaTeX

$$$IsGreatest(s, b) \\rightarrow IsGreatest(s \\cup \\{a\\}, \\(\max(a,b)))$$$

Lean4

protected theorem insert [LinearOrder γ] (a) {b} {s : Set γ} (hs : IsGreatest s b) :
    IsGreatest (insert a s) (max a b) := by
  rw [insert_eq]
  exact isGreatest_singleton.union hs

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