vadd_iff — Mathlib

English

A set is ample iff its affine translation is ample.

Русский

Множество ампельно тогда и только тогда, когда его аффинный перенос ампелен.

LaTeX

$$$\mathrm{AmpleSet}(y+ s) \iff \mathrm{AmpleSet}(s)$$$

Lean4

/-- A set is ample iff its affine translation is. -/
theorem vadd_iff [ContinuousAdd E] {s : Set E} {y : E} : AmpleSet (y +ᵥ s) ↔ AmpleSet s :=
  AmpleSet.image_iff (ContinuousAffineEquiv.constVAdd ℝ E y)

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