inter — Mathlib

English

The intersection of two strictly convex sets is strictly convex.

Русский

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

LaTeX

$$$\text{StrictConvex}(s) \land \text{StrictConvex}(t) \Rightarrow \text{StrictConvex}(s \cap t)$$$

Lean4

protected theorem inter {t : Set E} (hs : StrictConvex 𝕜 s) (ht : StrictConvex 𝕜 t) : StrictConvex 𝕜 (s ∩ t) :=
  by
  intro x hx y hy hxy a b ha hb hab
  rw [interior_inter]
  exact ⟨hs hx.1 hy.1 hxy ha hb hab, ht hx.2 hy.2 hxy ha hb hab⟩

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