union — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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