affineSpan_coe_preimage_eq_top — Mathlib

English

Let A ⊆ P be nonempty. Then the affine hull of the preimage of A under the inclusion from affineSpan k A into P is the whole ambient space P.

Русский

Пусть A ⊆ P непусто. Тогда афинная оболочка предобраза A при включении affineSpan k A → P равна всему пространству P.

LaTeX

$$$\\operatorname{affineSpan}_k\\big(((\\uparrow) : \\operatorname{affineSpan}_k(A) \\to P)^{-1} A\\big) = \\top$$$

Lean4

/-- A set, considered as a subset of its spanned affine subspace, spans the whole subspace. -/
@[simp]
theorem affineSpan_coe_preimage_eq_top (A : Set P) [Nonempty A] : affineSpan k (((↑) : affineSpan k A → P) ⁻¹' A) = ⊤ :=
  by
  rw [eq_top_iff]
  rintro ⟨x, hx⟩ -
  refine affineSpan_induction' (fun y hy ↦ ?_) (fun c u hu v hv w hw ↦ ?_) hx
  · exact subset_affineSpan _ _ hy
  · exact AffineSubspace.smul_vsub_vadd_mem _ _

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