insert — Mathlib

English

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

Русский

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

LaTeX

$$$IsLeast(s, b) \\rightarrow IsLeast(s \\cup \\{a\\}, \\(\min(a,b)))$$$

Lean4

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

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