subsingleton_of_subsingleton_span_eq_top

English

If a subset s is Subsingleton and its affine span is the whole space, then the ambient space P is Subsingleton.

Русский

Если подмножество s является Subsingleton и его аффинный охват равен всему пространству, то пространство P является Subsingleton.

LaTeX

$$$ s.Subsingleton \\\\Rightarrow affineSpan(k,s) = top \\\\Rightarrow Subsingleton(P) $$$

Lean4

theorem subsingleton_of_subsingleton_span_eq_top {s : Set P} (h₁ : s.Subsingleton) (h₂ : affineSpan k s = ⊤) :
    Subsingleton P := by
  obtain ⟨p, hp⟩ := AffineSubspace.nonempty_of_affineSpan_eq_top k V P h₂
  have : s = { p } := Subset.antisymm (fun q hq => h₁ hq hp) (by simp [hp])
  rw [this, AffineSubspace.ext_iff, AffineSubspace.coe_affineSpan_singleton, AffineSubspace.top_coe, eq_comm, ←
    subsingleton_iff_singleton (mem_univ _)] at h₂
  exact subsingleton_of_univ_subsingleton h₂

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