union — Mathlib

English

The union of two upper sets is an upper set: if s and t are upper sets, then s ∪ t is upper.

Русский

Объединение двух верхних множеств является верхним множеством: если s и t — верхние множества, то s ∪ t — верхнее множество.

LaTeX

$$$IsUpperSet s \rightarrow IsUpperSet t \rightarrow IsUpperSet (s \cup t)$$$

Lean4

theorem union (hs : IsUpperSet s) (ht : IsUpperSet t) : IsUpperSet (s ∪ t) := fun _ _ h => Or.imp (hs h) (ht h)

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