inter — Mathlib

English

If s and t are DirSupClosed, then their intersection is DirSupClosed.

Русский

Если множества s и t замкнуты по направленным верхним границам, то их пересечение тоже замкнуто по направленным верхним границам.

LaTeX

$$$\\forall s,t:\\,\\text{DirSupClosed}(s)\\to \\text{DirSupClosed}(t)\\to \\text{DirSupClosed}(s\\cap t)$$$

Lean4

theorem inter (hs : DirSupClosed s) (ht : DirSupClosed t) : DirSupClosed (s ∩ t) := fun _d hd hd' _a ha hds ↦
  ⟨hs hd hd' ha <| hds.trans inter_subset_left, ht hd hd' ha <| hds.trans inter_subset_right⟩

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