inter — Mathlib

English

The intersection of two absolutely convex sets is absolutely convex.

Русский

Пересечение двух абсолютно выпуклых множеств является абсолютно выпуклым.

LaTeX

$$$\\text{AbsConvex}(𝕜\,s) \\land \\text{AbsConvex}(𝕜\,t) \\Rightarrow \\text{AbsConvex}(𝕜\\;s \\cap t)$$$

Lean4

theorem inter {s t : Set E} (hs : AbsConvex 𝕜 s) (ht : AbsConvex 𝕜 t) : AbsConvex 𝕜 (s ∩ t) :=
  ⟨hs.1.inter ht.1, hs.2.inter ht.2⟩

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