innerDual_insert — Mathlib

English

The dual cone of an insertion equals the intersection of the duals of the singleton and the rest: innerDual(insert x s) = innerDual {x} ∩ innerDual s.

Русский

Двойной конус вставки x и множества s равен пересечению двойных конусов {x} и s.

LaTeX

$$$\\text{innerDual}(\\text{insert } x\,s)=\\text{innerDual}({x})\\cap \\text{innerDual}(s)$$$

Lean4

theorem innerDual_insert (x : E) (s : Set E) : innerDual (insert x s) = innerDual { x } ⊓ innerDual s := by
  rw [insert_eq, innerDual_union]

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