affineSpan_le — Mathlib

English

The affine span of a set is contained in a subspace exactly when the set is contained in that subspace.

Русский

Аффинная оболочка множества входит в подпространство тогда и только тогда, когда множество входит в это подпространство.

LaTeX

$$$\\mathrm{affineSpan}(k,s) \\le Q \\iff s \\subseteq Q$$$

Lean4

theorem _root_.affineSpan_le {s : Set P} {Q : AffineSubspace k P} : affineSpan k s ≤ Q ↔ s ⊆ (Q : Set P) :=
  (AffineSubspace.gi k V P).gc _ _

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