inter — Mathlib

English

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

Русский

Пересечение двух нижних множеств является нижним множеством: если s и t — нижние множества, то s ∩ t — нижнее множество.

LaTeX

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

Lean4

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

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