inter — Mathlib

English

The intersection 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 \cap t)$$$

Lean4

theorem inter (hs : IsUpperSet s) (ht : IsUpperSet t) : IsUpperSet (s ∩ t) := fun _ _ h => And.imp (hs h) (ht h)

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