add — Mathlib

English

If s1 and s2 are linear subsets of M, then their Minkowski sum s1 + s2 is linear.

Русский

Если s1 и s2 — линейные подмножества M, то их сумма s1 + s2 линейна.

LaTeX

$$$IsLinearSet(s_1) \land IsLinearSet(s_2) \Rightarrow IsLinearSet(s_1 + s_2).$$$

Lean4

theorem add (hs₁ : IsLinearSet s₁) (hs₂ : IsLinearSet s₂) : IsLinearSet (s₁ + s₂) :=
  by
  rcases hs₁ with ⟨a, t₁, ht₁, rfl⟩
  rcases hs₂ with ⟨b, t₂, ht₂, rfl⟩
  exact ⟨a + b, t₁ ∪ t₂, ht₁.union ht₂, by simp [vadd_add_vadd, closure_union, coe_sup]⟩

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